summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Expand)Author
2018-02-15Fix corner case for rewrite of mult by pow 2 (#1601)Andrew Reynolds
2018-02-15Refactor regressions (#1581)Andrew Reynolds
2018-02-15Fix context memory manager unit test (#1609)Andres Noetzli
2018-02-14Quantifiers subdirectories (#1608)Andrew Reynolds
2018-02-09Renaming CHECK to CVC4_CHECK. This avoids name collisions with other popular ...Tim King
2018-02-08Updated copyrightAina Niemetz
2018-02-08Remove invalid regression test (#1579)Andres Noetzli
2018-02-07Adds a new CHECK macro that abort()s on failure. (#1532)Tim King
2018-02-07Add remaining transcendental functions (#1551)Andrew Reynolds
2018-02-06Fix two multiply-by-constant corner cases for bv rewriter (#1562)Andrew Reynolds
2018-02-06Fix rewrite for string replace (#1537)Andrew Reynolds
2018-02-05Statically eliminate redundant sygus constructors (#1560)Andrew Reynolds
2018-02-02Fix remaining synthesis solution regressions (#1557)Andrew Reynolds
2018-02-02Option to check solutions produced by SyGuS solver (#1553)Haniel Barbosa
2018-01-24Added unit tests for PLUS, NEG, NOT ICs for CBQI BV. (#1534)Aina Niemetz
2018-01-21Refactor and fix solveBvLit for CBQI BV. (#1526)Aina Niemetz
2018-01-12Improvements for CBQI BV (#1504)Andrew Reynolds
2018-01-09Fix linearization for terms where the solve variable does not occur. (#1506)Mathias Preiner
2018-01-08Improvements to quant+BV/Bool variable elimination (#1495)Andrew Reynolds
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback