| 2018-02-09 |
Tim King | Renaming CHECK to CVC4_CHECK. This avoids name collisio... |
commit | commitdiff | tree |
| 2018-02-09 |
Tim King | Replacing an incorrect reference to an injected class... |
commit | commitdiff | tree |
| 2018-02-09 |
Andres Noetzli | Replace CMM flag with debug CMM flag, fix leak in debug... |
commit | commitdiff | tree |
| 2018-02-09 |
Tim King | Inlining line_buffered_input to avoid warning about... |
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Clean up bv utils (part one). (#1580) |
commit | commitdiff | tree |
| 2018-02-08 |
Tim King | Adding virtual destructors on classes with virtual... |
commit | commitdiff | tree |
| 2018-02-08 |
Andrew Reynolds | Minor improvements to sygus sampling. (#1577) |
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Updated copyright |
commit | commitdiff | tree |
| 2018-02-08 |
Tim King | Initializing Timer::d_wall_limit (CID 1362899). (#1573) |
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Simplify and cleanup bv::utils::mkConjunction. (#1571) |
commit | commitdiff | tree |
| 2018-02-08 |
Mathias Preiner | Check whether Cryptominisat4/ABC was installed via... |
commit | commitdiff | tree |
| 2018-02-08 |
Andres Noetzli | Remove invalid regression test (#1579) |
commit | commitdiff | tree |
| 2018-02-08 |
Tim King | Removing an unused variable. (#1576) |
commit | commitdiff | tree |
| 2018-02-08 |
Tim King | Fixing more inconsistent usages of override. (#1575) |
commit | commitdiff | tree |
| 2018-02-08 |
Aina Niemetz | Reduce number of Travis builds. (#1578) |
commit | commitdiff | tree |
| 2018-02-08 |
Tim King | Fixing line numbers on type_checker_template.cpp (... |
commit | commitdiff | tree |
| 2018-02-07 |
Mathias Preiner | Cleanup Cryptominisat header. (#1561) |
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Use template for bv::utils::mkOr. (#1570) |
commit | commitdiff | tree |
| 2018-02-07 |
Tim King | Adds a new CHECK macro that abort()s on failure. (... |
commit | commitdiff | tree |
| 2018-02-07 |
Andrew Reynolds | Add remaining transcendental functions (#1551) |
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Use template for bv::utils::mkAnd. (#1569) |
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Renamed bv::utils::isBVGroundTerm to isBvConstTerm... |
commit | commitdiff | tree |
| 2018-02-07 |
Aina Niemetz | Split and document theory_bv_utils. (#1566) |
commit | commitdiff | tree |
| 2018-02-07 |
Mathias Preiner | Use separate shell script for common get-* script parts... |
commit | commitdiff | tree |
| 2018-02-07 |
Tim King | Fixes two memory leaks coming from Transf. (#1564) |
commit | commitdiff | tree |
| 2018-02-06 |
Aina Niemetz | Updated copyright header for bv_inverter.(cpp|h). |
commit | commitdiff | tree |
| 2018-02-06 |
Aina Niemetz | Updated year in update-copyright script. |
commit | commitdiff | tree |
| 2018-02-06 |
Tim King | Resolving warnings from -Winconsistent-missing-override... |
commit | commitdiff | tree |
| 2018-02-06 |
Andrew Reynolds | Fix two multiply-by-constant corner cases for bv rewrit... |
commit | commitdiff | tree |
| 2018-02-06 |
Aina Niemetz | Updated authors list |
commit | commitdiff | tree |
| 2018-02-06 |
Andrew Reynolds | Fix rewrite for string replace (#1537) |
commit | commitdiff | tree |
| 2018-02-06 |
Tim King | Using getOperator() directly instead of using -1. CID... |
commit | commitdiff | tree |
| 2018-02-06 |
Tim King | Aborting on errors in StatisticsRegistry::unregisterSta... |
commit | commitdiff | tree |
| 2018-02-06 |
Andrew Reynolds | Statically eliminate redundant sygus constructors ... |
commit | commitdiff | tree |
| 2018-02-05 |
Tim King | Cleaning up the printing of theory model representative... |
commit | commitdiff | tree |
| 2018-02-05 |
Tim King | Removing references to __gnu_cxx. (#1541) |
commit | commitdiff | tree |
| 2018-02-04 |
Andrew Reynolds | Sample based on sygus grammar by default (#1558) |
commit | commitdiff | tree |
| 2018-02-03 |
Andrew Reynolds | Option to use sampling for CEGIS (#1555) |
commit | commitdiff | tree |
| 2018-02-03 |
Tim King | Restoring ostream format. Resolves a few CIDs 1362780... |
commit | commitdiff | tree |
| 2018-02-02 |
Andrew Reynolds | Fix remaining synthesis solution regressions (#1557) |
commit | commitdiff | tree |
| 2018-02-02 |
Haniel Barbosa | Option to check solutions produced by SyGuS solver... |
commit | commitdiff | tree |
| 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 |
| next |
projects / cvc5.git / shortlog