Age | Commit message (Collapse) | Author | |
---|---|---|---|
2013-12-24 | Better automatic handling of output language setting. | Morgan Deters | |
2013-12-18 | Add missing regression-results directory. | Morgan Deters | |
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-10 | Fix timer statistics to report correct time even on process abort. | 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 | Update copyrights, add missing file-level documentation; fix perms. | Morgan Deters | |
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-20 | Changing the number of bits allocated per field in node values. | Tim King | |
2013-11-14 | Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ ↵ | Morgan Deters | |
Google for the report and patch! | |||
2013-11-11 | Change exit status to be more consistent with other command-line tools: 0 ↵ | Morgan Deters | |
success, nonzero error | |||
2013-11-07 | Flatten libcvc4 build structure; remove some #include interdependences | Morgan Deters | |
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 | Add support for check-sat with argument. | Morgan Deters | |
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-30 | Minor fixes to build system. | Morgan Deters | |
2013-07-29 | Fix numerous compiler warnings on various platforms | Morgan Deters | |
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. |