| 2018-02-01 |
Andrew Reynolds | Add interface in sygus to get synthesis solution Nodes... |
commit | commitdiff | tree |
| 2018-02-01 |
Andrew Reynolds | Use sygus to synthesize/verify rewrite rules (#1547) |
commit | commitdiff | tree |
| 2018-01-30 |
Andrew Reynolds | Further clean and document datatypes rewriter (#1548) |
commit | commitdiff | tree |
| 2018-01-29 |
Andrew Reynolds | Generalize explanations for PBE sygus strings based... |
commit | commitdiff | tree |
| 2018-01-28 |
Andrew Reynolds | Sort children of all commutative operators for sygus... |
commit | commitdiff | tree |
| 2018-01-27 |
Tim King | Removing an unused variable. Resolves CID 1172257.... |
commit | commitdiff | tree |
| 2018-01-27 |
Tim King | Removing structurally dead code. (#1540) |
commit | commitdiff | tree |
| 2018-01-25 |
Tim King | Commenting out throw specifiers on SmtEngine. These... |
commit | commitdiff | tree |
| 2018-01-25 |
Aina Niemetz | Added unit tests for PLUS, NEG, NOT ICs for CBQI BV... |
commit | commitdiff | tree |
| 2018-01-23 |
Aina Niemetz | Fix MULT handling for CBQI BV. (#1531) |
commit | commitdiff | tree |
| 2018-01-23 |
Tim King | Commenting out throw specifiers for DeltaRationExceptio... |
commit | commitdiff | tree |
| 2018-01-22 |
Aina Niemetz | Add previous concat handling for CBQI BV as heuristic... |
commit | commitdiff | tree |
| 2018-01-22 |
Aina Niemetz | Refactor and fix solveBvLit for CBQI BV. (#1526) |
commit | commitdiff | tree |
| 2018-01-22 |
Andrew Reynolds | Only push/pop around check-sat if it is associated... |
commit | commitdiff | tree |
| 2018-01-17 |
Tim King | Removes yet more throw specifiers. Updating the documen... |
commit | commitdiff | tree |
| 2018-01-16 |
Tim King | Removing more miscellaneous throw specifiers. (#1509) |
commit | commitdiff | tree |
| 2018-01-15 |
Tim King | Removing throw specifiers from Type. (#1511) |
commit | commitdiff | tree |
| 2018-01-14 |
Tim King | Removing throw specifiers from OptionsHandler. (#1510) |
commit | commitdiff | tree |
| 2018-01-14 |
Aina Niemetz | Remove BITVECTOR_SUB from isInvertible(). (#1513) |
commit | commitdiff | tree |
| 2018-01-12 |
Andrew Reynolds | Improvements for CBQI BV (#1504) |
commit | commitdiff | tree |
| 2018-01-10 |
Aina Niemetz | Removed division by constant handling for CBQI BV ... |
commit | commitdiff | tree |
| 2018-01-10 |
Tim King | Removing throw specifiers for TypeRules. (#1501) |
commit | commitdiff | tree |
| 2018-01-10 |
Tim King | Removing throw specifiers from type enumerators. (... |
commit | commitdiff | tree |
| 2018-01-10 |
Tim King | Cleaning up throw specifiers on Exception and subclasse... |
commit | commitdiff | tree |
| 2018-01-10 |
Mathias Preiner | Fix linearization for terms where the solve variable... |
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Reorganized bitvector.h. (#1505) |
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Fix output of --trace=help. (#1500) |
commit | commitdiff | tree |
| 2018-01-09 |
Tim King | Removing throw specifiers from miscellaneous src/expr... |
commit | commitdiff | tree |
| 2018-01-09 |
Tim King | Removing more miscellaneous throw specifiers. (#1488) |
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Add bv util mkConst(unsigned, Integer&). (#1499) |
commit | commitdiff | tree |
| 2018-01-09 |
Tim King | Remove throw specifiers from symbol table. (#1490) |
commit | commitdiff | tree |
| 2018-01-09 |
Aina Niemetz | Added division by constant handling for CBQI BV. (... |
commit | commitdiff | tree |
| 2018-01-08 |
Aina Niemetz | Remove portfolio option from builds. (#1496) |
commit | commitdiff | tree |
| 2018-01-08 |
Tim King | Removes throw specifiers from command.{h,cpp}. (#1485) |
commit | commitdiff | tree |
| 2018-01-08 |
Andrew Reynolds | Improvements to quant+BV/Bool variable elimination... |
commit | commitdiff | tree |
| 2018-01-08 |
Andres Noetzli | Fix broken GMP URL in get-win-dependencies script ... |
commit | commitdiff | tree |
| 2018-01-08 |
Tim King | Remove throw specifiers from datatype. (#1489) |
commit | commitdiff | tree |
| 2018-01-08 |
Tim King | Re-ordering field initialization in QuantInfo to remove... |
commit | commitdiff | tree |
| 2018-01-08 |
Tim King | Removes RationalFromDoubleException. Replaces this... |
commit | commitdiff | tree |
| 2018-01-06 |
Tim King | Removing throw specifiers from src/parser/. (#1486) |
commit | commitdiff | tree |
| 2018-01-06 |
Mathias Preiner | Add special {SGE,SGT,NE}_UDIV1 side conditions for... |
commit | commitdiff | tree |
| 2018-01-06 |
Mathias Preiner | Use simpler EQUAL SCs for LSHR0, LSHR1, ASHR0, AHSR1... |
commit | commitdiff | tree |
| 2018-01-05 |
Mathias Preiner | Add UGT/SGT side conditions for AND/OR + other fixes... |
commit | commitdiff | tree |
| 2018-01-05 |
Aina Niemetz | Fix side condition handling for PLUS, XOR, SIGN_EXTEND... |
commit | commitdiff | tree |
| 2018-01-05 |
Mathias Preiner | Add side conditions for inequalities of SHL. (#1472) |
commit | commitdiff | tree |
| 2018-01-04 |
Andrew Reynolds | Improvements for CBQI (#1478) |
commit | commitdiff | tree |
| 2018-01-04 |
Tim King | Removing miscellaneous throw specifiers. (#1474) |
commit | commitdiff | tree |
| 2018-01-04 |
Tim King | Removing throw specifiers from context/. (#1473) |
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Add side conditions for UGT/SGT over BITVECTOR_UREM... |
commit | commitdiff | tree |
| 2018-01-03 |
Mathias Preiner | Add UGT/SGT side conditions for LSHR. (#1469) |
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Add side conditions for inequalities over BITVECTOR_MU... |
commit | commitdiff | tree |
| 2018-01-03 |
Andrew Reynolds | Global negate (#1466) |
commit | commitdiff | tree |
| 2018-01-03 |
Mathias Preiner | Add side conditions for inequalities of ASHR. (#1461) |
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Add side conditions for inequalities over BITVECTOR_UDI... |
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Simplify side condition for SGE over UREM (index =... |
commit | commitdiff | tree |
| 2018-01-03 |
Mathias Preiner | Fix handling for UGT/SGT. (#1467) |
commit | commitdiff | tree |
| 2018-01-02 |
Andrew Reynolds | Rewrites for BitVector multiplication (#1465) |
commit | commitdiff | tree |
| 2018-01-02 |
Mathias Preiner | Add side conditions for inequalities of LSHR. (#1462) |
commit | commitdiff | tree |
| 2018-01-02 |
Andrew Reynolds | Improve rewriter for string equality (#1427) |
commit | commitdiff | tree |
| 2017-12-30 |
Aina Niemetz | Add side conditions for inequalities over BITVECTOR_URE... |
commit | commitdiff | tree |
| 2017-12-30 |
Aina Niemetz | Fix RNG for seed = 0. (#1459) |
commit | commitdiff | tree |
| 2017-12-30 |
Andrew Reynolds | Cbqi repeat solve literal (#1458) |
commit | commitdiff | tree |
| 2017-12-29 |
Mathias Preiner | Add side conditions for inequalities of AND/OR. (#1457) |
commit | commitdiff | tree |
| 2017-12-29 |
Aina Niemetz | Fix unit tests for ineq for CBQI BV. (#1456) |
commit | commitdiff | tree |
| 2017-12-29 |
Aina Niemetz | Add unit tests for side conditions for inequality for... |
commit | commitdiff | tree |
| 2017-12-28 |
Andrew Reynolds | Fixes for cbqi (#1453) |
commit | commitdiff | tree |
| 2017-12-28 |
Arjun Viswanathan | Rel smt parser (#1446) |
commit | commitdiff | tree |
| 2017-12-28 |
Aina Niemetz | Minor refactor for inequality handling for CBQI BV... |
commit | commitdiff | tree |
| 2017-12-27 |
Andrew Reynolds | Disable sygus PBE when sygus stream is enabled (#1451) |
commit | commitdiff | tree |
| 2017-12-21 |
Andrew Reynolds | Fixes for cbqi-bv (#1449) |
commit | commitdiff | tree |
| 2017-12-21 |
Aina Niemetz | Add explicit disequality handling when generating side... |
commit | commitdiff | tree |
| 2017-12-21 |
Mathias Preiner | Add rewriting rule for ranking benchmarks. (#1448) |
commit | commitdiff | tree |
| 2017-12-20 |
Andrew Reynolds | Transcendental functions check model (#1443) |
commit | commitdiff | tree |
| 2017-12-19 |
Aina Niemetz | Fix travis write errors. (#1445) |
commit | commitdiff | tree |
| 2017-12-16 |
Aina Niemetz | Enable side condition handling for shifts introduced... |
commit | commitdiff | tree |
| 2017-12-14 |
Aina Niemetz | Add missing side conditions for SHL, LSHR, ASHR for... |
commit | commitdiff | tree |
| 2017-12-12 |
Mathias Preiner | Add SIGTERM handler. (#1440) |
commit | commitdiff | tree |
| 2017-12-11 |
justinxu421 | Add new infrastructure for preprocessing passes (#1053) |
commit | commitdiff | tree |
| 2017-12-10 |
Andrew Reynolds | Fix issue 1433. (#1435) |
commit | commitdiff | tree |
| 2017-12-10 |
Andres Noetzli | Fix issue with mkConst/getConst of TypeConstant (#1439) |
commit | commitdiff | tree |
| 2017-12-09 |
Mathias Preiner | Add CEGQI BV linearization of additions and equalities... |
commit | commitdiff | tree |
| 2017-12-08 |
Aina Niemetz | Fixed side conditions for CBQI BV, added unit tests... |
commit | commitdiff | tree |
| 2017-12-08 |
Andrew Reynolds | Document and clean datatypes rewriter (#1437) |
commit | commitdiff | tree |
| 2017-12-08 |
Andrew Reynolds | Make collect model info return a Bool (#1421) |
commit | commitdiff | tree |
| 2017-12-07 |
Andrew Reynolds | Fixes related to SyGuS + real arithmetic (#1432) |
commit | commitdiff | tree |
| 2017-12-07 |
Andrew Reynolds | Add command for define-fun-rec and add to API (#1412) |
commit | commitdiff | tree |
| 2017-12-06 |
Aina Niemetz | Fixed time stats for MiniSat solve time. (#1431) |
commit | commitdiff | tree |
| 2017-12-06 |
Andres Noetzli | Remove CDChunkList (#1414) |
commit | commitdiff | tree |
| 2017-12-05 |
Mathias Preiner | Fix output of --show-trace-tags. (#1430) |
commit | commitdiff | tree |
| 2017-12-05 |
Haniel Barbosa | Adding SyGuS grammars for rationals. (#1426) |
commit | commitdiff | tree |
| 2017-12-04 |
Andrew Reynolds | Eliminate expand definitions from Sygus (#1425) |
commit | commitdiff | tree |
| 2017-12-04 |
Andrew Reynolds | Fix strings rewriter for strip constant endpoint revers... |
commit | commitdiff | tree |
| 2017-12-04 |
Mathias Preiner | Fix side condition for BITVECTOR_MULT. (#1422) |
commit | commitdiff | tree |
| 2017-12-03 |
Haniel Barbosa | Normalize grammars - 2 (#1420) |
commit | commitdiff | tree |
| 2017-12-02 |
Andrew Reynolds | Minor improvements to inst match generator (#1415) |
commit | commitdiff | tree |
| 2017-12-02 |
Andrew Reynolds | Improve rewriter for string replace (#1416) |
commit | commitdiff | tree |
| 2017-12-01 |
Andres Noetzli | Fix reset-assertions (#1413) |
commit | commitdiff | tree |
| 2017-12-01 |
Andrew Reynolds | Minor additions for sygus (#1419) |
commit | commitdiff | tree |
| 2017-12-01 |
Andrew Reynolds | Refactor and generalize PBE strategies (#1410) |
commit | commitdiff | tree |
| 2017-12-01 |
Andres Noetzli | Fix build when Valgrind instrumentation enabled |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog