Add option multi-trigger-linear, minor optimization to E-matching.

Merge pull request #139 from 4tXJ7f/remove_throw

[Coverity] Remove throw qualifiers in src/smt

[Coverity] Remove throw qualifiers in src/smt

Addresses coverity issues:

1172167
1172174
1172176
1172183
1172185
1172186
1172188
1172189
1172191
1172192
1172193
1172194
1172197
1172197
1172198
1172434
1172437
1172438
1172443
1172445
1172446
1172447
1172448
1362695
1362700
1362717
1362736
1362768
1362786
1362811
1379599
1421404
1421405
1421406
1421407
1421408
1421409
1421410
1421411
1421412
1421413

Minor fixes for trigger selection max.

Add quantifiers options related to model and master equality engine.

Merge pull request #138 from PaulMeng/master

Refactor the standard effort of relational solver

Refactor the standard effort of relational solver

Fix bug 787.

Fix for bug 733

Minor refactoring sygus.

More work on sygus. Add regress4 to Makefile.

Fixing a bug for checking whether a node was visited.

Minor cleanups to ExtTheory.

Removing the friend class modifier from ExtTheory to Theory.

Merge pull request #137 from 4tXJ7f/throw_quals

Remove throw qualifiers in type enumerators

Making the ExtTheory object a private member of Theory.

Making ppNotifyAssertions take a const vector.

Moving the CareGraph into its own file.

Moving the theory::Assertion struct into its own file.

Remove throw qualifiers in type enumerators

This addresses Coverity issues:

- 1172154
- 1172156
- 1172157
- 1172158
- 1172159
- 1379612
- 1379612
- 1421430
- 1172166
- 1172144
- 1362709
- 1362696
- 1172145
- 1172147
- 1172148
- 1379610
- 1362772
- 1362676
- 1362704
- 1362749
- 1362876
- 1362843
- 1362837
- 1362881
- 1172223
- 1172155

Alphabetizing libcvc4_la_SOURCES.

Add some regressions. Minor.

Refactor model building for quantifiers to be a single pass, simplification. Modify datatypes collect model info to include dt equivalence classes. Further work on sygus. Other minor fixes.

Fixing warning message.

support incremental unsat cores

Fix more cases of rewritten explanations in strings for bug 784. Minor.

Minor fix for bounded integers.

Work on new approach for sygus involving conditional solutions. Refactoring of sygus solver. Bug fix for sygus solution reconstruction.

Improve computeCareGraph functions to check shared term equality status once per equivalence class pair.

Merge pull request #135 from PaulMeng/master

fixed cvc4 parser for set complement

fixed cvc4 parser for set complement

Fix for bug 707.

Fix to help with bug 717

better support for proof production when encountering bool terms: handle the new proof constructs generated by the equality engine.

proof production for bool-array.smt2 passes

Fixes bug 781. Copy constructor for Expr needed to set the NodeManagerScope.

More fixes, features to examples.

Minor fixes, always expand applications of lambdas at preprocess.

Support for SMT LIB 2.6 syntax declare-datatype and match.

Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.

Fix regress1 Makefile for rewriterules, fixes bug 783.

Merge pull request #134 from 4tXJ7f/fix_host

Fix win-build script to use MinGW-w64 by default

Allow 0 argument recursive functions. Fixes bug 782.

Fix win-build script to use MinGW-w64 by default

Previous changes to the win-build script left the script in an
inconsistent state: the script was updated to refer to MinGW-w64 but the
default host was still referring to MinGW.

Merge pull request #133 from 4tXJ7f/fix_uninitialized

Fix uninitialized variable

fix uninitialized variable

Merge pull request #132 from 4tXJ7f/fix_mingw64

Fix MinGW-w64 build

Minor fix for cbqi-all.

bug fix

better proof support for bools and formulas

Fix MinGW-w64 build

This commit fixes configure.ac to try to get clock_gettime() from
pthread. Without it, clock_gettime() is detected as missing at
configuration time for MinGW-w64 but exists at compile time, which
causes conflicts. Additionally, this commit updates the helper script
for Windows to use MinGW-w64 by default instead of MinGW.

More fixes for printing/parsing sets, fix kind name.

Fix cvc parser for set compliment.

Do not eagerly construct explanations in relation solver.

Support for set compliment and universe set. Simplify approach for sep.nil nodes.

Adding support for bool-to-bv

Squashed commit of the following:

commit 5197a663eb262afbeb7740f53b5bd27479dccea0
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Mar 6 00:16:16 2017 -0800

    Remove IFF case

commit 2119b25a30ed42eca54f632e7232c9f76ae5755a
Author: guykatzz <katz911@gmail.com>
Date:   Mon Feb 20 12:37:06 2017 -0800

    proof support for bvcomp

commit d8c0c0d2c9c92ce06a5033ec0f3f85ea7bda1a22
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 21:09:04 2017 -0800

    Added missing cases to operator<< for bv rewrite rules.

commit 0ed797c31d0e66cadc35b2397716c841d1aff270
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Fri Feb 17 11:43:51 2017 -0800

    Added rewrite rules for new bitvector kinds.

commit 3b23dffb317de5559f8a95118fef633f711c114a
Author: Clark Barrett <barrett@cs.stanford.edu>
Date:   Mon Feb 13 14:41:49 2017 -0800

    First draft of bool-to-bv pass.

Fix for collectModelInfo related to finite types + preregistration. Generalize previous fix for sets, minor changes to Datatypes.

Another minor fix for sets related to sharing + finite element types.

Fixes related to sets.

Minor cleanup and reorganization related to last commit.

Eliminate Boolean term conversion. Generalizes removeITE pass to remove Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.

Minor fixes for relations, quantifiers dsplit.

Fixes for sets+rels check. Minor.

Minimization modes for fmf bound.

Generalize finite bound inference to unifiable variables in set membership literals.

Fix regexp cache issue in strings, add regression.

Fix non-idempotent rewrite in Array rewriter

This commit fixes bug 637 (
http://church.cims.nyu.edu/bugzilla3/show_bug.cgi?id=637 ) as
proposed in Bugzilla and adds the minified test case to the
regression tests.

Merge pull request #128 from 4tXJ7f/fix_lfsc_perf

[LFSC] Fix performance issues, more determinism

Minor fix in relations.

[LFSC] Fix performance issues, more determinism

For certain proofs, the performance was drastically different on
different OSes. The cause for this difference was a pointer comparison
in the deduplication in `Expr::defeq()`. Depending on how the OS
allocated the memory, an expression `a` would get replaced with an
equivalent expression `b` or vice versa, which in turn affected
performance of `Expr::free_in()` dramatically (sub-second vs. >5 min
running times). This commit makes the process more deterministic by
using a heuristic that favors symbolic expressions and greedily tries to
make small refcounts smaller when replacing, and changes
`Expr::free_in()` to not repeatedly explore the same subexpressions.

Fix call to SExpr constructor for greater portability.

Merge pull request #130 from chadbrewbaker/master

Fixing memory leak

Do not rewrite explanations in strings.

Merge pull request #129 from timothy-king/regression-scrubber

Adding regression test scrubbing.

Merge pull request #131 from makaimann/fix_702

Proposed fix for bug 702

Proposed fix for bug 702. Checks to make sure the Expr's operator is not of kind BUILTIN before passing to prefixPrintGetValue()

Fix for when variables are (partially) bound in multiple ways, add regression. Improve printing for bound int module. Track when relations are enabled in sets, set incomplete if card+rels are both enabled since model construction is not guaranteed to succeed.

Merge pull request #127 from cristian-mattarei/issue_679

Bug 679 fix

revert

Quashing memory leak

Adding regression test scrubbing.

With reference to Bug 679, this commit integrates part of the patch proposed, and it fixes the correct float parsing of an std::istringstream.

The compilation issue in Bug 679 does not apply anymore with gcc6.3.1

quashing debug memory leak

Minor fix for sets.

Disabling a regression test that assumes CVC4 is configured with proofs on. Modifying the travis rules so there are instances with proofs disabled.

Fix for tff type declarations inTPTP parser, fixes bug 748.  Other minor changes.

Marking regression test files as non-executable.

Marking the proof signature files as non-executable.

Setting the executable bit for the newer run scripts in contrib.

Reverting two files encoding with DOS linebreaks back into using unix linebreaks.

Merge pull request #122 from 4tXJ7f/fix_lfsc_str

[LFSC] Minor fixes/improvements

Merge pull request #120 from 4tXJ7f/fix_f_pp_holes

Fix dependency tracing for fewerPreprocessingHoles

Merge pull request #121 from 4tXJ7f/fix_lfsc_mem_leaks

[LFSC] Fix memory leaks when creating CExprs

Changing a set of TNodes to a set of Nodes in the BV inequality solver. The ref count of the TNodes in the set can become 0. Set operations containing garbage collected TNodes could then fail.

Eliminating a signed vs. unsigned comparison.

Changing getTearDownIncremental() to return the type of options::tearDownIncremental.

Adding a destructor to InstantiationNotify.

Adding a destructor to RepBoundExt.

Reordering sep and sets in Makefile.theories.

[LFSC] Minor fixes/improvements

- Avoid mixing new/delete with malloc/free
- Remove reimplementation of strcmp
- Add assertions

[LFSC] Fix memory leaks when creating CExprs

In certain cases, LFSC was creating CExprs with the single-argument
constructor, which allocates an array of one child, only to immediately
replace it with a new array (without deleting the old one).
Additionally, this commit fixes the construction of TYPE/KIND/MPZ/MPQ
expressions (the null pointer is appended automatically by the single
argument constructor, an array with two null pointer entries should not
be necessary).