summaryrefslogtreecommitdiff
path: root/src/options
AgeCommit message (Expand)Author
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
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
2017-11-22Sygus Lambda Grammars (#1390)Andrew Reynolds
2017-11-21Adding infrastructure for normalizing SyGuS grammars (#1397)Haniel Barbosa
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-18Ho instantiation (#1204)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-03Fix bv help message. (#1315)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
2017-10-27Cbqi multiple instantiation (#1289)Andrew Reynolds
2017-10-24Cbqi bv ineq mode (#1273)Andrew Reynolds
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-20SyGuS term size limit (#1262)Andrew Reynolds
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-10Add copyright information. (#1201)Aina Niemetz
2017-10-04Ho quant util (#1119)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback