| 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 |
Andrew Reynolds | Statically eliminate redundant sygus constructors ...
|
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-02 |
Andrew Reynolds | Fix remaining synthesis solution regressions (#1557)
|
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-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 DeltaRationExceptions...
|
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 documentatio...
|
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-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 from type enumerators. (...
|
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 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 |
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 |
Andrew Reynolds | Improvements to quant+BV/Bool variable elimination...
|
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 |
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 |
Mathias Preiner | Add side conditions for inequalities of SHL. (#1472)
|
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_MULT...
|
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_UDIV...
|
commit | commitdiff | tree |
| 2018-01-03 |
Aina Niemetz | Simplify side condition for SGE over UREM (index =...
|
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_UREM...
|
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 |
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)
https://github.com/travis-ci/travis-ci/issues...
|
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-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-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-05 |
Mathias Preiner | Fix output of --show-trace-tags. (#1430)
|
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 reverse...
|
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 | 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-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 |
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 hierarchy...
|
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 |
| next |
projects / cvc5.git / search