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

Age	Commit message (Collapse)	Author
2018-05-03	Merge branch 'master' into fix_warnsfix_warns	Andres Noetzli

2018-05-03	Interleave quantifiers checks with ground theory checks at LAST_CALL (#1834)	Andrew Reynolds

2018-05-03	Option to interleave tangent plane inferences (#1833)	Andrew Reynolds

2018-05-03	Link cegis unif with the enumeration manager (#1859)	Andrew Reynolds

2018-05-03	Make CegisUnif default to Cegis when no unif used (#1836)	Haniel Barbosa

2018-05-02	Fix cvc printer for nullary constructors (#1856)	Andrew Reynolds

2018-05-02	Remove (dummy) SMT1 printer (#1854)	Andres Noetzli

2018-05-02	Support HORN logic string (#1849)	Andrew Reynolds

2018-05-02	Initial support for string standard in smt lib 2.6 (#1848)	Andrew Reynolds

2018-05-02	Fix warnings in proof code	Andres Noetzli
	Adds missing `override`s and removes the `inline` keyword from a function that is defined in the source file.
2018-05-01	Cegis unif enumerator manager (#1837)	Andrew Reynolds

2018-05-01	Improve tangent planes for transcendental functions (#1832)	Andrew Reynolds

2018-04-30	Refactor real2int (#1813)	Haniel Barbosa
	This commit refactors the real2int preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass.
2018-04-30	Remove dead code in bv-to-bool preprocessing pass (#1828)	Andres Noetzli
	Fixes Coverity issue 1468436. As Coverity correctly detects, kind::BITVECTOR_XOR is dealt with in an if-statement before the switch statement on kind. This is because kind::XOR is binary while kind::BITVECTOR_XOR is n-ary (as a comment in the code correctly indicates).
2018-04-30	Remove subsort symmetry breaking (#1807)	Andrew Reynolds

2018-04-30	Fix 1156 (#1830)	Andrew Reynolds

2018-04-30	Disable unsat-cores/proofs for slow regression (#1835)	Andres Noetzli

2018-04-29	Allow multiple functions in sygus unif approaches (#1831)	Andrew Reynolds

2018-04-29	Make factoring inference more aggressive (#1825)	Andrew Reynolds

2018-04-29	Refactor nonlinear check (#1814)	Andrew Reynolds

2018-04-29	Improvements to simple transcendental function check model. (#1823)	Andrew Reynolds

2018-04-28	Initial implementation of SygusUnifRL (#1829)	Haniel Barbosa

2018-04-27	Make construct solution behavior specific to SygusIO (#1827)	Andrew Reynolds

2018-04-27	Print function for equality status. (#1826)	Andrew Reynolds

2018-04-27	Simplify tangent plane direction (#1824)	Andrew Reynolds

2018-04-27	New module for synthesizing functions in a data-driven SyGuS approach (#1819)	Haniel Barbosa

2018-04-27	Core improvements to extended rewriter (#1820)	Andrew Reynolds

2018-04-26	Fix subgoal generation context (#1816)	Andrew Reynolds

2018-04-25	Refactor array-proofs and uf-proofs (#1655)	yoni206
	This commit unifies duplicate code blocks from array_proof.cpp and uf_proof.cpp into theory_proof.cpp.
2018-04-25	Equality resolution in the extended rewriter (#1811)	Andrew Reynolds

2018-04-25	Refactor bv-to-bool and bool-to-bv preprocessing passes (#1788)	yoni206

2018-04-25	Move candidate rewrite code to own file (#1804)	Andrew Reynolds

2018-04-25	Add benchmark requiring subgoal generation with induction. Disable option. ↵	Andrew Reynolds
	(#1806)
2018-04-25	Remove nl solve subs option. (#1803)	Andrew Reynolds

2018-04-25	Fix issue with multi-triggers that include variable triggers (#1810)	Andrew Reynolds

2018-04-23	Draft smt comp 2018 for quantifiers and non-linear (#1808)	Andrew Reynolds

2018-04-21	Improve sygus sampling for strings (#1802)	Andrew Reynolds

2018-04-20	Remove unused cache.h (#1795)	Andres Noetzli

2018-04-20	Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are ↵	yoni206
	enabled (#1801) Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable). This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.
2018-04-20	Reenable filtering based on ordering in sygus sampler (#1784)	Andrew Reynolds

2018-04-20	Draft of casc j9 scripts (#1800)	Andrew Reynolds

2018-04-20	Allow metadata lines in test files to have leading spaces (#1799)	yoni206
	Currently, lines like `;EXPECT: sat` instead of `; EXPECT: sat` cause problems. This PR fixes it.
2018-04-20	Symmetry detection module (#1749)	PaulMeng

2018-04-20	Restrict test summary to first-level subfolders (#1797)	Andres Noetzli

2018-04-19	Adding config/tap-driver.sh to .gitignore (#1792)	yoni206
	#1791 removed config/tap-driver.sh from the repo, as ./autogen.sh adds it automatically. The current PR prevents this file from being added to the untracked changes list when doing git status.
2018-04-19	Refactor pbRewrites preprocessing pass (#1767)	Andres Noetzli
	This commit refactors the pbRewrites preprocessing pass into the new style. This commit is essentially just a code move and adds a regression test for the preprocessing pass. It also makes use of the AssertionPipeline::replace function to do proper dependency tracking.
2018-04-19	Remove tap-driver.sh (#1791)	Andres Noetzli
	The autogen.sh script that we use causes the tap-driver.sh script to be copied from automake installed on the system, so we do not have to include it in our git repository. This also avoids ping-ponging between different versions of the tap-driver script if different people have different versions and commit them as part of their PRs.
2018-04-16	Add timeout (option) to regression script (#1786)	Andres Noetzli
	This commit adds the option to run regressions with a timeout using the `TEST_TIMEOUT` environment variable. The default timeout is set to 10 minutes. This should make it less likely that our nightly builds hang and makes it easier to sort out slow tests. Default timeout tested with regression level 2 on a debug build with proofs.
2018-04-16	Disable slow regression test (#1787)	Andres Noetzli

2018-04-16	Disable check proofs/unsat cores for two regs (#1785)	Andres Noetzli
	Disabling proof checking/unsat core checking for the two benchmarks in question, reduces the time to run regressions significantly. After the change, regression level 2 takes 7m30s to run on my machine and regression level 1 takes just below 3m (16 threads). Individually, the tests take over 7m each when checking proofs/unsat cores, so they add significant overhead.