Age | Commit message (Collapse) | Author | |
---|---|---|---|
2010-08-18 | more tests, configuration for UF | Morgan Deters | |
2010-08-17 | Merge 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-17 | Add "no trash" CDMap elements, so that CDMap elements can themselves | Morgan Deters | |
be allocated in context memory. CDMap black-box test extended. | |||
2010-08-17 | Change TheoryEngine to use pointers to theories instead of | Morgan Deters | |
calling them directly. In tests this doesn't appear to lead to slowdown. | |||
2010-08-16 | add zlib checks to configure (new minisat requires it?) | Morgan Deters | |
2010-08-16 | Fixing failures in minisat | Dejan Jovanović | |
2010-08-15 | (no commit message) | Dejan Jovanović | |
2010-08-15 | (no commit message) | Dejan Jovanović | |
2010-08-13 | renaming minisat .C to .cc | Dejan Jovanović | |
2010-08-13 | Adding the changes to the original copy | Dejan Jovanović | |
2010-08-13 | Importing MiniSat2 070721 into trunk | Christopher L. Conway | |
2010-08-13 | Removing newer version of MiniSat for Dejan's preferred import | Christopher L. Conway | |
2010-08-13 | Importing MiniSat2 2.2.0 into trunk | Christopher L. Conway | |
2010-08-13 | Removing old version of MiniSat for proper vendor import | Christopher L. Conway | |
2010-07-29 | Adding configuration_private.h to allow inlining of configuration checks | Christopher L. Conway | |
2010-07-29 | fix TheoryEngineWhite, add documentation; related to bug #188 | Morgan Deters | |
2010-07-28 | Adding TypeCheckingException to throws clause in SMT parsers | Christopher L. Conway | |
2010-07-28 | Forcing 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-28 | fixed theory engine white test for new (old) theoryOf() behavior (re: bug 188) | Morgan Deters | |
2010-07-27 | Moving EQ->IFF handling from TheoryEngine to parser/type checker | Christopher L. Conway | |
2010-07-27 | Adding optional 'check' parameter to getType() methods | Christopher L. Conway | |
2010-07-22 | incorporate 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-22 | Added test file for fuzzsmt bug, bug187.smt2. | Tim King | |
2010-07-10 | add >, <=, and >= comparisons for Exprs and Nodes | Morgan Deters | |
2010-07-10 | Fix for the type in sat propagation. | Dejan Jovanović | |
2010-07-09 | the tableaux optimization | Dejan Jovanović | |
2010-07-08 | Moving cluster-qf_lra-full to scripts project | Christopher L. Conway | |
2010-07-08 | Moving cluster-qf_lra-benchmark to scripts project | Christopher L. Conway | |
2010-07-08 | Adding missing operators in SMT2 parser: UMINUS, DIVISION, GEQ, LEQ | Christopher L. Conway | |
2010-07-08 | Fixing Array type in SMT v1.2 | Christopher L. Conway | |
2010-07-08 | I 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-08 | context work to support cdmaps with elements allocated in context memory | Morgan Deters | |
2010-07-08 | Updates to the post_mortem.py script. | Tim King | |
2010-07-07 | Shared term manager tested and working | Clark Barrett | |
It is currently tracking all asserted equalities for simplicity. Might want to check if this is a performance hit | |||
2010-07-07 | Making plus-mult.cvc test a bit more torturous (as enabled by r744) | Christopher L. Conway | |
2010-07-07 | Fixes arith rewriter to allow for division by a constant. It previously only ↵ | Tim King | |
allowed for a constant divided by a constant. | |||
2010-07-07 | Fixing test plus-mult.cvc by making it linear (Fixes: #184) | Christopher L. Conway | |
2010-07-07 | minor changes to cdmap/cdset interface for detection of duplicate inserts | Morgan Deters | |
2010-07-07 | chris and i committed the same fix; reverting the (now duplicated) fix | Morgan Deters | |
2010-07-07 | Updated headers | Clark Barrett | |
2010-07-07 | Added shared term manager. Basic mechanism for identifying shared terms is | Clark Barrett | |
working. Still need to implement theory-specific shared term propagation. | |||
2010-07-07 | Disabling failing tests | Christopher L. Conway | |
2010-07-07 | add exit status to regression that was failing | Morgan Deters | |
2010-07-07 | some 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-07 | competition submission should be fully static | Morgan Deters | |
2010-07-07 | fixed submission target | Morgan Deters | |
2010-07-07 | things for competition upload: new "make submission" target | Morgan Deters | |
2010-07-07 | Adding tests for precedence of arithmetic in CVC inputs | Christopher L. Conway | |
2010-07-07 | Adding config.reconfig to .gitignore | Christopher L. Conway | |
2010-07-06 | Fixed exit status for competition mode. | Tim King | |