summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2017-11-23Ho parsing and regressions (#1350)Andrew Reynolds
2017-11-21Cegqi bv remove extract terms preprocess pass (#1376)Andrew Reynolds
2017-11-15Reenable some regressions, minor. (#1369)Andrew Reynolds
2017-11-15Adding garbage collection for Proof objects. (#1294)Tim King
2017-11-14Clean Ceg Instantiators (#1365)Andrew Reynolds
2017-11-13Disable sygus qe preprocessing by default (#1353)Andrew Reynolds
2017-11-13Argument Relevance for Synthesis Conjectures (#1311)Andrew Reynolds
2017-11-09Add modular arithmetic operators. (#1321)Aina Niemetz
2017-11-05Improve rewriting for string contains part 2 (#1300)Andrew Reynolds
2017-11-03Suppport SAT logic (#1310)Andrew Reynolds
2017-11-03Sygus clean main (#1297)Andrew Reynolds
2017-11-01CBQI BV choice expressions (#1296)Andrew Reynolds
2017-10-28Change bvudiv semantics based on input language (#1292)Andres Noetzli
2017-10-27Improve strings rewriter for contains (#1207)Andrew Reynolds
2017-10-25Removing throw specifiers from OutputChannel and subclasses. (#1209)Tim King
2017-10-25CBQI BV: Add handling for missing operators. (#1274)Aina Niemetz
2017-10-23CBQI BV: Add ULT/SLT inverse handling. (#1268)Aina Niemetz
2017-10-23Document sygus programming-by-examples utility (#1260)Andrew Reynolds
2017-10-20Make Sygus conjectures higher-order (#1244)Andrew Reynolds
2017-10-16Fix for issue 1247 (#1257)Clark Barrett
2017-10-16Adds unit test that show Node and TNode work with for each loops. (#1230)Tim King
2017-10-13CBQI BV: Added EXTRACT handling. (#1240)Aina Niemetz
2017-10-12CBQI BV quick heuristics (#1239)Andrew Reynolds
2017-10-12Initial support for solving bit-vector inequalities (#1229)Andrew Reynolds
2017-10-12Sygus logics (#1226)Andrew Reynolds
2017-10-11Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)Aina Niemetz
2017-10-11Add side conditions for UDIV_TOTAL, SHL, CONCAT. (#1224)Mathias Preiner
2017-10-11Adds infrastructure for a rewriting pass in BvInstantiator::processAssertion ...Andrew Reynolds
2017-10-09CBQI BV: Add inverse for more operators. (#1213)Aina Niemetz
2017-10-04Add mkZero, mkOne and mkUmulo to bv utils. (#1200)Aina Niemetz
2017-10-03Add regression from #50 regarding "as" parsing in smt2 (#1188)Andrew Reynolds
2017-10-03Op overload parser (#1162)Andrew Reynolds
2017-10-01Refactor check function in last call effort of non-linear extension. (#1175)Andrew Reynolds
2017-09-30SyGuS streaming solution mode (#1131)Andrew Reynolds
2017-09-29Simplify representation of inversion Skolems for bv cegqi (#1164)Andrew Reynolds
2017-09-29Initial working version of BV word-level instantiation (#1158)Andrew Reynolds
2017-09-28Improve finite model finding for recursive predicates (#1150)Andrew Reynolds
2017-09-25Fix bug related to sort inference + subtypes. (#1125)Andrew Reynolds
2017-09-21Sygus inv templ refactor (#1110)Andrew Reynolds
2017-09-19Fix issue #1074, improve non-fatal error handling (#1075)Andres Noetzli
2017-09-18Fix issue #1105 involving string to int (#1112)Andrew Reynolds
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
2017-09-13Add isConst check for lambda expressions. (#1084)Andrew Reynolds
2017-09-10Ensure that expand definitions is called on all non-variable expressi… (#1070)Andrew Reynolds
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
2017-08-31Answer unknown when uf-ss=no-minimal is combined with cardinality constraints...Andrew Reynolds
2017-08-30Fix model construction for parametric types (#1059)Andrew Reynolds
2017-08-24Test Java API on CIPat Hawks
2017-08-21Change Bugzilla urls to Github issues.Mathias Preiner
2017-08-17Remove unused SubrangeBound(s) classes (#221)Andres Noetzli
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback