Age | Commit message (Collapse) | Author | |
---|---|---|---|
2018-05-28 | Builtin evaluation functions for sygus (#1991) | Andrew Reynolds | |
2018-05-25 | Reenable repair const (#1983) | Andrew Reynolds | |
2018-05-23 | Add notions of evaluated kinds in TheoryModel (#1947) | Andrew Reynolds | |
2018-05-23 | Generalize check-model in NonLinearExtension for quadratic equations (#1892) | Andrew Reynolds | |
2018-05-22 | Repair constants using symbolic constructors (#1960) | Andrew Reynolds | |
2018-05-21 | Add SymFPU licensing information. (#1952) | Mathias Preiner | |
2018-05-18 | changing default (#1944) | Haniel Barbosa | |
2018-05-17 | Option to force return values of Bool functions to be constant in CegisUnif ↵ | Haniel Barbosa | |
(#1930) | |||
2018-05-17 | Cegis-specific infrastructure (#1933) | Andrew Reynolds | |
2018-05-14 | Add regressions, change defaults. (#1911) | Andrew Reynolds | |
2018-05-10 | Sygus repair constants (#1812) | Andrew Reynolds | |
2018-05-09 | Better option names for PBE (#1891) | Andrew Reynolds | |
2018-05-09 | Add the symmetry breaker module (#1847) | PaulMeng | |
2018-05-04 | Make --output-lang consistent with --lang (#1877) | Andres Noetzli | |
2018-05-03 | Option to interleave tangent plane inferences (#1833) | Andrew Reynolds | |
2018-05-02 | Remove (dummy) SMT1 printer (#1854) | Andres Noetzli | |
2018-05-02 | Initial support for string standard in smt lib 2.6 (#1848) | 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 subsort symmetry breaking (#1807) | Andrew Reynolds | |
2018-04-27 | New module for synthesizing functions in a data-driven SyGuS approach (#1819) | Haniel Barbosa | |
2018-04-25 | Remove nl solve subs option. (#1803) | Andrew Reynolds | |
2018-04-20 | Reenable filtering based on ordering in sygus sampler (#1784) | Andrew Reynolds | |
2018-04-20 | Symmetry detection module (#1749) | PaulMeng | |
2018-04-16 | Make 256 the default cardinality for strings (#1783) | Andrew Reynolds | |
2018-04-09 | Remove unused arith options (#1758) | Andres Noetzli | |
Commit 629824db3911ab11ae286e4b14151a537602ba5a added options when introducing the pseudo boolean processor that were never used. This commit removes them. | |||
2018-04-03 | Option to turn arbitrary input into sygus (#1704) | Andrew Reynolds | |
Preprocessing pass that turns an arbitrary (e.g. smt2) input into a sygus conjecture, which is helpful for Horn clause solving. This includes improvements to the robustness of the sygus solver. | |||
2018-04-02 | Improvements to extended rewriter for Booleans and ITE (#1705) | Andrew Reynolds | |
2018-03-27 | Fix for --sygus-rr-synth (#1723) | Andrew Reynolds | |
2018-03-26 | Synth-check and accelerate options for sygus-rr (#1691) | Andrew Reynolds | |
2018-03-26 | Abort when sygus-verify finds unsoundness. (#1717) | Andrew Reynolds | |
2018-03-24 | Remove doc/libcvc4.3 from options/Makefile.am. (#1696) | Mathias Preiner | |
This commit fixes an issue with calling make clean && make. The final doc/libcvc4.3 is now generated during ./autogen.sh and should not be deleted with make clean. | |||
2018-03-23 | Remove unused code (#1700) | Andrew Reynolds | |
2018-03-23 | Enable post-condition strenghtening by default for non-syntax restricted ↵ | Andrew Reynolds | |
invariant synthesis (#1703) | |||
2018-03-21 | Refactor mkoptions (#1631) | Mathias Preiner | |
This commit refactors code generation for options. It uses a new configuration format for defining options (*.toml) and a new Python script mkoptions.py to generate the source code and option documentation. The option behavior did not change for most of the options, except that for bool --enable-/--disable- long options enable/disable was removed. E.g. --enable-miplib-trick and --disable-miplib-trick got changed to --miplib-trick and --no-miplib-trick. This commit fixes also an issues with set-option/get-option via the SMT2 interface. Before long options were only accessible if the name included the =ARG part. | |||
2018-03-20 | Add support for CaDiCaL as eager BV SAT solver. (#1675) | Mathias Preiner | |
2018-03-09 | Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653) | Aina Niemetz | |
2018-03-05 | Enable -Wsuggest-override by default. (#1643) | Mathias Preiner | |
Adds missing override keywords. | |||
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-12 | Option to use extended rewriter as a preprocessing pass (#1600) | Andrew Reynolds | |
2018-02-08 | Minor improvements to sygus sampling. (#1577) | Andrew Reynolds | |
2018-02-05 | Statically eliminate redundant sygus constructors (#1560) | Andrew Reynolds | |
2018-02-04 | Sample based on sygus grammar by default (#1558) | Andrew Reynolds | |
2018-02-02 | Option to use sampling for CEGIS (#1555) | Andrew Reynolds | |
2018-02-02 | Option to check solutions produced by SyGuS solver (#1553) | Haniel Barbosa | |
2018-02-01 | Use sygus to synthesize/verify rewrite rules (#1547) | Andrew Reynolds | |
2018-01-22 | Add previous concat handling for CBQI BV as heuristic for EQ. (#1528) | Aina Niemetz | |
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. | |||
2018-01-21 | Refactor and fix solveBvLit for CBQI BV. (#1526) | Aina Niemetz | |
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) | |||
2018-01-17 | Removes yet more throw specifiers. Updating the documentation as needed. (#1518) | Tim King | |