2012-09-12 |
Morgan Deters | Adding model assertions after SAT responses. |
blob | commitdiff | raw |
2012-09-11 |
Tim King | Partially reverting the changes made in 4308. There... |
blob | commitdiff | raw | diff to current |
2012-09-10 |
Andrew Reynolds | modified getValue to return Expr instead of Node |
blob | commitdiff | raw | diff to current |
2012-09-06 |
Morgan Deters | Remove SmtEngine::getStackLevel(), which exposed implem... |
blob | commitdiff | raw | diff to current |
2012-08-31 |
Andrew Reynolds | merge from fmf-devel branch. more updates to models... |
blob | commitdiff | raw | diff to current |
2012-08-28 |
Morgan Deters | Improved compatibility layer, now supports quantifiers... |
blob | commitdiff | raw | diff to current |
2012-08-27 |
Morgan Deters | fix a destruction-order issue that was (1) causing... |
blob | commitdiff | raw | diff to current |
2012-08-16 |
Morgan Deters | The SmtEngine now ensures that setLogicInternal() is... |
blob | commitdiff | raw | diff to current |
2012-08-08 |
Morgan Deters | Public interface review items: |
blob | commitdiff | raw | diff to current |
2012-08-07 |
Morgan Deters | Fix SmtEngine::setInfo() handling for certain keys... |
blob | commitdiff | raw | diff to current |
2012-08-06 |
Morgan Deters | Support setting :regular-output-channel and :diagnostic... |
blob | commitdiff | raw | diff to current |
2012-08-03 |
Morgan Deters | fix uses of getMetaKind() from outside the expr package... |
blob | commitdiff | raw | diff to current |
2012-07-31 |
Morgan Deters | fixes for portfolio |
blob | commitdiff | raw | diff to current |
2012-07-31 |
Morgan Deters | Options merge. This commit: |
blob | commitdiff | raw | diff to current |
2012-07-17 |
Morgan Deters | SMT-LIBv2 compliance updates: |
blob | commitdiff | raw | diff to current |
2012-07-17 |
Morgan Deters | fix for --produce-models with CVC4 presentation language |
blob | commitdiff | raw | diff to current |
2012-07-16 |
Morgan Deters | Support for having two SmtEngines with the same ExprMan... |
blob | commitdiff | raw | diff to current |
2012-07-12 |
Andrew Reynolds | merged fmf-devel branch, includes support for SMT2... |
blob | commitdiff | raw | diff to current |
2012-07-08 |
Morgan Deters | minor SMT-LIBv2 compliance issues |
blob | commitdiff | raw | diff to current |
2012-07-08 |
Morgan Deters | Bugs resolved by this commit: #314, #322, #359, #364... |
blob | commitdiff | raw | diff to current |
2012-06-18 |
Kshitij Bansal | bugfix, enable only QF_LRA, not other arith |
blob | commitdiff | raw | diff to current |
2012-06-18 |
Kshitij Bansal | QF_LRA, Quantifiers: enable use decision for (only... |
blob | commitdiff | raw | diff to current |
2012-06-17 |
Kshitij Bansal | QF_AUFLIA: enable use decision for (only for) stopping... |
blob | commitdiff | raw | diff to current |
2012-06-17 |
Dejan Jovanović | enabling theoryof=term for quantifiers with sharing |
blob | commitdiff | raw | diff to current |
2012-06-17 |
Clark Barrett | Removed assertion that can fail |
blob | commitdiff | raw | diff to current |
2012-06-16 |
Kshitij Bansal | This is an attempt to fix the bug in the justification... |
blob | commitdiff | raw | diff to current |
2012-06-16 |
Dejan Jovanović | changing theoryOf in shared mode with arrays to move... |
blob | commitdiff | raw | diff to current |
2012-06-16 |
Tim King | Fixing if condition for trivial equalities in arithmeti... |
blob | commitdiff | raw | diff to current |
2012-06-15 |
Clark Barrett | Fixes some assertion failures |
blob | commitdiff | raw | diff to current |
2012-06-15 |
Clark Barrett | Fix for incompleteness bug with decision engine: repeat... |
blob | commitdiff | raw | diff to current |
2012-06-15 |
Kshitij Bansal | one bug fixed |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Kshitij Bansal | WIP |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Kshitij Bansal | add failing regression, move error up |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Clark Barrett | New substitutions implementation - fixes performance... |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Clark Barrett | Removed an assertion, unneeded header file |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Morgan Deters | some changes to make CVC4 work nicely with trace execut... |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Morgan Deters | making --simplification=none the default for quantified... |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Kshitij Bansal | bug ifx, mv |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Kshitij Bansal | restore destruction of stuff in driver |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Kshitij Bansal | This commit: |
blob | commitdiff | raw | diff to current |
2012-06-14 |
Tim King | Brings the tuning branch into trunk. This includes... |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Clark Barrett | Moved some things around in the preprocessor. Now... |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Kshitij Bansal | cleanup of exit mechanism when decisionEngine is on... |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Clark Barrett | Fixed compile error |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Clark Barrett | Enabling constant propagation |
blob | commitdiff | raw | diff to current |
2012-06-12 |
Clark Barrett | Adding constant propagation code - needs more testing... |
blob | commitdiff | raw | diff to current |
2012-06-09 |
Clark Barrett | Turning on unconstrained simp for QF_AUFBV |
blob | commitdiff | raw | diff to current |
2012-06-08 |
Kshitij Bansal | Merge from decision branch (till r3663) |
blob | commitdiff | raw | diff to current |
2012-06-07 |
Morgan Deters | LogicInfo locking implemented, and some initialization... |
blob | commitdiff | raw | diff to current |
2012-06-06 |
Clark Barrett | Don't ever call nonclausalSimplify if simplificationMod... |
blob | commitdiff | raw | diff to current |
2012-06-06 |
Morgan Deters | removing std::cout from trunk |
blob | commitdiff | raw | diff to current |
2012-06-04 |
Clark Barrett | Added preprocessing pass that propagates unconstrained... |
blob | commitdiff | raw | diff to current |
2012-06-01 |
Morgan Deters | add a global user-context push/pop in smt engine, just... |
blob | commitdiff | raw | diff to current |
2012-05-31 |
Clark Barrett | Fixed bug in bv: one more case where non-shared equalit... |
blob | commitdiff | raw | diff to current |
2012-05-30 |
Clark Barrett | Added BitwiseEq bitvector rewrite |
blob | commitdiff | raw | diff to current |
2012-05-15 |
Tim King | This commit removes the CONST_INTEGER kind from nodes... |
blob | commitdiff | raw | diff to current |
2012-05-14 |
Dejan Jovanović | fixes for shared term registration. previously the... |
blob | commitdiff | raw | diff to current |
2012-05-13 |
Dejan Jovanović | fixing build warnings |
blob | commitdiff | raw | diff to current |
2012-05-11 |
Clark Barrett | Disabled arith-rewrite-equalities by default unless... |
blob | commitdiff | raw | diff to current |
2012-05-11 |
Clark Barrett | Added some ITE rewrites, |
blob | commitdiff | raw | diff to current |
2012-05-09 |
Dejan Jovanović | * simplifying equality engine interface |
blob | commitdiff | raw | diff to current |
2012-05-09 |
Kshitij Bansal | Merge from decision branch (ITE support) |
blob | commitdiff | raw | diff to current |
2012-04-30 |
Clark Barrett | Added map from skolem variables to new ite formulas... |
blob | commitdiff | raw | diff to current |
2012-04-28 |
Morgan Deters | New LogicInfo functionality. |
blob | commitdiff | raw | diff to current |
2012-04-23 |
Kshitij Bansal | Merge from decision branch -- partially working justifi... |
blob | commitdiff | raw | diff to current |
2012-04-17 |
Kshitij Bansal | A dummy decision engine. Expected performance impact... |
blob | commitdiff | raw | diff to current |
2012-04-17 |
Tim King | Merges branches/arithmetic/atom-database r2979 through... |
blob | commitdiff | raw | diff to current |
2012-04-11 |
Morgan Deters | merge from arrays-clark branch |
blob | commitdiff | raw | diff to current |
2012-04-06 |
Morgan Deters | * Fix ITEs and functions in CVC language printer. |
blob | commitdiff | raw | diff to current |
2012-04-02 |
Kshitij Bansal | fix for cvc4_logic dump |
blob | commitdiff | raw | diff to current |
2012-03-22 |
Liana Hadarean | Merged updated version of the bitvector theory: |
blob | commitdiff | raw | diff to current |
2012-03-21 |
Morgan Deters | Disable nonclausal simplification for QF_SAT benchmarks... |
blob | commitdiff | raw | diff to current |
2012-03-09 |
Morgan Deters | Some work on the dump infrastructure to support portfol... |
blob | commitdiff | raw | diff to current |
2012-03-02 |
Dejan Jovanović | CDMap -> CDHashMap |
blob | commitdiff | raw | diff to current |
2012-03-01 |
Morgan Deters | Partial merge from kind-backend branch, including Minis... |
blob | commitdiff | raw | diff to current |
2012-02-28 |
Morgan Deters | Replace the sequence of hardcoded addTheory() calls... |
blob | commitdiff | raw | diff to current |
2012-02-24 |
Dejan Jovanović | Theory interface changes: |
blob | commitdiff | raw | diff to current |
2012-02-23 |
Morgan Deters | Added ability to set a "cvc4-specific logic" in standar... |
blob | commitdiff | raw | diff to current |
2012-02-20 |
Morgan Deters | Added Theory::postsolve() infrastructure as Clark reque... |
blob | commitdiff | raw | diff to current |
2012-02-20 |
Morgan Deters | By default, ONLY enable symmetry breaker ONLY for QF_UF... |
blob | commitdiff | raw | diff to current |
2011-10-29 |
Morgan Deters | Support for SMT-LIBv2 (get-proof), CVC-style DUMP_PROOF... |
blob | commitdiff | raw | diff to current |
2011-10-28 |
Liana Hadarean | merged the proofgen3 branch into trunk: |
blob | commitdiff | raw | diff to current |
2011-10-13 |
Morgan Deters | Interruption, time-out, and deterministic time-out... |
blob | commitdiff | raw | diff to current |
2011-10-03 |
Morgan Deters | user push/pop support in minisat and simplification... |
blob | commitdiff | raw | diff to current |
2011-09-30 |
Morgan Deters | fixes to incremental simplification, cnf routines,... |
blob | commitdiff | raw | diff to current |
2011-09-29 |
Morgan Deters | Some base infrastructure for user push/pop; a few bugfi... |
blob | commitdiff | raw | diff to current |
2011-09-16 |
Morgan Deters | dump define-funs correctly with "--dump declarations... |
blob | commitdiff | raw | diff to current |
2011-09-15 |
Dejan Jovanović | additional stuff for sharing, |
blob | commitdiff | raw | diff to current |
2011-09-02 |
Morgan Deters | Merge from my post-smtcomp branch. Includes: |
blob | commitdiff | raw | diff to current |
2011-09-02 |
Morgan Deters | Partial merge of integers work; this is simple B&B... |
blob | commitdiff | raw | diff to current |
2011-08-24 |
Dejan Jovanović | Simplification of the preregister and register throught... |
blob | commitdiff | raw | diff to current |
2011-07-11 |
Morgan Deters | merge from symmetry branch |
blob | commitdiff | raw | diff to current |
2011-07-09 |
Dejan Jovanović | surprize surprize |
blob | commitdiff | raw | diff to current |
2011-07-05 |
Dejan Jovanović | updated preprocessing and rewriting input equalities... |
blob | commitdiff | raw | diff to current |
2011-05-23 |
Morgan Deters | fixes for "make dist" and "make doc", minor cleanups |
blob | commitdiff | raw | diff to current |
2011-05-23 |
Morgan Deters | Merge from arrays2 branch. |
blob | commitdiff | raw | diff to current |
2011-05-05 |
Morgan Deters | Merge from nonclausal-simplification-v2 branch: |
blob | commitdiff | raw | diff to current |
2011-05-02 |
Morgan Deters | fix a performance issue from last commit |
blob | commitdiff | raw | diff to current |
2011-05-02 |
Morgan Deters | Minor fixes to various parts of CVC4, including the... |
blob | commitdiff | raw | diff to current |
2011-04-25 |
Morgan Deters | Monday tasks: |
blob | commitdiff | raw | diff to current |
next |