Age | Commit message (Collapse) | Author | |
---|---|---|---|
2010-03-12 | Fixing unnecessary construction of NOT nodes when generating conflict ↵ | Dejan Jovanović | |
clauses and: * adding the smallest test case (eq_diamond23.smt) that memouts in 50s * adding the initial attributes black box test | |||
2010-03-11 | Changing const TNode& to TNode in the CNF conversion + a new small benchmark ↵ | Dejan Jovanović | |
that fail on "x != x" | |||
2010-03-11 | Added some hand generated UF tests. Unfortunartely all of them work. Also ↵ | Tim King | |
fixed some cleanup stuff. | |||
2010-03-11 | Fix for the main bug that was bugging me -- Bug 49. The assertions queue in ↵ | Dejan Jovanović | |
the theories didn't get cleared on SatSolver backtracking so there were unasserted literals being returned as part of some conflicts. Sat solver now explicitely calls in the theory engine after it backtracks in order to clear the queues (clearAssertionQueues). Also, changed the let.smt as it used to exibit "single literal conflict" problem. The sat solve can not except conflicts similar to (x != x), these should be rewritten to false during pre-processing. Adding 3 more small problems from the library that we can solve now to the regressions. | |||
2010-03-10 | Adding preliminary let/flet support to SMT parser (Bug #51) | Christopher L. Conway | |
2010-03-09 | Adding support for "distinct" builtin in SMT parser | Christopher L. Conway | |
2010-03-09 | Adding the smallest of test cases from the smtlib. | Dejan Jovanović | |
2010-03-09 | removing makefile.in | Dejan Jovanović | |
2010-03-09 | one more simple test for uf | Dejan Jovanović | |
2010-03-09 | (no commit message) | Dejan Jovanović | |
2010-03-08 | adding simple-uf to the regressions, and the code that apparently solves it | Dejan Jovanović | |
2010-02-22 | resolve bug 32; public-facing interface functions in expr package must set ↵ | Morgan Deters | |
current NodeManager | |||
2010-02-11 | Adding precedence regressions | Christopher L. Conway | |
2010-02-09 | Changes to the CNF conversion and the SAT solver. All regression pass now, ↵ | Dejan Jovanović | |
and we're ready for nightly testing. We should not add regression tests that test future behaviour, as the builds will nag for all failing regressions. Thus, I've separated the multi-query regressions into multiple regressions until the cnf/context/sat is able to handle it. Also, fixed a typo in the CVC parser. | |||
2010-02-08 | Fixing the test case, it had a unary or. The cnf converter should be adapted ↵ | Dejan Jovanović | |
to handle cases like this. | |||
2010-02-06 | Preliminary support for types in parser | Christopher L. Conway | |
2010-02-04 | fix run_regression script | Morgan Deters | |
2010-02-04 | assign expected-status to regressions | Morgan Deters | |
2010-02-04 | build system for multi-level regressions | Morgan Deters | |
2010-02-04 | Moved regressions into various levels based on running time. | Tim King | |
2010-02-04 | test infrastructure updated for multiple-level regressions | Morgan Deters | |
2010-02-03 | Adding functions/predicates to SMT grammar | Christopher L. Conway | |
2010-02-03 | simple ITE parsing | Dejan Jovanović | |
2010-02-03 | Enabled more regress tests. Takes 26s on my machine to run a make -k check ↵ | Tim King | |
in debug mode. All regress tests currently pass. | |||
2010-02-03 | some more tests for the context. | Dejan Jovanović | |
2010-02-01 | Added this test back to avoid make check problems. | Tim King | |
2010-01-29 | fixed CNF conversion, and more modular; CNF conversion command line option; ↵ | Morgan Deters | |
various cleanups; renamed numChildren() to getNumChildren() and added it to NodeBuilder interface; fancier, non-exponential CNF conversion with variable introduction is still buggy (?) | |||
2010-01-28 | Removing Makefile.in's | Christopher L. Conway | |
2010-01-27 | support "make check" in src/ subdirs for unit-testing of just that module; ↵ | Morgan Deters | |
also support synonyms for "make check" globally | |||
2010-01-27 | test framework fixes; bug 13 closed | Morgan Deters | |
2010-01-26 | Added test/regress/boolean.cvc | Tim King | |
2010-01-26 | fixes to build structure, util classes, lots of fixes to Node and ↵ | Morgan Deters | |
NodeBuilder. outstanding SEGVs fixed | |||
2010-01-23 | Added pure PL regression tests. Mostly CNF | Tim King | |
2010-01-22 | Added regression test | Tim King | |
2009-12-17 | build system cleanup; test system separation into white-box, black-box, and ↵ | Morgan Deters | |
public tests | |||
2009-12-17 | support nonstandard, unconfigured builds (e.g., "./configure debug" followed ↵ | Morgan Deters | |
by "make production ASSERTIONS=1") | |||
2009-12-16 | Fixes to the build system: | Morgan Deters | |
Makefile.am files - remove obsolete INCLUDES, incorporate into AM_CPPFLAGS Makefile files in src/ - support "make" under src/ (current build profile) configure.ac - updates to fix warnings config/antlr.m4 - updates to fix warnings autogen.sh - updates to generate warnings from autotools; also support Macs src/include/cvc4_config.h - guard with #ifdef total reimplementation of NodeBuilder ExprValue => NodeValue context_mm.{h,cpp} - fixed numerous compile errors | |||
2009-12-11 | build fixes, configuration simplifications | Morgan Deters | |
2009-12-08 | check in automake/libtool/autoconf-generated files; add better file not ↵ | Morgan Deters | |
found handling | |||
2009-12-08 | broken formula | Morgan Deters | |
2009-12-07 | fixing a few broken build-related items, adding test cases | Morgan Deters | |
2009-11-20 | fixes to build/test system | Morgan Deters | |