summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Collapse)Author
2018-05-28Builtin evaluation functions for sygus (#1991)Andrew Reynolds
2018-05-25Reenable repair const (#1983)Andrew Reynolds
2018-05-23Add notions of evaluated kinds in TheoryModel (#1947)Andrew Reynolds
2018-05-23Generalize check-model in NonLinearExtension for quadratic equations (#1892)Andrew Reynolds
2018-05-22Repair constants using symbolic constructors (#1960)Andrew Reynolds
2018-05-21Add SymFPU licensing information. (#1952)Mathias Preiner
2018-05-18changing default (#1944)Haniel Barbosa
2018-05-17Option to force return values of Bool functions to be constant in CegisUnif ↵Haniel Barbosa
(#1930)
2018-05-17Cegis-specific infrastructure (#1933)Andrew Reynolds
2018-05-14Add regressions, change defaults. (#1911)Andrew Reynolds
2018-05-10Sygus repair constants (#1812)Andrew Reynolds
2018-05-09Better option names for PBE (#1891)Andrew Reynolds
2018-05-09Add the symmetry breaker module (#1847)PaulMeng
2018-05-04Make --output-lang consistent with --lang (#1877)Andres Noetzli
2018-05-03Option to interleave tangent plane inferences (#1833)Andrew Reynolds
2018-05-02Remove (dummy) SMT1 printer (#1854)Andres Noetzli
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-05-01Improve tangent planes for transcendental functions (#1832)Andrew Reynolds
2018-04-30Refactor 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-30Remove subsort symmetry breaking (#1807)Andrew Reynolds
2018-04-27New module for synthesizing functions in a data-driven SyGuS approach (#1819)Haniel Barbosa
2018-04-25Remove nl solve subs option. (#1803)Andrew Reynolds
2018-04-20 Reenable filtering based on ordering in sygus sampler (#1784)Andrew Reynolds
2018-04-20Symmetry detection module (#1749)PaulMeng
2018-04-16Make 256 the default cardinality for strings (#1783)Andrew Reynolds
2018-04-09Remove 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-03Option 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-02Improvements to extended rewriter for Booleans and ITE (#1705)Andrew Reynolds
2018-03-27Fix for --sygus-rr-synth (#1723)Andrew Reynolds
2018-03-26Synth-check and accelerate options for sygus-rr (#1691)Andrew Reynolds
2018-03-26Abort when sygus-verify finds unsoundness. (#1717)Andrew Reynolds
2018-03-24Remove 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-23Remove unused code (#1700)Andrew Reynolds
2018-03-23Enable post-condition strenghtening by default for non-syntax restricted ↵Andrew Reynolds
invariant synthesis (#1703)
2018-03-21Refactor 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-20Add support for CaDiCaL as eager BV SAT solver. (#1675)Mathias Preiner
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-02-27Option to not use partial function semantics for arithmetic div by zero (#1620)Andrew Reynolds
2018-02-27Improvements to sygus sampling (#1621)Andrew Reynolds
2018-02-12Option to use extended rewriter as a preprocessing pass (#1600)Andrew Reynolds
2018-02-08Minor improvements to sygus sampling. (#1577)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-04Sample based on sygus grammar by default (#1558)Andrew Reynolds
2018-02-02Option to use sampling for CEGIS (#1555)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-02-01Use sygus to synthesize/verify rewrite rules (#1547)Andrew Reynolds
2018-01-22Add 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-21Refactor 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-17Removes yet more throw specifiers. Updating the documentation as needed. (#1518)Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback