summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2010-09-16Bug fix to CVC4::theory::arith::VarList as well as some superficial changes. ↵Tim King
test/regress/regress0/arith/arith.03.cvc now passes and is turned on by default. Tiny documentation fix for the arithmetic normal form.
2010-09-14* added test/regress/regress0/arith for easy arithmetic regress tests.Tim King
2010-09-14ensure uf/congruence closure debugging stuff isn't called in production buildsMorgan Deters
2010-09-13make Node iterators more STL-friendly, resolves bug #196Morgan Deters
2010-09-13build system consistency in target names for unit test targetsMorgan Deters
2010-09-13statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is givenMorgan Deters
2010-09-13link TAGS file into builds/ directory, when built. Resolves bug #195Morgan Deters
2010-09-13* New normal form for arithmetic is in place.Tim King
* src/theory/arith/normal_form.{h,cpp} contains the description for the new normal form as well as utilities for dealing with the normal form. * src/theory/arith/next_arith_rewriter.{h,cpp} contains the new rewriter. The new rewriter implements preRewrite() and postRewrite() for arithmetic. * src/theory/arith/arith_rewriter.{h,cpp} have been removed. * TheoryArith::rewrite() has been removed. * Arithmetic with the new normal form outperforms the trunk where the branch occurred (-r797) on 46% of the examples in QF_LRA. (33% have no noticeable difference.) Some important optimizations are stilling pending to the code for handling the new normal form. (Bug 196.)
2010-09-02"Leftist NodeBuilders" are now supported.Morgan Deters
That is, "nb << a << b << c << OR << d << AND" turns into (AND (OR a b c) d) The rule is: pushing a kind onto a NodeBuilder with a nonzero number of child Nodes in it, the action "collapses" it. If a kind is already associated to the NodeBuilder, it is an error. Thus: NodeBuilder<> nb(AND); nb << AND; and NodeBuilder<> nb; nb << AND << OR; are both errors (if assertions are on). In reality, though, the implementation is trickier, as the collapsing is done lazily on the following push. This complicates things a bit, but by placing an Assert(false), I found that we aren't depending on the old behavior (at least for any unit tests or regressions in the source tree). The Assert(false) is now removed and leftist NodeBuilders are in business. Fixes bug 101.
2010-09-02recategorize eq_diamond14 as a regress2 test (instead of regress0)Morgan Deters
2010-09-02fix an error in TimerStatMorgan Deters
2010-09-02neglected build system update from r848 (last commit)Morgan Deters
2010-09-02* add TimerStat statistic typeMorgan Deters
* add Stats black-box unit test * new make target: "make units" now runs unit tests only * revised make target: "make regress" now runs regressions only * configure.ac: pull in librt for clock_gettime()
2010-09-01"make check" now places binaries in the proper place before doing the ↵Morgan Deters
checks; this closes bug 46 finally, though the major annoyances related to this bug already had been fixed long ago
2010-09-01reflect in build strings that -gmp is now the default and -cln is an optionMorgan Deters
2010-09-01added documentation, closes bug 97Morgan Deters
2010-08-24Making GMP default, CLN opt-in with --with-clnChristopher L. Conway
2010-08-20updating the minisat restart parameters after running some experimentsDejan Jovanović
2010-08-20turn off extra-checking (which does extra theory-rewriter checking); it was ↵Morgan Deters
enabled by mistake in the last commit
2010-08-19UF theory bug fixes, code cleanup, and extra debugging output.Morgan Deters
Enabled new UF theory by default. Added some UF regressions. Some work on the whole equality-over-bool-removed-in-favor-of-IFF thing. (Congruence closure module and other things have to handle IFF as a special case of equality, etc..) Added pre-rewriting to TheoryBool which rewrites: * (IFF true x) => x * (IFF false x) => (NOT x) * (IFF x true) => x * (IFF x false) => (NOT x) * (IFF x x) => true * (IFF x (NOT x)) => false * (IFF (NOT x) x) => false * (ITE true x y) => x * (ITE false x y) => y * (ITE cond x x) => x Added post-rewriting that does all of the above, plus normalize IFF and ITE: * (IFF x y) => (IFF y x), if y < x * (ITE (NOT cond) x y) => (ITE cond y x) (Note: ITEs survive the removal-of-ITEs pass only if they are Boolean-valued.) A little more debugging output from CNF stream, context pushes/pops, ITE removal. Some more documentation. Fixed some typos.
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback