summaryrefslogtreecommitdiff
path: root/test/regress
AgeCommit message (Collapse)Author
2013-12-23Proof-checking code; fixups of segfaults and missing functionality in proof ↵Morgan Deters
generation; fix bug 285. * segfaults/assert-fails in proof-generation fixed, including bug 285 * added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present) * proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals) * proofs are *not* yet supported in incremental mode * added --dump-proofs to dump out proofs, like --dump-models * run_regression script now runs with --check-proofs where appropriate * options scripts now support :link-smt for SMT options, like :link for command-line
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-09mv prp to regress1Kshitij Bansal
2013-12-07fix bug 542Kshitij Bansal
2013-12-05disable substring in default modeTianyi Liang
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-11Change exit status to be more consistent with other command-line tools: 0 ↵Morgan Deters
success, nonzero error
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-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-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
2013-07-17Fix bug 516; include some bug testcases.Morgan Deters
2013-07-11Support 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-09Fix for bug 519; don't involve ITESimplifier in model generation.Morgan Deters
2013-06-24Support 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-04Merge branch '1.2.x'Morgan Deters
2013-06-04Fix clang static initialization order issue; fixes bug 512.Morgan Deters
2013-05-22Add regressions for finite model findingAndrew Reynolds
2013-05-21Merge branch '1.2.x'Morgan Deters
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback