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)

Removing more miscellaneous throw specifiers. (#1509)

Removing more miscellaneous throw specifiers. Also fixing the spelling of amount in several places.

Removing throw specifiers from Type. (#1511)

Removing throw specifiers from OptionsHandler. (#1510)

Remove BITVECTOR_SUB from isInvertible(). (#1513)

Improvements for CBQI BV (#1504)

Removed division by constant handling for CBQI BV (unsound). (#1508)

This removes division by constant handling in the BV inverter introduced in #1498.
Division by constant was simplified to:
x / s OP t ---> x = t / s^-1 if s odd and there exists a multiplicative modular inverse s^-1.
This however, is incorrect since
x / s * 1 / s^-1 != x / (s * s^-1)

Removing throw specifiers for TypeRules. (#1501)

Removing throw specifiers from type enumerators. (#1502)

Cleaning up throw specifiers on Exception and subclasses. (#1475)

Fix linearization for terms where the solve variable does not occur. (#1506)

Reorganized bitvector.h. (#1505)

Fix output of --trace=help. (#1500)

Removing throw specifiers from miscellaneous src/expr/ classes. (#1503)

Removing more miscellaneous throw specifiers. (#1488)

Removing more miscellaneous throw specifiers.

Add bv util mkConst(unsigned, Integer&). (#1499)

Remove throw specifiers from symbol table. (#1490)

Added division by constant handling for CBQI BV. (#1498)

Remove portfolio option from builds. (#1496)

Removes throw specifiers from command.{h,cpp}. (#1485)

Improvements to quant+BV/Bool variable elimination (#1495)

Fix broken GMP URL in get-win-dependencies script (#1493)

Remove throw specifiers from datatype. (#1489)

Re-ordering field initialization in QuantInfo to remove compiler warning. (#1487)

Removes RationalFromDoubleException. Replaces this with an explicit M… (#1476)

* Removes RationalFromDoubleException. Replaces this with an explicit Maybe<Rational> datatype. Makes Maybe<T> CVC4_PUBLIC. Updates the users of Rational::fromDouble(). Miscellaneous cleanup of ApproxSimplex.

Removing throw specifiers from src/parser/. (#1486)

Add special {SGE,SGT,NE}_UDIV1 side conditions for BV of size 1. (#1483)

This commit further fixes some other issues with bit-vectors of size 1.

Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1, SHL0, SHL1. (#1482)

Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)

Fix side condition handling for PLUS, XOR, SIGN_EXTEND for CBQI BV. (#1480)

Add side conditions for inequalities of SHL. (#1472)

Improvements for CBQI (#1478)

Includes:

- Basic rewriting for choice functions in the builtin rewriter,
- Do not consider more than one equal term in ceg instantiator (helps cases where we have a
  repeated pattern of duplicate instantiations),
- Do not introduce dummy extract equalities in the cbqi-bv-rm-extract pass (dummy concat
  equalities suffice).
- Do not consider extracts in nested quantified formulas in the cbqi-bv-rm-extract pass.

Removing miscellaneous throw specifiers. (#1474)

Removing throw specifiers from context/. (#1473)

Add side conditions for UGT/SGT over BITVECTOR_UREM for CBQI BV. (#1470)

Add UGT/SGT side conditions for LSHR. (#1469)

 Add side conditions for inequalities over BITVECTOR_MULT for CBQI BV. (#1468)

Global negate (#1466)

 Add side conditions for inequalities of ASHR. (#1461)

Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)

We now can handle all cases of (in|dis)equality over BITVECTOR_UREM. This also simplifies some
of the side conditions for equality.

Simplify side condition for SGE over UREM (index = 1) for CBQI BV. (#1463)

Fix handling for UGT/SGT. (#1467)

Previously, we only handled the case x s < t. With this fix, we now get BITVECTOR_[SU]GT for litk
if we encounter a literal t < x s.

Rewrites for BitVector multiplication (#1465)

Add side conditions for inequalities of LSHR. (#1462)

Improve rewriter for string equality (#1427)

Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)

We now can handle all cases of (in|dis)equality over UREM. Previously, we could not handle equality
for index=0 and had to rewrite x % s = t to x - x / s * s. Since we can now handle this case, we do not
apply this rewriting anymore.

Fix RNG for seed = 0. (#1459)

The default value for the seed for CVC4's RNG is 0. However, xorshift* requires a non-zero seed, else it generates only zero values. This fixes and prevents this behavior by resetting a given zero seed to ~0.

Cbqi repeat solve literal (#1458)

Add side conditions for inequalities of AND/OR. (#1457)