summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-08-18more tests, configuration for UFMorgan Deters
2010-08-17Merge from "cc" branch:Morgan Deters
CongruenceClosure implementation; CongruenceClosure white-box test. New UF theory implementation based on new CC module. This one supports predicates. The two UF implementations exist in parallel (they can be selected at runtime via the new command line option "--uf"). Added type infrastructure for TUPLE. Fixes to unit tests that failed in 16-August-2010 regressions. Needed to instantiate TheoryEngine with an Options structure, and explicitly call ->shutdown() on it before destruction (like the SMTEngine does). Fixed test makefiles to (1) perform all tests even in the presence of failures, (2) give proper summaries of subdirectory tests (e.g. regress0/uf and regress0/precedence) Other minor changes.
2010-08-17Add "no trash" CDMap elements, so that CDMap elements can themselvesMorgan Deters
be allocated in context memory. CDMap black-box test extended.
2010-08-17Change TheoryEngine to use pointers to theories instead ofMorgan Deters
calling them directly. In tests this doesn't appear to lead to slowdown.
2010-08-16add zlib checks to configure (new minisat requires it?)Morgan Deters
2010-08-16Fixing failures in minisatDejan Jovanović
2010-08-15(no commit message)Dejan Jovanović
2010-08-15(no commit message)Dejan Jovanović
2010-08-13renaming minisat .C to .cc Dejan Jovanović
2010-08-13Adding the changes to the original copyDejan Jovanović
2010-08-13Importing MiniSat2 070721 into trunkChristopher L. Conway
2010-08-13Removing newer version of MiniSat for Dejan's preferred importChristopher L. Conway
2010-08-13Importing MiniSat2 2.2.0 into trunkChristopher L. Conway
2010-08-13Removing old version of MiniSat for proper vendor importChristopher L. Conway
2010-07-29Adding configuration_private.h to allow inlining of configuration checksChristopher L. Conway
2010-07-29fix TheoryEngineWhite, add documentation; related to bug #188Morgan Deters
2010-07-28Adding TypeCheckingException to throws clause in SMT parsersChristopher L. Conway
2010-07-28Forcing a type check on Node construction in debug mode (Fixes: #188)Christopher L. Conway
NOTE: mkNode/mkExpr/parsing functions can now throw type checking exceptions
2010-07-28fixed theory engine white test for new (old) theoryOf() behavior (re: bug 188)Morgan Deters
2010-07-27Moving EQ->IFF handling from TheoryEngine to parser/type checkerChristopher L. Conway
2010-07-27Adding optional 'check' parameter to getType() methodsChristopher L. Conway
2010-07-22incorporate a fix from smtcomp2010 version for handling CNF of (= bool ↵Morgan Deters
bool); also make theoryOf(= t1 t2) return theoryOf(t1.getType()), rather than theoryOf(t1), as the latter gives different results for (= (geq x1 x2) (leq x2 x1)) and (= a (leq x2 x1)), which is strange and causes problems. should discuss at tuesday meeting. resolves bug 187.
2010-07-22Added test file for fuzzsmt bug, bug187.smt2.Tim King
2010-07-10add >, <=, and >= comparisons for Exprs and NodesMorgan Deters
2010-07-10Fix for the type in sat propagation.Dejan Jovanović
2010-07-09the tableaux optimizationDejan Jovanović
2010-07-08Moving cluster-qf_lra-full to scripts projectChristopher L. Conway
2010-07-08Moving cluster-qf_lra-benchmark to scripts projectChristopher L. Conway
2010-07-08Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQChristopher L. Conway
2010-07-08Fixing Array type in SMT v1.2Christopher L. Conway
2010-07-08I am adding my smt-crunch scripts to source control. Others may find them ↵Tim King
useful. To use them, log into goedel, sudo su acsys-user, and run ./cluster-script PATH_TO_EXECUTABLE. Be sure to change the email address in the script before using it. Improvements are of course welcome.
2010-07-08context work to support cdmaps with elements allocated in context memoryMorgan Deters
2010-07-08Updates to the post_mortem.py script.Tim King
2010-07-07Shared term manager tested and workingClark Barrett
It is currently tracking all asserted equalities for simplicity. Might want to check if this is a performance hit
2010-07-07Making plus-mult.cvc test a bit more torturous (as enabled by r744)Christopher L. Conway
2010-07-07Fixes arith rewriter to allow for division by a constant. It previously only ↵Tim King
allowed for a constant divided by a constant.
2010-07-07Fixing test plus-mult.cvc by making it linear (Fixes: #184)Christopher L. Conway
2010-07-07minor changes to cdmap/cdset interface for detection of duplicate insertsMorgan Deters
2010-07-07chris and i committed the same fix; reverting the (now duplicated) fixMorgan Deters
2010-07-07Updated headersClark Barrett
2010-07-07Added shared term manager. Basic mechanism for identifying shared terms isClark Barrett
working. Still need to implement theory-specific shared term propagation.
2010-07-07Disabling failing testsChristopher L. Conway
2010-07-07add exit status to regression that was failingMorgan Deters
2010-07-07some build system changes reverted after the CLN build system work a few ↵Morgan Deters
days ago, these are now fixed: competition configurations build with -O9 (as they used to); they are static-binary by default and shared libs are not built; also the default autoconf compiler flags "-g -O2" is removed from builds
2010-07-07competition submission should be fully staticMorgan Deters
2010-07-07fixed submission targetMorgan Deters
2010-07-07things for competition upload: new "make submission" targetMorgan Deters
2010-07-07Adding tests for precedence of arithmetic in CVC inputsChristopher L. Conway
2010-07-07Adding config.reconfig to .gitignoreChristopher L. Conway
2010-07-06Fixed exit status for competition mode.Tim King
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback