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

added initial AX rules;
fixed a bug for empty string in regex

added initial AX rules;
fixed a bug for empty string in regex

Disable prenex by default when using fmf bound int, minor improvement to datatypes rewriter

Adding an option to the equality engine constructor to treat all constants as
trigger terms. I've disabled constants as triggers for all equality engines
except for the shared terms engine where it is needed.

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

bug fix for constant regular expression model building

bug fix for constant regular expression model building

Do not collapse wrongly applied selectors for non-well-founded codatatypes pre-model.

Add misc trigger options.

Fix oversight in dumping assertions in preprocessing.

Add cvc parsing support for cardinality constraints.  Bug fix for enumerating elements to meet cardinality lower bounds.

Minor fixes to language bindings. (Resolves #607.)

Option to enable/disable cyclicity check in datatypes.

bug fix, thanks to Guy's example.

Better error description (related to bug 605).

Cleanup.

Added string constant in java api example.

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

Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

Added C++/Java api examples;
Converted cset to be vector of char, instead of vector of int, since we only accept ascii in input.

Fix dt.size care graph.

Relaxed the constant requirement for regular expression loop;
Added "ignoring negative membership" option (fragment checking is not provided,
and users must make sure the constraint is in the fragment;
otherwise, the solution may not be correct).

clean up and improve intersection

Fix valgrind-flagged error about uninitialized value.

Fix segfault in lambdas when constructed via API.

Fix UnsatCore in language bindings.

Floating point infrastructure.

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

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

Revert "Disable constants sharing in eq engine, disable hack in theory engine."

This partially reverts commit f70804a7159390fcb01d8c1ec208fbfd8e544fba.

In particular, it DOES NOT revert
  "Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine."
which is part of the same commit.

disable inter cache

Synchronize conjecture generation with E-matching.  Minor fix to --full-saturate-quant.

add intersection rewriting

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

add more regexp rewriting

add more functions for regular expressions

add more regexp rewriting

add more functions for regular expressions

Fix bug in --term-db-mode=relevant with variable triggers.  Support inst-closure predicate and mode --term-db-inst-closure.  Minor changes to theory_quantifiers.

added number of resource units used as a stat

Throw error when pattern is not list of terms.

Change default option to --inst-when=full-last-call (interleave instantiation and theory combination).  Fix inefficiency in NNF, enable by default.  Set best defaults for --mbqi=abs.

Disable constants sharing in eq engine, disable hack in theory engine.  Changes to strings solver : modify lemmas/splits to avoid constants, minor refactoring.  Fix assertion failure in quantifiers engine.

Fix #lines in template.

Making construction of trigger sets not use the global engine state.

Distribute UnsafeInterruptException interface file for SWIG.

Merge pull request #70 from kbansal/sets-for-merge-squashed

Set Constant's normal form and other short fixes

Set Constant's normal form and other short fixes

Other short fixes:
* use debug tag "theory::assertions::fulleffort" to dump assertions only at FULL_EFFORT
* theoryof-mode fix in smt_engine.cpp
* hack in TheoryModel::getModelValue [TODO: notify Clark/Andy]
* Lemma generation when it rewrites to true/false fix
* TermInfoManager::addTerm(..) fix
* Move SUBSET rewrite to preRewrite
* On preRegister, queue up propagation to be done upfront
** Hospital4 fails when all other fixes have been applied but not this one. Good to have an actual benchmark which relies on this code.
* TheorySetsProperties::getCardinality(..) fix

Thanks to Alvise Rabitti and Stefano Calzavara for reporting some of these; and to Morgan and Clark for help in fixing!

clear model cache in BVQuickCheck clearSolver() (fixes bug 587)

All Minisat solve calls now return lbool (fixes bug 599)

Compute model basis only for fmf.  Add another co-datatype regression.

Add local theory extensions instantiation strategy (incomplete).  Refactor how default options are set for quantifiers.  Minor improvement to datatypes.  Add unsat co-datatype regression.  Clean up instantiation engine.  Set inst level 0 on introduced constants for types with no ground terms.  Return introduced constant for variable trigger when no ground terms exist.

added command line option for extractArith bv rewrite

Short-circuit in TheoryArithPrivate::check(), care of Tim.

New, uniform checkTime statistic for all theories (as discussed in meeting).

Resource-limiting work.

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

Add term db mode.  Minor changes to quantifiers rewriter: split ITE's where equality resolution is possible on condition, pull nested quantifiers from ITE branches.  Minor cleanup.

Be lazier to consider EQC in UF+cardinality solver.  Minor cleanup.

Minor changes to AUTHORS and COPYING

Minor adjustments to wording.

Copyright text fixes.

Merge pull request #69 from mdeters/bug594

Fix memory leak in CDHashMap<> with Node keys (resolves bug 594).

Remove two obsolete versions of MBQI.

More preparation for filtering relevant terms in TermDb.

Possible fix for bug594

Merge pull request #65 from mdeters/bv-ineq-cachefix

Fix BV inequality solver caching, and TNode fix.

BV inequality graph TNode fix.

Fix BV inequality solver caching.

Fix tokenization of "reset" in SMT-LIB v2.0.  It's a reserved word only in 2.5.

Minor cleanup.

Merge pull request #64 from mdeters/theorysets-hashset-iteration

Update TheorySets to use CDHashSet<>::key_begin() / key_end().

Work on synchronizing decision=justification and E-matching.

Merge pull request #63 from mdeters/theorystrings-hashset-iteration

Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().

Bug 593 fix: if the type is finite, it is now considered for detecting theories of nested terms.

Do not eliminate variables only occurring in patterns.  Minor improvements to sort inference.  Remove unused code.

Merge branch '1.4.x'

Update TheorySets to use CDHashSet<>::key_begin() / key_end().

Update TheoryStrings to use CDHashSet<>::key_begin() / key_end().

Work around an apparent bug in libc++ that was causing crashes on Mac..

Fix a deterministic assignment-ordering for get-assignment (fixes a regression failure on Mac).

Increase stack size when running regressions (fixes some regression crashes on Mac).

Fix dt shared terms issue, reenable regression.

Fix bug with incremental+datatypes.  Minor cleanup.  Disable regression bug484, enable parsing_ringer.

Merge pull request #62 from mdeters/bv-cleanup

Remove some unused variables.

Remove some unused variables.

Fixed bug in model builder with subtypes

Remove some dead code.

Fix a memory leak in SatSolverRegistry (re: bug #594).

Fix memory issues in bitvector theory, which is now valgrind-clean (mostly resolves bug #594).

Merge branch '1.4.x'

Conflicts:
src/smt/model_postprocessor.cpp
test/regress/regress0/Makefile.am

Fix missing case in Boolean terms rewriting.  (Resolves bug #596.)

Merge branch '1.4.x'

Conflicts:
src/smt/model_postprocessor.cpp

Corrected fix for missing case in model postprocessor (resolves bug #595).

Enable --quant-cf by default.  Fix bug in qcf for mixed Int/Real.  Minor improvement to performance of E-matching.

Revert "Fix missing case in model postprocessor (resolves bug #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

Revert "Fix missing case in model postprocessor (resolves bug #595)."

This reverts commit 61042cf551b19d06673be2b069bacc7cb1cd775a.

Conflicts:
test/regress/regress0/Makefile.am

Update competition build rules.

Merge branch '1.4.x'

Conflicts:
test/regress/regress0/Makefile.am

Fix missing case in model postprocessor (resolves bug #595).

Properly distinguish which EQC to assign values in datatypes, use assertRepresentative.  Disable regression related to records.  Enable fmf-fun related regression (modified).  Apply modified version of Morgan's patch to fix tuples/records in model.  Fix bug with sort inference + patterns.  Minor infrastructure.