summaryrefslogtreecommitdiff
path: root/test/regress/regress0
AgeCommit message (Collapse)Author
2012-03-22some improvements to the sharing mechanism/interfaceDejan Jovanović
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions. Removing one test case from the integer regress0.
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2012-02-29fixing bug310Dejan Jovanović
* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file * default care graph computation was not sufficient, fixed
2012-02-21Fix for bug303. The problem was with function applications that get ↵Dejan Jovanović
normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced. Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
2012-02-20portfolio mergeMorgan Deters
2012-02-16Last commit accidentally lacked r2778 and r2779 from integer2. I have ↵Tim King
manually brought these changes over. Changed the tests used by test/regress/regress0/arith/integers/Makefile.am to be 15 of the more interesting tests. Did a bit of cleanup on TheoryArith to eliminate a warning and remove dead code.
2012-02-15This commit merges into trunk the branch branches/arithmetic/integers2 from ↵Tim King
r2650 to r2779. - This excludes revision 2777. This revision had some strange performance implications and was delaying the merge. - This includes the new DioSolver. The DioSolver can discover conflicts, produce substitutions, and produce cuts. - The DioSolver can be disabled at command line using --disable-dio-solver. - This includes a number of changes to the arithmetic normal form. - The Integer class features a number of new number theoretic function. - This commit includes a few rather loud warning. I will do my best to take care of them today.
2012-02-07removing the 100 integer benchmarks from regress0, too manyDejan Jovanović
2011-12-10attempt to fix bug 293: if a split on a trivial shared pair is requested ↵Dejan Jovanović
from a theory, such as 1 = 0, it is reasserted to the theory.
2011-11-30disable bug288.smt so that "make check" goes through---pending integers ↵Morgan Deters
merge, see bug #288
2011-11-30Simplified bug288.smt to reflect the problem in integers better.Tim King
2011-11-30Adding a failing UFLIA benchmark corresponding to bug #288.Tim King
2011-11-16* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!Morgan Deters
* Also some better configure script wording
2011-10-29support for proof regressions in other parts of the test treeMorgan Deters
2011-10-29Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵Morgan Deters
SmtEngine::getProof(), a few other things..
2011-10-28proof regressionsMorgan Deters
2011-10-19Merging the branch branches/arithmetic/push-pop-support from r2247 to r2256 ↵Tim King
into trunk. Arithmetic should now be closer to being able to support push and pop.
2011-10-17Sharing workDejan Jovanović
2011-10-04also add test caseMorgan Deters
2011-10-04fixes to context-dependent caching substitutionsMorgan Deters
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30more push/pop infrastructure, some SAT stuffMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in ↵Morgan Deters
preparation of user push/pop in SAT solver
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-07-12forgot to reflect naming change in makefile. fixedMorgan Deters
2011-07-12fix bug 272, array unsoundness, and some array cleanupMorgan Deters
2011-07-11remove some array regressions from "make check" so nightly regressions runMorgan Deters
2011-07-11status of examplesMorgan Deters
2011-07-11new array bugs ?Morgan Deters
2011-07-11mark the new minimized benchmark as unsatMorgan Deters
2011-07-11if running in QF_AX, equalities over terms of uninterpreted sort go to ↵Morgan Deters
arrays, as well as pre-registration of free constants of uninterpreted sort, etc..
2011-07-11minimized exampleMorgan Deters
2011-07-11array benchmarksMorgan Deters
2011-07-11merge from symmetry branchMorgan Deters
2011-07-09minor fixupsMorgan Deters
2011-07-09surprize surprizeDejan Jovanović
2011-07-05missing test caseDejan Jovanović
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-06-30only use theory registration if (1) a theory requests it, or (2) if there's ↵Morgan Deters
more than one "real" theory (not BUILTIN or BOOL) active
2011-05-31This commit contains the code for allowing arbitrary equalities in the ↵Tim King
theory of arithmetic. * This code has been partially tested. (My testing situation is currently not so great.) The code for testing not preregistering equalities can be compile time enabled by setting the boolean turnOffEqualityPreRegister. Don't be shocked by slowdowns or failures. This does pass make regress as well as a fresh checkout does. (The Mac version has issues.) * I need to disable the permanent row removal heuristic by default. We need to discuss why this needs to happen. We should probably detect pure QF_LRA/QF_RDL problems and enable this when this can safely be done. * I have disabled the arithmetic rewrite equality flag. This code needs to be added to the parser. * For all of the above changes, I have annotated the code with the key word BREADCRUMB. * I have renamed ArithUnatePropagator to ArithAtomDatabase.
2011-05-23fixes for "make dist" and "make doc", minor cleanupsMorgan Deters
2011-05-23Merge from arrays2 branch.Morgan Deters
2011-05-13* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolioMorgan Deters
branch) * add Theory::isSharedTermFact() -- it currently always returns false, pending theory combination work * Add "unknown" cardinalities to Cardinality class * Fix run_regression script to handle CRLF line terminators on Macs (where sed is non-GNU) * Convert CRLF line terminators in datatypes regressions to LF
2011-05-06added 10 benchmarks to regress/regress0/datatypes from paperAndrew Reynolds
2011-05-05Merge from nonclausal-simplification-v2 branch:Morgan Deters
* Preprocessing-time, non-clausal, Boolean simplification round to support "quasi-non-linear rewrites" as discussed at last few meetings. * --simplification=none is the default for now, but we'll probably change that to --simplification=incremental. --simplification=batch is also a possibility. See --simplification=help for details. * RecursionBreaker<T> now uses a hash set for the seen trail. * Fixes to TLS stuff to support that. * Fixes to theory and SmtEngine documentation. * Fixes to stream indentation. * Other miscellaneous stuff.
2011-05-02adding some previously-failing "bug" test cases for bitvectorsMorgan Deters
2011-05-02updating bv regressionsDejan Jovanović
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback