| 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 |
| 2017-12-01 |
Andres Noetzli | Add debugging tools for ContextMemoryManager (#1407) |
commit | commitdiff | tree |
| 2017-11-30 |
Aina Niemetz | Add Gaussian Elimination as a preprocessing pass for... |
commit | commitdiff | tree |
| 2017-11-30 |
Andrew Reynolds | Fixes for issue 1404 (#1409) |
commit | commitdiff | tree |
| 2017-11-30 |
Andrew Reynolds | Remove remaining references to QuantArith (#1408) |
commit | commitdiff | tree |
| 2017-11-30 |
Andrew Reynolds | Minor improvements and changes to defaults for cbqi... |
commit | commitdiff | tree |
| 2017-11-29 |
Andrew Reynolds | Improve caching in term formula removal (#1398) |
commit | commitdiff | tree |
| 2017-11-29 |
Tim King | Adding missing break statements. CID 1362756. (#1394) |
commit | commitdiff | tree |
| 2017-11-29 |
Tim King | Simplifying the conditions in checkLetBinding to avoid... |
commit | commitdiff | tree |
| 2017-11-29 |
Mathias Preiner | Add Cryptominisat script and patches to source file... |
commit | commitdiff | tree |
| 2017-11-29 |
Andrew Reynolds | Improve the rewriter for SINE. (#1221) |
commit | commitdiff | tree |
| 2017-11-28 |
Andrew Reynolds | Improve rewrite for string substr (#1337) |
commit | commitdiff | tree |
| 2017-11-28 |
Andrew Reynolds | Improve trigger filter instances (#1402) |
commit | commitdiff | tree |
| 2017-11-28 |
Tim King | Removing throw specifiers from internal Printer hierarc... |
commit | commitdiff | tree |
| 2017-11-28 |
Andrew Reynolds | Fix models for --solve-real-as-int. (#1371) |
commit | commitdiff | tree |
| 2017-11-25 |
Andrew Reynolds | Fixes for higher-order (#1405) |
commit | commitdiff | tree |
| 2017-11-25 |
Andrew Reynolds | (Refactor) Instantiate utility (#1387) |
commit | commitdiff | tree |
| 2017-11-24 |
Andrew Reynolds | Implement tangent and secant planes for transcendental... |
commit | commitdiff | tree |
| 2017-11-24 |
Andrew Reynolds | Ho parsing and regressions (#1350) |
commit | commitdiff | tree |
| 2017-11-23 |
Haniel Barbosa | Converting defined functions and let expressions from... |
commit | commitdiff | tree |
| 2017-11-22 |
Andrew Reynolds | Sygus Lambda Grammars (#1390) |
commit | commitdiff | tree |
| 2017-11-22 |
Andrew Reynolds | Transcendental tangent planes utilities (#1288) |
commit | commitdiff | tree |
| 2017-11-21 |
Haniel Barbosa | Adding infrastructure for normalizing SyGuS grammars... |
commit | commitdiff | tree |
| 2017-11-21 |
Andrew Reynolds | Cegqi bv remove extract terms preprocess pass (#1376) |
commit | commitdiff | tree |
| 2017-11-20 |
Tim King | Initializes members of QuantInfo. Resolves CID 1362929... |
commit | commitdiff | tree |
| 2017-11-20 |
Tim King | Removing an unused variable from SygusInput. Resolves... |
commit | commitdiff | tree |
| 2017-11-19 |
Andrew Reynolds | Ho instantiation (#1204) |
commit | commitdiff | tree |
| 2017-11-19 |
Tim King | Names the Effort enum of QuantConflictFind class. ... |
commit | commitdiff | tree |
| 2017-11-17 |
Andrew Reynolds | (Refactor) Document and clean single invocation partiti... |
commit | commitdiff | tree |
| 2017-11-17 |
Aina Niemetz | Add random number generator. (#1370) |
commit | commitdiff | tree |
| next |
projects / cvc5.git / shortlog