Add support for check-sat-assuming. (#1637)

This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).

Add CVC4_PUBLIC keyword to overloads of << for Expr containers. (#1644)

Add uniform way to serialize containers of Expr to stream. (#1638)

Fixed typo.

Optimization for sygus streaming mode (#1636)

Simplify sygus wrt miniscoping (#1634)

Fixed comments in smt_engine.h.

Print candidate rewrites in terms of original grammar (#1635)

Create infrastructure for sygus modules (#1632)

SmtEngine::getAssignment now returns a vector of assignments. (#1628)

Minor fixes for rec-fun (#1616)

Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)

Improve rewriter for string indexof (#1592)

Option to not use partial function semantics for arithmetic div by zero (#1620)

Improvements to sygus sampling (#1621)

Add unit tests for BitVector, minor BV rewrite fix (#1622)

This commit adds unit tests for the BitVector class and adds some additional argument checks. Additionally, it fixes a minor issue in the ZeroExtendUltConst rule if the zero_extend was by 0 bits. In that case, the rule was calling BitVector::extract() with high < low.

Split and document bitvector.h. (#1615)

Fix cd-simplification for strings (#1624)

Minor improvements to string rewriter (#1572)

Fixed disabling the BV equality slicer for quantifiers. (#1623)

This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer.

Disable BV equality slicer if not pure QF_BV. (#1619)

Improve documentation of bv::utils::isCoreTerm (#1617)

Moved and simplified bv::utils::intersect. (#1614)

Tested against the recursive implementation with a temporary assertion on regression tests
with --bv-eq-slicer=auto.

Minor fixes and additions for transcendental functions (#1612)

Also adds parsing support for PI in smt2 with syntax "real.pi".

Unrecursified and merged bv::utils::is(Core|Equality)Term. (#1605)

This unrecursifies and merges bv::utils::isCoreTerm and bv::utils::isEqualityTerm to avoid
code duplication.

In the best case, the recursive implementation visits less nodes. This can be achieved with
the non-recursive implementation, however, at the cost of increased code complexity.
In practice, on QF_BV the new implementation slightly improves performance.

Tested against the recursive implementation with a temporary assertion on regression
tests (bv::utils::isCoreTerm was tested with --bv-eq-slicer=auto).
Further tested on QF_BV with a TO of 300s (slight performance improvement).

bv::utils::mk(And|Or) Do not return true if size of vector is 0. (#1613)

Make regress1 default, only test regress0 on Travis. (#1611)

Removed bv::utils::mkConjunction (redundant). (#1610)

Fix corner case for rewrite of mult by pow 2 (#1601)

Refactor regressions (#1581)

Fix context memory manager unit test (#1609)

Commit 83f150c727f197c530d6f46a75b516eea52bed29 changed the flag
that we use to determine whether to use the context memory manager
or the debug version. However, the change was not reflected in
the context memory manager unit test. This commit fixes the unit
test to check the correct flag.

Quantifiers subdirectories (#1608)

Remove unused cd_set_collection.h (#1606)

Provide a uniform way to serialize node containers to output stream. (#1604)

Moved (unrecursified) bv::utils::collectVars. (#1602)

Skip header for determining top contributors list. (#1603)

Option to use extended rewriter as a preprocessing pass (#1600)

Minor improvements to sygus sampler (#1598)

Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)

This unrecursifies and moves bv::utils::numNodes to an unnamed namespace in lazy_bitblaster.cpp
(only place where it is used). Tested against the recursive implementation (with a temporary
Assertion) on regression tests.

More minor improvements to synth-rr (#1597)

Move BitVector specific funs from bv::utils to util/bitvector.h. (#1589)

Remove mkNode from bv::utils (#1587)

Removing an always true comparison (unsigned) >= 0u.  (#1582)

Class to reduce printing of redundant candidate rewrites (#1588)

Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular assertion macros. This name is likely temporary while Assert() is deprecated. (#1590)

Replacing an incorrect reference to an injected class name when the type was meant. (#1585)

Replace CMM flag with debug CMM flag, fix leak in debug CMM (#1586)

Previously, we had -DCVC4_CONTEXT_MEMORY_MANAGER that needed to be added as a compile flag
to use the context memory manager (which we want by default). This makes compiling with
other build systems cumbersome because you have to know about the flag.

This commit replaces the -DCVC4_CONTEXT_MEMORY_MANAGER flag with a -DCVC4_DEBUG_CONTEXT_MEMORY_MANAGER
flag that does the opposite (in absence of the flag, we use the context memory manager).
Additionally, the commit fixes a memory leak in the debug context memory manager (the
destructor did not clean up the allocations).

Inlining line_buffered_input to avoid warning about unused variables in production builds. (#1584)

Clean up bv utils (part one). (#1580)

This is part one of an effort to clean up bv utils. It addresses review comments not addressed in
#1566 (changes of moved code), removes unused functions and moves a helper to compute the
gcd over Index.

Adding virtual destructors on classes with virtual functions. (#1583)

Minor improvements to sygus sampling. (#1577)

Updated copyright

Initializing Timer::d_wall_limit (CID 1362899). (#1573)

Simplify and cleanup bv::utils::mkConjunction. (#1571)

Check whether Cryptominisat4/ABC was installed via get-* script. (#1565)

Remove invalid regression test (#1579)

Removing an unused variable. (#1576)

Fixing more inconsistent usages of override. (#1575)

Reduce number of Travis builds. (#1578)

Fixing line numbers on type_checker_template.cpp (#1574)

Cleanup Cryptominisat header. (#1561)

Clang formatted sat_solver_factor.cpp

Use template for bv::utils::mkOr. (#1570)

Adds a new CHECK macro that abort()s on failure. (#1532)

Add remaining transcendental functions (#1551)

Use template for bv::utils::mkAnd. (#1569)

Renamed bv::utils::isBVGroundTerm to isBvConstTerm. (#1568)

Split and document theory_bv_utils. (#1566)

This moves the implementation from the header to the .cpp file. It further documents all functions in
the header file.

Use separate shell script for common get-* script parts. (#1567)

Fixes two memory leaks coming from Transf. (#1564)

First, it adds a virtual destructor so the subclasses will get cleaned up. Second, it wraps the returned
pointer in a unique_ptr. Should fix ASAN failures in the nightly run.

Updated copyright header for bv_inverter.(cpp|h).

Updated year in update-copyright script.

Resolving warnings from -Winconsistent-missing-override on clang. (#1563)

Fix two multiply-by-constant corner cases for bv rewriter (#1562)

Updated authors list

Fix rewrite for string replace (#1537)

Using getOperator() directly instead of using -1. CID 1172262. (#1559)

Aborting on errors in StatisticsRegistry::unregisterStat() instead of throwing exceptions. This is called from destructors and therefore it is inappropraiate to throw exceptions. This solution is temporary until Assert() is deprecated in favor of an aborting version. (#1539)

Statically eliminate redundant sygus constructors (#1560)

Cleaning up the printing of theory model representative sets. (#1538)

Removing references to __gnu_cxx. (#1541)

Sample based on sygus grammar by default (#1558)

Option to use sampling for CEGIS (#1555)

Restoring ostream format. Resolves a few CIDs 1362780. (#1543)

Fix remaining synthesis solution regressions (#1557)

Option to check solutions produced by SyGuS solver (#1553)

Add interface in sygus to get synthesis solution Nodes (#1552)

Use sygus to synthesize/verify rewrite rules (#1547)

Further clean and document datatypes rewriter (#1548)

Generalize explanations for PBE sygus strings based on negative contains when multiple strategies are present (#1546)

Sort children of all commutative operators for sygus. (#1544)

Removing an unused variable. Resolves CID 1172257. (#1542)

Removing structurally dead code. (#1540)

Commenting out throw specifiers on SmtEngine. These can later be refined into better documentation. (#1512)

Added unit tests for PLUS, NEG, NOT ICs for CBQI BV. (#1534)

Fix MULT handling for CBQI BV. (#1531)

Commenting out throw specifiers for DeltaRationExceptions. These functions can be cleaned up later. (#1529)

Add previous concat handling for CBQI BV as heuristic for EQ. (#1528)

Previously, we computed an inverse for s1 o x, x o s2, s1 o x o s2 while disregarding that invertibility
depends on si. This adds this handling as an optional heuristic for concats over (dis)equality since it improves performance on a considerable number of benchmarks.

Refactor and fix solveBvLit for CBQI BV. (#1526)

This refactors and simplifies solveBvLit() and fixes the following:

- generate side conditions for BITVECTOR_NEG, BITVECTOR_NOT, BITVECTOR_PLUS,
BITVECTOR_XOR over inequalities and disequality
- fix CONCAT handling (generate side conditions rather then computing an inverse which was incorrect)
- fix SIGN_EXTEND handling (same as with CONCATs)

Only push/pop around check-sat if it is associated with an assertion (#1525)

Removes yet more throw specifiers. Updating the documentation as needed. (#1518)