summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2018-01-05Add UGT/SGT side conditions for AND/OR + other fixes. (#1481)Mathias Preiner
2018-01-03Global negate (#1466)Andrew Reynolds
2018-01-02Add side conditions for inequalities over BITVECTOR_UDIV for CBQI BV. (#1464)Aina Niemetz
2018-01-02Fix handling for UGT/SGT. (#1467)Mathias Preiner
2018-01-02Rewrites for BitVector multiplication (#1465)Andrew Reynolds
2017-12-29Add side conditions for inequalities over BITVECTOR_UREM for CBQI BV. (#1460)Aina Niemetz
2017-12-28Fix unit tests for ineq for CBQI BV. (#1456)Aina Niemetz
2017-12-28Add unit tests for side conditions for inequality for CBQI BV. (#1455)Aina Niemetz
2017-12-27Rel smt parser (#1446)Arjun Viswanathan
2017-12-20Fixes for cbqi-bv (#1449)Andrew Reynolds
2017-12-20Add explicit disequality handling when generating side condition for CBQI BV....Aina Niemetz
2017-12-20Transcendental functions check model (#1443)Andrew Reynolds
2017-12-13Add missing side conditions for SHL, LSHR, ASHR for CBQI BV. (#1441)Aina Niemetz
2017-12-10Fix issue 1433. (#1435)Andrew Reynolds
2017-12-08Add CEGQI BV linearization of additions and equalities over additions. (#1417)Mathias Preiner
2017-12-08Fixed side conditions for CBQI BV, added unit tests. (#1434)Aina Niemetz
2017-12-07Fixes related to SyGuS + real arithmetic (#1432)Andrew Reynolds
2017-12-06Remove CDChunkList (#1414)Andres Noetzli
2017-12-04Fix strings rewriter for strip constant endpoint reverse direction (#1424)Andrew Reynolds
2017-12-01Fix reset-assertions (#1413)Andres Noetzli
2017-12-01Refactor and generalize PBE strategies (#1410)Andrew Reynolds
2017-11-30Add debugging tools for ContextMemoryManager (#1407)Andres Noetzli
2017-11-30Add Gaussian Elimination as a preprocessing pass for BV. (#1342)Aina Niemetz
2017-11-29Improve caching in term formula removal (#1398)Andrew Reynolds
2017-11-28Improve rewrite for string substr (#1337)Andrew Reynolds
2017-11-27Fix models for --solve-real-as-int. (#1371)Andrew Reynolds
2017-11-25Fixes for higher-order (#1405)Andrew Reynolds
2017-11-24Implement tangent and secant planes for transcendental functions (#1401)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback