summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-03-09Strengthen minisat assertion regarding t-propagations that was ↵Morgan Deters
unintentionally allowing a theory to propagate p and ~p at the same time (and the conflict was undetected, leading to an incorrect answer). Credit to Clark for finding this.
2012-03-09minor fixes: to "make dist" in build directories with language bindings ↵Morgan Deters
enabled; and to makefile standards conformance
2012-03-08fix "make dist"Morgan Deters
2012-03-08Fixin the bug Clark found. In final check, enqueued propagations were not ↵Dejan Jovanović
discharged.
2012-03-08Removing QUICK_CHECK, and other unused ones, from the Theory::Effort.Dejan Jovanović
Seems to be working better <http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3749&category=&p=5&reference_id=3739>, and should fix the failing cases in the regressions. Removing one test case from the integer regress0.
2012-03-07cdqueue : fix size(). Thank you Clark for spotting this silly mistake.François Bobot
2012-03-07fix some Java compatibility-layer interface problems; also fix some Mac OS X ↵Morgan Deters
build issues
2012-03-06updating the equality engine to be able to give explanations for terms that ↵Dejan Jovanović
were not in the databas (queried by areEqual and areDisequal) and it's a bit better http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3738&category=&p=-1&reference_id=3731
2012-03-03Changing the dependency checking; GMP is required (and sometimes must be ↵Morgan Deters
explicitly linked in with -l) when using CLN. Fixes a bug on recent Debian that Francois reported. Hopefully this doesn't break anything..
2012-03-02Remove some commented out code from sat.hKshitij Bansal
2012-03-02This commit merges in the changes from branches/arithmetic/refactor0Tim King
- Improved the checks in AssertLower and AssertUpper so that redundant bounds cause less work. - Because of the above change, d_constantIntegerVariables now cannot have duplicate elements enqueued. This allows removing d_varsInDioSolver. - Fix to an assertion in CDQueue. - Implements a CDArithVarSet using a vector of booleans and CDList. - Refactored ArithVar out of arith_utilities.h. Miscellaneous cleanup of arithmetic.
2012-03-02CDMap -> CDHashMapDejan Jovanović
CDSet -> CDHashSet
2012-03-02committing the TNode/Node fix that was in the kind-backend branch; there's ↵Morgan Deters
still something fishy here, I think I need to merge in a few more things to support incrementality properly. But this fixes "make check" for now
2012-03-02Renamed CDQueue to CDTrailQueue and CDQueue2 to CDQueue. Small changes to ↵Tim King
function names and documentation.
2012-03-01Partial merge from kind-backend branch, including Minisat and CNF work toMorgan Deters
support incrementality. Some clean-up work will likely follow, but the CNF/Minisat stuff should be left pretty much untouched. Expected performance change negligible; slightly better on memory: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3705&reference_id=3697&mode=&category=&p=5 Note that there are crashes, but that these are exhibited in the nightly regression run too!
2012-03-01cdqueue2 : cdlist that can be used like queue and can delete element that ↵François Bobot
will never be restored
2012-03-01Fixed a copy paste error where a lower bound was looked up instead of an ↵Tim King
upper bound.
2012-02-29This should fix the debian build fails:Liana Hadarean
* removed bvpicosat directory as it is currently not used Cleared some of the flurry of warnings my previous merge caused in src/prop/
2012-02-29fixing bug310Dejan Jovanović
* theories that are parametric and therefore need the combination framwork should be tagged as "parametric" in the kinds file * default care graph computation was not sufficient, fixed
2012-02-29consistency in how the Dump output stream is usedMorgan Deters
2012-02-28This commit merges in branches/arithmetic/internalbb up to revision 2831. ↵Tim King
This is a significant refactoring of code. - r2820 -- Refactors Simplex so that it does significantly fewer functions. -- Adds the LinearEqualityModule for handling update and pivotAndUpdate and other utility functions that require access to both the tableau and partial model. -- Some of the code for propagation has moved to TheoryArith. -r2826 -- Small changes to documentation and removes the no longer implemented deduceLowerBound() and deduceUpperBound(). - r2827 -- Adds isZero() to Rational. Adds cmp to DeltaRational. - r2831 -- Refactored comparison to upper and lower in the partial model to use DeltaRational::cmp. -- Refactored AssertUpper and AssertLower in TheoryArith to include functionality that has weaseled into TheoryArith::assertionCases.
2012-02-28Improves the arithmetic difference manager to delay any work until a shared ↵Tim King
term is added.
2012-02-28fix theory "kinds" file documentation for allowed arity of operatorsMorgan Deters
2012-02-28Adds the CDQueue class. This is a wrapper for combining a CDList<T> and a ↵Tim King
CDO<size_t> into a FIFO queue.
2012-02-28Replace the sequence of hardcoded addTheory() calls with a use of the theory ↵Morgan Deters
traits---with the effect that everything with a kinds file is registered as a theory. Eventually we may want a more dynamic way of selecting theory implementations, but for now we don't have a need for this. Expected performance impact: none. (This commit addresses and re-closes the reopened bug #307.)
2012-02-27fixes to new-theory script; resolves bug #307Morgan Deters
2012-02-25ppAsert -> ppAssertDejan Jovanović
2012-02-25Refactored CnfStream to work with the bv theory Bitblaster:Liana Hadarean
* separated SatSolverInput interface class into two classes: - TheoryProxy for the sat solver to communicate with the theories - SatSolverInterface abstract class to communicate with the sat solver * instead of using #ifdef typedef for SatClauses and SatLiterals, now there are CVC4 SatLiteral/SatClause types and mappings between them and the internal sat solver clause/literal representation * added abstract classes for DPLLSatSolver and BVSatSolver different interfaces Replaced TheoryBV with bitblasting implementation: * all operators bitblasted * only operator elimination rewrite rules so far
2012-02-24Theory interface changes:Dejan Jovanović
solve -> ppAsert staticLearning -> ppStaticLearn preprocess -> ppRewrite SolveStatus -> PPAssertStatus (SOLVE_* -> PP_ASSERT_*) via Eclipse refactoring magic.
2012-02-23Added ability to set a "cvc4-specific logic" in standards-compliantMorgan Deters
SMT-LIBv1 and SMT-LIBv2 input: In SMT-LIBv1, you specify the "cvc4_logic" benchmark attribute; for instance: (benchmark actually_a_sat_benchmark_but_looks_like_uf :logic QF_UF :cvc4_logic { QF_SAT } [...] In SMT-LIBv2, you use a set-info; for instance: (set-logic QF_UF) (set-info :cvc4-logic "QF_SAT") [...] Right now, the only thing this does is disable the symmetry breaker for benchmarks like the above ones. As part of this work, TheoryEngine::setLogic() was removed (the logic field there wasn't actually used anywhere, its need disappeared when Theory::setUninterpretedSortOwner() was provided). Also, Theory::d_uninterpretedSortOwner got a name change to Theory::s_uninterpretedSortOwner, to highlight that it is static to the Theory class. This represents a breakage of our separation goals for CVC4, since it means that two SmtEngines cannot be created separately to solve a QF_AX and QF_UF problem. A bug report is pending.
2012-02-23pcvc4 only built if --with-portfolio given to the configure script ↵Morgan Deters
(Clark-requested change)
2012-02-22Fix for bug 305.Tim King
2012-02-22fixes to configure and boost.m4 to make certain boost installations nonfatal ↵Morgan Deters
errors; threading support should only be required to build pcvc4, not cvc4
2012-02-22another static library unavailability issueMorgan Deters
2012-02-22make sure to clear out READLINE_LIBS if readline causes problems at ↵Morgan Deters
configure time; fixes a bug reported by Clark for static-binary builds on machines where no static libreadline is available (like CIMS machines)
2012-02-22Added OutputChannel::propagateAsDecision() functionality, allowing a theoryMorgan Deters
to request a decision on a literal. All these theory requests are kept in a context-dependent queue and serviced in order when the SAT solver goes to make a decision. Requests that don't have a SAT literal give an assert-fail. Requests for literals that already have an assignment are silently ignored. Since the queue is CD, requests can actually be serviced more than once (e.g., if a request is made at DL 5, but not serviced until DL 10, and later, a conflict backtracks to level 7, the request may be serviced again). Performance impact: none to negligible for theories that don't use it See http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3620&reference_id=3614&mode=&category=&p=0
2012-02-22Fixes to documentation / fixes for MacOSMorgan Deters
2012-02-22minor change to order fn in sat solver's ElimLtKshitij Bansal
(better, (marginally) faster -- regressions 3605, 3606)
2012-02-21add a "--with-portfolio" configure option that makes a missing boost-thread ↵Morgan Deters
library an error; useful for builds requiring a "pcvc4" binary at the end
2012-02-21fix src/util/hash.h to specialize GNU's hash template for <uint64_t> on ↵Morgan Deters
platforms that need it; fixes Mac builds.
2012-02-21language bindings fixes for yesterday's portfolio mergeMorgan Deters
2012-02-21Fix for bug303. The problem was with function applications that get ↵Dejan Jovanović
normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced. Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
2012-02-21don't require libboost_thread (its presence is detected at configure-time), ↵Morgan Deters
and other build/documentation fixes from yesterday's portfolio merge; resolves bug 302
2012-02-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in ↵Morgan Deters
my previous checkin)
2012-02-20fix "make dist"Morgan Deters
2012-02-20zlib not required; remove configure's dependency on itMorgan Deters
2012-02-20portfolio mergeMorgan Deters
2012-02-20readline links in -ltermcap -ltinfo too (fixes breakage in static-binary builds)Morgan Deters
2012-02-20Added Theory::postsolve() infrastructure as Clark requested.Morgan Deters
(Though currently unused.) For theories that request presolve and postsolve (in their kinds file), they will get a presolve() notification before the first check(). After the final check during the current search, they get a postsolve(). presolve() and postsolve() notifications always come in pairs, bracketing all check()/propagate()/getValue() calls related to a single query. In the case of incremental benchmarks, theories may get additional presolve()/postsolve() pairs, but again, they always come in pairs. Expected performance impact: none (for theories that don't use it) http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3598&reference_id=3581&p=5
2012-02-20By default, ONLY enable symmetry breaker ONLY for QF_UF (both SMT-LIBv1Morgan Deters
and SMT-LIBv2). There are --enable-symmetry-breaker and --disable-symmetry-breaker options that are always respected regardless of this default. Expected performance impact: positive New default (UF only) compared to old default (always on): http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3595&p=5 Symmetry breaker remains a big win on UF: http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=3594&reference_id=3596&p=5 The last link to results looks at first that the symmetry breaker should always be turned off, since its use loses more regressions than it gains. *However*, the lost ones are only our "QF_SAT" benchmarks. For these, we should indeed turn off the symmetry breaker, but that's impossible for now because we tag them internally with the logic "QF_UF."
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback