cvc5.git - CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.

Age	Commit message (Collapse)	Author
2018-03-08	Cleanup Cryptominisat SAT wrapper. (#1652)	Mathias Preiner
	Cryptominisat has name conflicts with the other Minisat implementations since the Minisat implementations export var_Undef, l_True, ... as macro whereas Cryptominisat uses static const. In order to avoid these conflicts we forward declare CMSat::SATSolver and include the cryptominisat header only in cryptominisat.cpp. Further, the helper functions are moved into an anonymous namespace in the .cpp file and functions that were not used are removed.
2018-03-08	Fixed message in get-antlr script.	Aina Niemetz

2018-03-08	Fix Travis for unit test compilation errors. (#1651)	Mathias Preiner
	make units does not fail if we have compile error for a unit test, however, make check does. -Wsuggest-override is now explicitly disabled for unit tests since CxxTest does not add override keywords to the generated source code and thus get a lot of compiler warnings. Further, this fixes some issues introduced with #1647 due to make units not failing on Travis and fixes the nightly builds.
2018-03-06	Make statistics output consistent. (#1647)	Mathias Preiner
	* Fixes --hide-zero-stats (and really skips the 0 values) * Removes the additional newline after each statistic * Introduces theory::getStatsPrefix(TheoryId) to generate consistent prefixes for statistics based on the theory id (e.g., THEORY_BV -> "theory::bv").
2018-03-06	Simplify initialization of quantifiers engine (#1641)	Andrew Reynolds

2018-03-06	Refactor symmetry breaking in datatypes sygus (#1640)	Andrew Reynolds

2018-03-06	Remove printf from output utilities (#1629)	Andres Noetzli
	This commit removes the unused printf functions from the output utilities. It also adds `const` keywords where possible. Finally, it removes overloaded `const char` functions if the same function existed for `const std::string&` and the `const char` version was only casting the `const char` to an `std::string`. This conversion happens implicitly, so the `const char` version is not needed.
2018-03-05	Update semantics for string indexof and replace (#1630)	Andrew Reynolds

2018-03-05	Fix boost url in contrib/get-win-dependencies.	Mathias Preiner
	This fixes the broken windows nightly builds.
2018-03-05	Enable -Wsuggest-override by default. (#1643)	Mathias Preiner
	Adds missing override keywords.
2018-03-05	Fix for sampler. (#1639)	Andrew Reynolds

2018-03-05	Add support for check-sat-assuming. (#1637)	Aina Niemetz
	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)).
2018-03-05	Add CVC4_PUBLIC keyword to overloads of << for Expr containers. (#1644)	Aina Niemetz

2018-03-05	Add uniform way to serialize containers of Expr to stream. (#1638)	Aina Niemetz

2018-03-02	Fixed typo.	Aina Niemetz

2018-03-02	Optimization for sygus streaming mode (#1636)	Andrew Reynolds

2018-03-02	Simplify sygus wrt miniscoping (#1634)	Andrew Reynolds

2018-03-02	Fixed comments in smt_engine.h.	Aina Niemetz

2018-03-02	Print candidate rewrites in terms of original grammar (#1635)	Andrew Reynolds

2018-03-01	Create infrastructure for sygus modules (#1632)	Andrew Reynolds

2018-02-28	SmtEngine::getAssignment now returns a vector of assignments. (#1628)	Aina Niemetz

2018-02-27	Minor fixes for rec-fun (#1616)	Andrew Reynolds

2018-02-27	Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)	Aina Niemetz

2018-02-27	Improve rewriter for string indexof (#1592)	Andrew Reynolds

2018-02-27	Option to not use partial function semantics for arithmetic div by zero (#1620)	Andrew Reynolds

2018-02-27	Improvements to sygus sampling (#1621)	Andrew Reynolds

2018-02-23	Add unit tests for BitVector, minor BV rewrite fix (#1622)	Andres Noetzli
	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.
2018-02-23	Split and document bitvector.h. (#1615)	Aina Niemetz

2018-02-23	Fix cd-simplification for strings (#1624)	Andrew Reynolds

2018-02-22	Minor improvements to string rewriter (#1572)	Andrew Reynolds

2018-02-22	Fixed disabling the BV equality slicer for quantifiers. (#1623)	Aina Niemetz
	This fixes an incorrect condition introduced in #1619 to disable the BV equality slicer.
2018-02-21	Disable BV equality slicer if not pure QF_BV. (#1619)	Aina Niemetz

2018-02-20	Improve documentation of bv::utils::isCoreTerm (#1617)	Aina Niemetz

2018-02-20	Moved and simplified bv::utils::intersect. (#1614)	Aina Niemetz
	Tested against the recursive implementation with a temporary assertion on regression tests with --bv-eq-slicer=auto.
2018-02-20	Minor fixes and additions for transcendental functions (#1612)	Andrew Reynolds
	Also adds parsing support for PI in smt2 with syntax "real.pi".
2018-02-20	Unrecursified and merged bv::utils::is(Core\|Equality)Term. (#1605)	Aina Niemetz
	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).
2018-02-16	bv::utils::mk(And\|Or) Do not return true if size of vector is 0. (#1613)	Aina Niemetz

2018-02-16	Make regress1 default, only test regress0 on Travis. (#1611)	Aina Niemetz

2018-02-15	Removed bv::utils::mkConjunction (redundant). (#1610)	Aina Niemetz

2018-02-15	Fix corner case for rewrite of mult by pow 2 (#1601)	Andrew Reynolds

2018-02-15	Refactor regressions (#1581)	Andrew Reynolds

2018-02-15	Fix context memory manager unit test (#1609)	Andres Noetzli
	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.
2018-02-14	Quantifiers subdirectories (#1608)	Andrew Reynolds

2018-02-13	Remove unused cd_set_collection.h (#1606)	Andres Noetzli

2018-02-13	Provide a uniform way to serialize node containers to output stream. (#1604)	Aina Niemetz

2018-02-13	Moved (unrecursified) bv::utils::collectVars. (#1602)	Aina Niemetz

2018-02-13	Skip header for determining top contributors list. (#1603)	Aina Niemetz

2018-02-12	Option to use extended rewriter as a preprocessing pass (#1600)	Andrew Reynolds

2018-02-12	Minor improvements to sygus sampler (#1598)	Andrew Reynolds

2018-02-11	Move (unrecursified) bv::utils::numNodes to lazy_bitblaster.cpp. (#1594)	Aina Niemetz
	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.