Age | Commit message (Collapse) | Author | |
---|---|---|---|
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-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. | |||
2018-04-16 | Make 256 the default cardinality for strings (#1783) | Andrew Reynolds | |
2018-04-16 | RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782) | Andres Noetzli | |
2018-04-16 | Skolemize candidate rewrite rule checks (#1777) | Andrew Reynolds | |
2018-04-15 | Make strings fmf apply to all but internally generated Skolems (#1780) | Andrew Reynolds | |
2018-04-15 | Fix type error with regexp (#1778) | Andrew Reynolds | |