Add ability to provide theory-specific proof rules to EqualityEngine, extends enumeration of MergeReasonType.  Add initial use in TheoryArrays.

Add working example of LFSC proof with quantifiers.  Update quantifiers signature to avoid dependent types in side condition.

Work on array pf signature, add working example.  Add quantifiers proof signature. Ignore terms not in current master EE for QCF.  Minor refactoring.  Make --rewrite-rules true by default.

Minor fixes post-merge of RR.

Fix LogicInfo unit test.

Some standardization of regression Makefiles that got out of sync.  Fixes cases of nonterminating rewrite-rules regressions.

Draft contrib/get-abc script for bitvectors libabc support.

Merge branch '1.3.x'

Fix for rewriterules build breakage.

Fix for random-seed option.

Fix for portfolio.

Minor cleanup.

* Reenable parts of bvsimple test
* Fix typo in #endif comment

Fix for (get-assignment), resolves bug 553.

Merge branch '1.3.x'

Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok.

Initial refactor of rewrite rules, make theory_rewriterules empty theory.  Push kinds to quantifiers/kinds, rewrite rewrite rules in rewriter.

Fix rewrite rule attribute, refactor QCF, instantiation engine does not register rewrite rules, minor clean up.

QCF is now functional backend to rewrite rules. Support boolean variables in QCF.  Change check-model to ignore rewrite rules.  Incorporate some fixes from master.

Move rewrite of rewrite rules from rewriter to preprocessor, attribute becomes pattern.

Minor fixes to QCF/rewrite engine, removes RE on last call approach.  Add option for one inst per round in RE.

Merging rewrite rules into master, check-model current fails on 3 FMF regressions.

Fix check-model issue, a line of code was omitted during merge.

adds intro vars length cache

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

minor change for strings-fmf

minor change for strings-fmf

Re-fix bug 551 by adding a check to the arith ITE simplifier to ignore non-ground ITEs also.

Merge pull request #18 from timothy-king/master

Merging in the glpk changes

Fixing name changes that cam in from the merge.

Merge remote-tracking branch 'CVC4root/master'

Remove --ite-remove-quant; support pulling ground ITEs out of quantifier bodies; fix bug 551, improper ITE removal under quantifiers.

Fix run_regression on Mac.

Fix bug 554 (nominally).

Fixing a SWIG problem for RationalFromDoubleException.

Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into   See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

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.