summaryrefslogtreecommitdiff
path: root/src/smt
AgeCommit message (Expand)Author
2018-04-19Refactor pbRewrites preprocessing pass (#1767)Andres Noetzli
2018-04-16RemoveTermFormulas: Remove ContainsTermITEVisitor (#1782)Andres Noetzli
2018-04-13allowing --bool-to-bv without quantifiers (#1771)yoni206
2018-04-12Fixes for free variables in assertions (#1762)Andrew Reynolds
2018-04-10Refactored BVGauss preprocessing pass. (#1766)Aina Niemetz
2018-04-10 Improve accuracy of stats for sygus sampler (#1755)Andrew Reynolds
2018-04-09Fix dumping of benchmark in SmtEngine::checkSatisfiability(). (#1764)Aina Niemetz
2018-04-05Add more general SignExtendUltConst rewriting. (#1385)Mathias Preiner
2018-04-03Refactor IntToBV preprocessing pass (#1716)Andres Noetzli
2018-04-03Option to turn arbitrary input into sygus (#1704)Andrew Reynolds
2018-04-02Remove references to nyu (#1721)Clark Barrett
2018-03-25Check model only when sat (#1694)Andrew Reynolds
2018-03-13SmtEngine::getModel() is now public. (#1665)Aina Niemetz
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
2018-03-02Fixed comments in smt_engine.h.Aina Niemetz
2018-02-28SmtEngine::getAssignment now returns a vector of assignments. (#1628)Aina Niemetz
2018-02-14Quantifiers subdirectories (#1608)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-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-24Commenting out throw specifiers on SmtEngine. These can later be refined into...Tim King
2018-01-21Only push/pop around check-sat if it is associated with an assertion (#1525)Andrew Reynolds
2018-01-15Removing more miscellaneous throw specifiers. (#1509)Tim King
2018-01-09Cleaning up throw specifiers on Exception and subclasses. (#1475)Tim King
2018-01-09Reorganized bitvector.h. (#1505)Aina Niemetz
2018-01-08Removes throw specifiers from command.{h,cpp}. (#1485)Tim King
2018-01-03Global negate (#1466)Andrew Reynolds
2017-12-27Disable sygus PBE when sygus stream is enabled (#1451)Andrew Reynolds
2017-12-20Fixes for cbqi-bv (#1449)Andrew Reynolds
2017-12-10Add new infrastructure for preprocessing passes (#1053)justinxu421
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-06Add command for define-fun-rec and add to API (#1412)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
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-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-17(Refactor) Document and clean single invocation partition. (#1364)Andrew Reynolds
2017-11-17Add random number generator. (#1370)Aina Niemetz
2017-11-16(Refactor) Arithmetic monomial sum (#1381)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-14Cleaning up exporting vectors within commands. Resolves CID 1172285 and 11722...Tim King
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-09Higher-order prep (#1338)Andrew Reynolds
2017-11-07Allow FORALL in quantifier elimination command (#1322)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback