Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-12-16 | Fix for bug 544. | Morgan Deters | |
2013-12-13 | Fix stack size on in-tree regressions. | Morgan Deters | |
2013-12-13 | cleanup | Morgan Deters | |
2013-12-13 | Some minor cleanup. | Morgan Deters | |
2013-12-09 | mv prp to regress1 | Kshitij Bansal | |
2013-12-07 | fix bug 542 | Kshitij Bansal | |
2013-12-05 | disable substring in default mode | Tianyi Liang | |
2013-12-05 | Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now ↵ | Morgan Deters | |
works). | |||
2013-12-04 | Remove a regression for which the portfolio takes forever (see bug 542). | Morgan Deters | |
2013-12-04 | Don't put define-funs in model output; bug 411 testcase no longer relevant. | Morgan Deters | |
2013-12-03 | adds LB strategy | Tianyi Liang | |
2013-12-02 | Add test case for (previously resolved) bug 528. | Morgan Deters | |
2013-12-02 | Support for parametric datatype subtyping, so that e.g. (Pair Int Int) is a ↵ | Morgan Deters | |
subtype of (Pair Real Real). Resolves bug #541. | |||
2013-11-25 | Substantial Changes: | Tim King | |
-ITE Simplification -- Moved the utilities in src/theory/ite_simplifier.{h,cpp} to ite_utilities. -- Separated simpWithCare from simpITE. -- Disabled ite simplification on repeat simplification by default. Currently, ite simplification cannot help unless we internally make new constant leaf ites equal to constants. -- simplifyWithCare() is now only run on QF_AUFBV by default. Speeds up nec benchmarks dramatically. -- Added a new compress ites pass that is only run on QF_LIA by default. This targets the perverse structure of ites generated during ite simplification on nec benchmarks. -- After ite simplification, if the ite simplifier was used many times and the NodeManager's node pool is large enough, this garbage collects: zombies from the NodeManager repeatedly, the ite simplification caches, and the theory rewrite caches. - TheoryEngine -- Added TheoryEngine::donePPSimpITE() which orchestrates a number of ite simplifications above. -- Switched UnconstrainedSimplifier to a pointer. - RemoveITEs -- Added a heuristic for checking whether or not a node contains term ites and if not, not bothering to invoke the rest of RemoveITE::run(). This safely changes the type of the cache used on misses of run. This cache can be cleared in the future. Currently disabled pending additional testing. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. - Theory Bool Rewriter -- Added additional simplifications for boolean ites. Minor Changes: - TheoryModel -- Removed vestigial copy of the ITESimplifier. - AttributeManager -- Fixed a garbage collection bug when deleting the node table caused the NodeManager to reclaimZombies() which caused memory corruption by deleting from the attributeManager. - TypeChecker -- added a neverIsConst() rule to the typechecker. Operators that cannot be used in constructing constant expressions by computeIsConst() can now avoid caching on Node::isConst() calls. -NodeManager -- Added additional functions for reclaiming zombies. -- Exposed the size of the node pool for heuristics that worry about memory consumption. - NaryBuilder -- Added convenience classes for constructing associative and commutative n-ary operators. -- Added a pass that turns associative and commutative n-ary operators into binary operators. (Mostly for printing expressions for strict parsers.) | |||
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 ↵ | Morgan Deters | |
success, nonzero error | |||
2013-11-05 | fixed proof regression script and added a new uf test case | lianah | |
2013-10-24 | Fix for bug515 | Clark Barrett | |
2013-10-21 | add a string test case | Tianyi Liang | |
2013-10-20 | adds regular expression range | Tianyi Liang | |
2013-10-16 | adds fmf for strings | Tianyi Liang | |
2013-10-15 | bug fix: string cache cleaning | Tianyi Liang | |
2013-10-14 | add another regexp test | Tianyi Liang | |
2013-10-14 | Adds Regular Expression support. | Tianyi Liang | |
2013-10-11 | Adds regular expression support, it is actually CFL because of variables. | Tianyi Liang | |
2013-10-01 | adds partial function substr. the use of this function should be guarded, ↵ | Tianyi Liang | |
especially for disequalities | |||
2013-09-30 | replace with a new method for disequality, move to QF_S | Tianyi Liang | |
2013-09-27 | Some fixes to recent strings commits. | Morgan Deters | |
2013-09-27 | adds communication with arith engine | Tianyi Liang | |
2013-09-27 | removes unsound cases, adds unrolling | Tianyi Liang | |
2013-09-27 | adds model generation for strings, and a hacked way in arith engine for models | Tianyi Liang | |
2013-09-18 | Support a personal build configuration and make rules. | Morgan Deters | |
2013-09-13 | Move some regress benchmarks around that took too long, other test cleanup. | Morgan Deters | |
2013-09-13 | Documentation fixes, some code typo fixes, file perms, other minor things. | Morgan Deters | |
2013-09-11 | Theory of strings. | Tianyi Liang | |
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu> | |||
2013-09-09 | Another minor fix for datatypes to repair my previous commit. | Andrew Reynolds | |
2013-09-09 | Support empty (and 1-ary) tuples and records. | Morgan Deters | |
2013-08-26 | Merge branch '1.2.x' | Kshitij Bansal | |
2013-08-26 | bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.x | Kshitij Bansal | |
2013-08-26 | Bug 374 benchmarks | Kshitij Bansal | |
2013-07-24 | Regressions now checking models on unknown too. But quantifiers don't have ↵ | Morgan Deters | |
to be simplified by check-model in that case. | |||
2013-07-19 | enable bug521 regression tests | Morgan Deters | |
2013-07-17 | Fix bug 516; include some bug testcases. | Morgan Deters | |
2013-07-11 | Support for TPTP's TFF0 (with arithmetic) | Morgan Deters | |
This commit reverses an "SZS ontology compliance hack" that was done for CASC-24 this year, and adds a TPTP pretty-printer which is capable of outputting results in the TPTP way (rather than the SMT way). This commit includes minor changes to the Expr package to add obvious missing functionality, and to fix the way expressions with builtin operators are made. These changes are truly a _fix_, the implementation had not been properly aligned with the design vision for some corner cases. | |||
2013-07-09 | Fix for bug 519; don't involve ITESimplifier in model generation. | Morgan Deters | |
2013-06-24 | Support for abs, to_int, is_int, divisible in SMT-LIB; also --rewrite-divk ↵ | Morgan Deters | |
allows linearization of div,mod,/ by a constant. | |||
2013-06-04 | Merge branch '1.2.x' | Morgan Deters | |
2013-06-04 | Fix clang static initialization order issue; fixes bug 512. | Morgan Deters | |
2013-05-22 | Add regressions for finite model finding | Andrew Reynolds | |
2013-05-21 | Merge branch '1.2.x' | Morgan Deters | |
2013-05-21 | Fix bug 512: an assertion failure only appearing with clang on Mac OS, due ↵ | Morgan Deters | |
to improper ITE removal in quantifier instantiations. |