Fix documentation for Theory::preRegisterTerm().
Minor fix for CBQI, ignore inst constant nodes.
testlemma regressions
work on set model
enable check-models for sets/ regressions
push subtyping for sets to the element type

for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real
fix a sharing issues with sets
constant normal form and rewrite
rewriter fix, weaken an assertion
Fix for registration issues of term appearing in a shared lemma

(brought to attention by lianah -- fix currently just adapted using
arrays -- this is to remind me to raise why do we even have this
isPreregistered bussiness)
fix for sets/mar2014/..317minimized..

Observed behavior:
  --check-model failed for set-term (union (z3f69 z3v151) (setenum z3v143))
with different set of elements in the model for representative and the node
itself.

Issue:
  The trouble with data structure being mainted to ensure that things
for which lemmas have been generated are not generated again. This
data structure (d_pendingEverInserted) needs to be user context
dependent. The bug was in the sequence of steps from requesting that
a lemma be generated to when it actually was. Sequence was:
addToPending (and also adds to pending ever inserted) ->
isComplete (might remove things from pending if requirment met in other ways) ->
getLemma (actually generated the lemma, if requirement not already met)

Resolution:
  adding terms to d_pendingEverInserted was moved from addToPending()
to getLemma().
cleanup
Merge pull request #22 from kbansal/sets-model

Sets model
adds intersection
Fixes an idempotency issue for non-linear multiplication with integer and real variables.
Merging in a fix from 1.3.x.
Fixes an idempotency issue for non-linear multiplication with integer and real variables.

Conflicts:
	src/theory/arith/normal_form.cpp
deriv symbolic regexp
adds intersection
deriv symbolic regexp
Merge branch 'master' of github.com:tiliang/CVC4