summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
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
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
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
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
2018-03-23Remove unused code (#1700)Andrew Reynolds
2018-03-23Enable post-condition strenghtening by default for non-syntax restricted inva...Andrew Reynolds
2018-03-21Refactor mkoptions (#1631)Mathias Preiner
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
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
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-17Removes yet more throw specifiers. Updating the documentation as needed. (#1518)Tim King
2018-01-14Removing throw specifiers from OptionsHandler. (#1510)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-09Fix output of --trace=help. (#1500)Aina Niemetz
2018-01-08Removing more miscellaneous throw specifiers. (#1488)Tim King
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-29Cbqi repeat solve literal (#1458)Andrew Reynolds
2017-12-27Disable sygus PBE when sygus stream is enabled (#1451)Andrew Reynolds
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-05Fix output of --show-trace-tags. (#1430)Mathias Preiner
2017-12-03Normalize grammars - 2 (#1420)Haniel Barbosa
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-29Minor improvements and changes to defaults for cbqi bv (#1406)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback