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)

Fix unit tests for ineq for CBQI BV. (#1456)

Add unit tests for side conditions for inequality for CBQI BV. (#1455)

Fixes for cbqi (#1453)

Rel smt parser (#1446)

Minor refactor for inequality handling for CBQI BV. (#1452)

Disable sygus PBE when sygus stream is enabled (#1451)

Fixes for cbqi-bv (#1449)

Add explicit disequality handling when generating side condition for CBQI BV. (#1447)

This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.

Add rewriting rule for ranking benchmarks. (#1448)

Transcendental functions check model (#1443)

Fix travis write errors. (#1445)

For reasons unknown, after the latest update of the Trusty environment on Travis,
we encountered write errors for the three Clang builds. As suggested here
https://github.com/travis-ci/travis-ci/issues/4704#issuecomment-321777557,
adding filter_secrets: false to the .travis.yml fixes the problem.

Note: switching back to the deprecated builds did not fix the problem.

Enable side condition handling for shifts introduced in #1441. (#1444)

PR #1441 forgot to enable the missing side condition handling for shifts. This PR enables it.

Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)

This adds side conditions for operators BITVECTOR_SHL, BITVECTOR_LSHR and
BITVECTOR_ASHR for index = 1, i.e., s << x = t and s >> x = t. Previously, we treated
 these cases as non-invertible.

Add SIGTERM handler. (#1440)

Print statistics if CVC4 gets a SIGTERM signal.

Add new infrastructure for preprocessing passes (#1053)

This commit adds new infrastructure for preprocessing passes. It is preparation only, it does not change how the current preprocessing passes work (this will be done in future commits).

Fix issue 1433. (#1435)

Fix issue with mkConst/getConst of TypeConstant (#1439)

When compiling the Java bindings on macOS, the linker complained about
CVC4::ExprManager::mkConst<CVC4::TypeConstant>() and
CVC4::Expr::getConst<CVC4::TypeConstant>() being undefined. After some
research, I found that the issue has been introduced by commit
36bf9f8bcb2a1a3aea1f90eb4d13aed3bbf6da8f. It looks like adding the
-no-undefined flags resulted in the symbols in question being omitted
due to TypeConstant not being exported. This commit makes TypeConstant
CVC4_PUBLIC, which fixes the issue.

Add CEGQI BV linearization of additions and equalities over additions. (#1417)

Adds support for linearizing additions w.r.t. to a variable.

For example,

a * x + b + c * d * -x = e + x

is rewritten to

x * (a - c * d - 1) = e - b.

This also adds an additional rewriting rule x * x = x --> x < 2.

Fixed side conditions for CBQI BV, added unit tests. (#1434)

This fixes the side conditions for BITVECTOR_UREM_TOTAL, BITVECTOR_UDIV_TOTAL,
BITVECTOR_LSHR, BITVECTOR_ASHR, BITVECTOR_SHL.

It refactors side condition generation for better readability and unit testing.
It further adds unit tests for all side conditions we generate in order to check if they too weak
or to restrictive (which may result in unsound behavior).

This is achieved by checking the following two implications:
not (exists x. s * x = t => SC) ... if sat, SC is too restrictive
not (SC => exists x. s * x = t) ... if sat SC is too weak

This simplifies to checking not (SC <=> exists x. s * x = t).

Document and clean datatypes rewriter (#1437)

Make collect model info return a Bool (#1421)

Fixes related to SyGuS + real arithmetic (#1432)

Add command for define-fun-rec and add to API (#1412)

Fixed time stats for MiniSat solve time. (#1431)

Also, moved implementation of BVMinisatSatSolver::MinisatNotify::notify to .cpp file.

Remove CDChunkList (#1414)

Fix output of --show-trace-tags. (#1430)

Now prints each tag in a separate line.

Adding SyGuS grammars for rationals. (#1426)

Eliminate expand definitions from Sygus (#1425)

Fix strings rewriter for strip constant endpoint reverse direction (#1424)

Fix side condition for BITVECTOR_MULT. (#1422)

Normalize grammars - 2 (#1420)

This is another step towards addressing #1304 and #1344. This pull request:

- Refactors SygusGrammarNorm
- Makes SyGusGrammarNorm a default component in the construction of grammar. The linearization of grammars however only occurs if the option --sygus-grammar-norm is used.
- Performs a "chain transformation" in the application of the PLUS operator in integer grammars
- Removes redundant expansions of definitions from TermDbSygus
- Adds a default empty print callback to SygusEmptyPrintCallback

This lays the basis for more general linearizations.

Minor improvements to inst match generator (#1415)

Improve rewriter for string replace (#1416)

Fix reset-assertions (#1413)

This commit fixes two issues with reset-assertions:

- pending pops were not done in SmtEngine, resulting in the following
  assertion failure:

  d_userLevels.size() == 0 && d_userContext->getLevel() == 1

- all definitions were erased on reset-assertion in an SMT2 file,
  leading to errors about undefined types

Minor additions for sygus (#1419)

Refactor and generalize PBE strategies (#1410)

Fix build when Valgrind instrumentation enabled

My last commit for the Valgrind instrumentation contained a typo that
made the nightlies fail. This commit fixes the issue.

Add debugging tools for ContextMemoryManager (#1407)

This commit adds two configuration options that help debugging memory
issues with allocations in the ContextMemoryManager:

--enable/disable-valgrind: This flag enables/disables Valgrind
instrumentation of the ContextMemoryManager. Enabled by default for
debug builds if the Valgrind headers are available.

--enable/disable-context-memory-manager: This flag enables/disables the
use of the ContextMemoryManager. If the flag is disableda dummy
ContextMemoryManager is used that does single allocations instead of
chunks. The flag is enabled by default.

Add Gaussian Elimination as a preprocessing pass for BV. (#1342)

This adds Gaussian Elimination as a preprocessing pass for BV. Gaussian Elimination is only applied if the given bit-width guarantees that no overflows can occur.

Fixes for issue 1404 (#1409)

Remove remaining references to QuantArith (#1408)

Minor improvements and changes to defaults for cbqi bv (#1406)

This

makes it so that --cbqi-bv tries at most 2 instantiations per quantified formula (one based on inversions when applicable, one based on model values). This makes it so that we do not have exponential run time in the worst case. This helps significantly for psyco benchmarks which have many quantified variables.

Enables --cbqi-bv by default and changes the default inequality mode to eq-boundary (which is the best performer overall), also enables extract removal by default

Allows cbqiNestedQE to be used in the BV logic.

Adds an option --cbqi-full which indicates whether we should try model value instantiations for bit-vectors (by default, this is done only for the pure BV logic).

Improve caching in term formula removal (#1398)

Adding missing break statements. CID 1362756. (#1394)

Simplifying the conditions in checkLetBinding to avoid using iterator… (#1372)

Add Cryptominisat script and patches to source file distribution.

This enables building CVC4 from a source release with Cryptominisat support.

Improve the rewriter for SINE. (#1221)

Improve rewrite for string substr (#1337)

Improve trigger filter instances (#1402)

Removing throw specifiers from internal Printer hierarchy. (#1393)

Fix models for --solve-real-as-int. (#1371)

Fixes for higher-order (#1405)