summaryrefslogtreecommitdiff
path: root/test
AgeCommit message (Collapse)Author
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-10attempt at a fix for the local regression failure (CLN linking issues on oneiricMorgan Deters
2012-02-07removing the 100 integer benchmarks from regress0, too manyDejan Jovanović
2012-02-06Fixing a bug in the integer unit tests when configured for GMP with ↵Tim King
assertions off.
2012-01-25Adding regress1 test ooo.rf6.smt2.Tim King
2011-12-15Partial fix in arithmetic for propagating shared terms. This partially ↵Tim King
resolves bug 289. Adds failing tests to regress1.
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-12-06LemmaStatus changes, as agreed to during 12/2 meeting.Morgan Deters
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-30Added a failing regression test corresponding to bug 289.Tim King
2011-11-30Adding a failing UFLIA benchmark corresponding to bug #288.Tim King
2011-11-16Addressed many of the concerns raised in the public interface review of CVC4 ↵Morgan Deters
Datatypes (bug #283) by Chris Conway. Thanks, Chris!
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-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-14public tests need to be linked against gmp/cln explicitly---looks like a ↵Morgan Deters
subtle linker change in Ubuntu 11.10 oneiric :-(
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-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..
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback