Age | Commit message (Collapse) | Author | |
---|---|---|---|
2012-02-15 | This 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-10 | attempt at a fix for the local regression failure (CLN linking issues on oneiric | Morgan Deters | |
2012-02-07 | removing the 100 integer benchmarks from regress0, too many | Dejan Jovanović | |
2012-02-06 | Fixing a bug in the integer unit tests when configured for GMP with ↵ | Tim King | |
assertions off. | |||
2012-01-25 | Adding regress1 test ooo.rf6.smt2. | Tim King | |
2011-12-15 | Partial fix in arithmetic for propagating shared terms. This partially ↵ | Tim King | |
resolves bug 289. Adds failing tests to regress1. | |||
2011-12-10 | attempt 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-06 | LemmaStatus changes, as agreed to during 12/2 meeting. | Morgan Deters | |
2011-11-30 | disable bug288.smt so that "make check" goes through---pending integers ↵ | Morgan Deters | |
merge, see bug #288 | |||
2011-11-30 | Simplified bug288.smt to reflect the problem in integers better. | Tim King | |
2011-11-30 | Added a failing regression test corresponding to bug 289. | Tim King | |
2011-11-30 | Adding a failing UFLIA benchmark corresponding to bug #288. | Tim King | |
2011-11-16 | Addressed 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-15 | Bindings work (ocaml bindings are now sort of working); also minor cleanup | Morgan Deters | |
2011-11-14 | public tests need to be linked against gmp/cln explicitly---looks like a ↵ | Morgan Deters | |
subtle linker change in Ubuntu 11.10 oneiric :-( | |||
2011-10-29 | support for proof regressions in other parts of the test tree | Morgan Deters | |
2011-10-29 | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF command, ↵ | Morgan Deters | |
SmtEngine::getProof(), a few other things.. | |||
2011-10-28 | proof regressions | Morgan Deters | |
2011-10-23 | Implement 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-21 | some printing and parser fixes for problems recently uncovered | Morgan Deters | |
2011-10-19 | Merging 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-17 | Sharing work | Dejan Jovanović | |
2011-10-13 | Interruption, 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-07 | Some new Datatype public functionality, as per Chris Conway's suggestions on ↵ | Morgan Deters | |
the dev mailing list. | |||
2011-10-05 | ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵ | Morgan Deters | |
to model gen on booleans; and a little cleanup | |||
2011-10-04 | also add test case | Morgan Deters | |
2011-10-04 | fixes to context-dependent caching substitutions | Morgan Deters | |
2011-10-04 | compatibility, bindings | Morgan Deters | |
2011-10-04 | compat layer cleanup | Morgan Deters | |
2011-10-03 | user push/pop support in minisat and simplification; also bindings work | Morgan Deters | |
2011-09-30 | more push/pop infrastructure, some SAT stuff | Morgan Deters | |
2011-09-30 | fixes to incremental simplification, cnf routines, other stuff in ↵ | Morgan Deters | |
preparation of user push/pop in SAT solver | |||
2011-09-29 | Some 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-29 | some test fixes | Morgan Deters | |
2011-09-21 | Java 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-21 | considerable bindings interface work, some improvements to build | Morgan Deters | |
2011-09-16 | some minor fixes to the cvc3 compatibility library and test case | Morgan Deters | |
2011-09-15 | additional stuff for sharing, | Dejan Jovanović | |
2011-09-02 | Merge 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-02 | Partial merge of integers work; this is simple B&B and some pseudoboolean | Morgan Deters | |
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks. | |||
2011-08-25 | Fixing the broken unit tests | Dejan Jovanović | |
2011-08-17 | new implementation of lemmas on demand | Dejan Jovanović | |
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637> | |||
2011-07-12 | forgot to reflect naming change in makefile. fixed | Morgan Deters | |
2011-07-12 | fix bug 272, array unsoundness, and some array cleanup | Morgan Deters | |
2011-07-11 | remove some array regressions from "make check" so nightly regressions run | Morgan Deters | |
2011-07-11 | status of examples | Morgan Deters | |
2011-07-11 | new array bugs ? | Morgan Deters | |
2011-07-11 | mark the new minimized benchmark as unsat | Morgan Deters | |
2011-07-11 | if 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.. |