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().

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)

rewriter fix, weaken an assertion

constant normal form and rewrite

fix a sharing issues with sets

push subtyping for sets to the element type

for eg, (Set Int) is subtype of (Set Real) if Int is subtype of Real

enable check-models for sets/ regressions

work on set model

testlemma regressions

Merge branch 'master' of github.com:tiliang/CVC4

remove unrolling depth

bring back D-Norm

Fix strings-exp setting.

remove unrolling depth

bring back D-Norm

Fix strings-exp setting.

Add swig renames for new Z3STR language.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

Merge branch 'master' of github.com:tiliang/CVC4

adds incremental for strings; clean-up codes

adds incremental for strings; clean-up codes

Merge pull request #14 from kbansal/sets-parserchanges

Sets parserchanges

Array smtlib compliance tests

Revert "fix naming conflicts in benchmarks"

This reverts commit 4cac1b63f76a0a973a015ea6f8e21ad31d84d971.

Don't tokenize SET_THEORY operators in smt2 parser

Improving support for POW in arithmetic. Resolves bug 549.

Guard java-specific swig code with SWIGJAVA.

Without this building just the python bindings will fail.

Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>

Don't theory-preprocess under quantifiers; but DO theory-preprocess lemmas (resolves bug #548).

More useful error message when someone tries mkExpr(VARIABLE).

Merge branch 'master' of github.com:tiliang/CVC4

add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors

minor clean-up, bring back derivatives

a new regular expression engine for solving both positive and negative membership constraints

add re.nostr for the empty regular expression; add re.allchar for the regular expresssion containing all charactors

minor clean-up, bring back derivatives

a new regular expression engine for solving both positive and negative membership constraints

Merge pull request #12 from kbansal/in-to-member

rename the kind IN to MEMBER

theory/sets: cleanup

rename kind::IN to kind::MEMBER (fixes some windows build conflicts)

Merge pull request #11 from kbansal/improve-stats-every-query

--stats-every-query option: print increment in addition to cumulative va...

--stats-every-query option: print increment in addition to cumulative value of each stat

the increment is printed in parantheses at the end, e.g.
sat::decisions, 100 (50)

Bug fix for QCF algorithm, was missing instantiations.  Make prop-eq the default QCF setting.  Bug fix to prevent non-ground terms from entering relevant domains.

sorry for the missing file

bug fix (caused by merge), move cardinality option to expert option

Merge branch 'master' of github.com:tiliang/CVC4

add a new file

for merging

smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

for merging

Minor code clean up in parser.

New translation work, support Z3-str-style string constraints.

Fix quotes in string constants.

Add options --full-saturate-quant and --mbqi=trust.  Other minor changes.

smt-lib syntax change: str.contain -> str.contains; add some prefix syntax for cvc format

bug fix: strings preprocess for the orignal term, causing unknown in some cases

Merge branch '1.3.x'

No diamond-breaking under quantifiers (resolves bug #550).

Merge branch 'master' of github.com:tiliang/CVC4

reorganize substr, fix some potential bugs, adds cache for preprocessing

reorganize substr, fix some potential bugs, adds cache for preprocessing

Merge branch '1.3.x'

Fix two variants of Node::substitute().

Node::substitute() is overloaded.  One version was properly substituting
operators (e.g. the "f" in f(x) could be substituted).  The others were
ignoring anything in function position.  Fixed.  Thanks to Wei Wang for
pointing this out.

portfolio: fix export of emptyset

Fix makefile dependence for system tests.

disable test cvc3_main, attempt to fix dist_check

Merge pull request #10 from kbansal/sets-for-merge

Sets for merge

option to print stats after every satisfiability or validity query

add new theory (sets)

Specification (smt2) -- as per this commit, subject to change

- Parameterized sort Set, e.g. (Set Int)

- Empty set constant (typed), use with "as" to specify the type, e.g.
    (as emptyset (Set Int))

- Create a singleton set
    (setenum X (Set X)) : creates singleton set

- Functions/operators
    (union (Set X) (Set X) (Set X))
    (intersection (Set X) (Set X) (Set X))
    (setminus (Set X) (Set X) (Set X))

- Predicates
    (in X (Set X) Bool) : membership
    (subseteq (Set X) (Set X) Bool) : set containment

fix a -Wunused

fix makefile

add more tests, and define int.to.str(NEGATIVE)=""

add two cases to the regression test

Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

hot fix for str2int/int2str

add negative int2str

String parsing example in CVC parser

Merge branch 'master' of github.com:tiliang/CVC4

Conflicts:
src/theory/strings/theory_strings_preprocess.cpp

hot fix for str2int/int2str

add negative int2str

String parsing example in CVC parser

Fix ite and iff handling in QCF.  Add option for heuristic instantiation in QCF (not working yet).  Improve automatic option setting for quantifiers.

portfolio: add stat to track time spent waiting for interrupted threads to stop

Merge branch 'master' of github.com:CVC4/CVC4

Merge branch 'master' of github.com:tiliang/CVC4

Merge branch '1.3.x'

Stopping non-linear terms from entering the dio solver. Fixes bug 547.

add negative int2str

String parsing example in CVC parser

missed files for the latter commit

str.to.int(INVALID) = -1

switch to total function str.to.int: maps invalid and non-digit strings to 0

bring back the commits which is lost accidentally.

add str2int

Fix for strings-exp: enable quantifiers

Fix strings preprocessing for justification heuristic

Merge branch 'master' of github.com:tiliang/CVC4

type conversion

type conversion

Make QCF more incremental.  Fix bug in QCF handling of ITE formulas, add support for ITE terms.  Add full-delay inst-when mode.  Make strings come before quantifiers in check.  Minor cleanup.

partial function charat

fix expanding def