summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
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-23Implement changes from yesterday morning's meeting (10/21/2011):Morgan Deters
* OutputChannel::lemma() now returns an unsigned int. This facility isn't functional yet, but the signature is there. For now, it always returns the current user level (which is "correct" from the interface point of view, but not what we want). * Pseudobooleans disabled. This should fix some quantifier benchmarks Andy's been working with on the quantifiers2 branch. * --limit / --time-limit options renamed --rlimit and --tlimit. There may be slowdown from disabling pseudobooleans.
2011-10-21some printing and parser fixes for problems recently uncoveredMorgan 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-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API This will need more work, but it's a start. Also implemented TheoryEngine::properPropagation(). Other minor things.
2011-10-07Some new Datatype public functionality, as per Chris Conway's suggestions on ↵Morgan Deters
the dev mailing list.
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵Morgan Deters
to model gen on booleans; and a little cleanup
2011-10-04also add test caseMorgan Deters
2011-10-04fixes to context-dependent caching substitutionsMorgan Deters
2011-10-04compatibility, bindingsMorgan Deters
2011-10-04compat layer cleanupMorgan 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-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-29some test fixesMorgan Deters
2011-09-21Java binding now working. Some interface types still need some work (e.g. ↵Morgan Deters
iterators aren't functional). Also, output isn't very flexible yet, as I told SWIG to ignore all the operator<<'s.
2011-09-21considerable bindings interface work, some improvements to buildMorgan Deters
2011-09-16some minor fixes to the cvc3 compatibility library and test caseMorgan Deters
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-08-25Fixing the broken unit testsDejan Jovanović
2011-08-17new implementation of lemmas on demandDejan Jovanović
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
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-06-30some things I had laying around in a directory but never got committed; ↵Morgan Deters
minor fix-ups to documentation and some node stuff
2011-06-02minor fix to build system for system testsMorgan Deters
2011-06-02added (temporary) support for ensuring that all ambiguously typed ↵Andrew Reynolds
constructor nodes created internally are given a type ascription
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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback