summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
2013-12-18Add missing regression-results directory.Morgan Deters
2013-12-16Fix for bug 544.Morgan Deters
2013-12-13Fix stack size on in-tree regressions.Morgan Deters
2013-12-13cleanupMorgan Deters
2013-12-13Some minor cleanup.Morgan Deters
2013-12-10Fix timer statistics to report correct time even on process abort.Morgan Deters
2013-12-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-05disable substring in default modeTianyi Liang
2013-12-05Update copyrights, add missing file-level documentation; fix perms.Morgan Deters
2013-12-05Fix Boolean terms w.r.t. parametric datatypes (e.g., (Pair Bool Bool) now ↵Morgan Deters
works).
2013-12-04Remove a regression for which the portfolio takes forever (see bug 542).Morgan Deters
2013-12-04Don't put define-funs in model output; bug 411 testcase no longer relevant.Morgan Deters
2013-12-03adds LB strategyTianyi Liang
2013-12-02Add test case for (previously resolved) bug 528.Morgan Deters
2013-12-02Support 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-25Substantial 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-20Changing the number of bits allocated per field in node values.Tim King
2013-11-14Some patches to CVC3 compatibility layer tests; Thanks to Adam Buchbinder @ ↵Morgan Deters
Google for the report and patch!
2013-11-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
2013-11-07Flatten libcvc4 build structure; remove some #include interdependencesMorgan Deters
2013-11-05fixed proof regression script and added a new uf test caselianah
2013-10-24Fix for bug515Clark Barrett
2013-10-21add a string test caseTianyi Liang
2013-10-20adds regular expression rangeTianyi Liang
2013-10-16adds fmf for stringsTianyi Liang
2013-10-15bug fix: string cache cleaningTianyi Liang
2013-10-14add another regexp testTianyi Liang
2013-10-14Adds Regular Expression support.Tianyi Liang
2013-10-11Adds regular expression support, it is actually CFL because of variables.Tianyi Liang
2013-10-01adds partial function substr. the use of this function should be guarded, ↵Tianyi Liang
especially for disequalities
2013-09-30replace with a new method for disequality, move to QF_STianyi Liang
2013-09-27Some fixes to recent strings commits.Morgan Deters
2013-09-27adds communication with arith engineTianyi Liang
2013-09-27removes unsound cases, adds unrollingTianyi Liang
2013-09-27adds model generation for strings, and a hacked way in arith engine for modelsTianyi Liang
2013-09-18Support a personal build configuration and make rules.Morgan Deters
2013-09-13Move some regress benchmarks around that took too long, other test cleanup.Morgan Deters
2013-09-13Documentation fixes, some code typo fixes, file perms, other minor things.Morgan Deters
2013-09-11Theory of strings.Tianyi Liang
Signed-off-by: Morgan Deters <mdeters@cs.nyu.edu>
2013-09-09Another minor fix for datatypes to repair my previous commit.Andrew Reynolds
2013-09-09Add support for check-sat with argument.Morgan Deters
2013-09-09Support empty (and 1-ary) tuples and records.Morgan Deters
2013-08-26Merge branch '1.2.x'Kshitij Bansal
2013-08-26bug 374 fix: assert litVal=desiredVal only for leaf nodes1.2.xKshitij Bansal
2013-08-26Bug 374 benchmarksKshitij Bansal
2013-07-30Minor fixes to build system.Morgan Deters
2013-07-29Fix numerous compiler warnings on various platformsMorgan Deters
2013-07-24Regressions now checking models on unknown too. But quantifiers don't have ↵Morgan Deters
to be simplified by check-model in that case.
2013-07-19enable bug521 regression testsMorgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback