summaryrefslogtreecommitdiff
path: root/src/prop
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-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-02Remove some commented out code from sat.hKshitij Bansal
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-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-29consistency in how the Dump output stream is usedMorgan Deters
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-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-22minor change to order fn in sat solver's ElimLtKshitij Bansal
(better, (marginally) faster -- regressions 3605, 3606)
2012-02-20fix sharing issue for portfolio (full lit-to-node map wasn't being kept in ↵Morgan Deters
my previous checkin)
2012-02-20portfolio mergeMorgan Deters
2011-12-12* merging some uf stuff from incremental_work branch that somehow nobody ↵Dejan Jovanović
merged-in * since two theories can propagate the same literal minisat now explicitly checks that a propagated literal has not been asserted yet
2011-11-29Merging the branch branches/arithmetic/shared-terms into trunk. Arithmetic ↵Tim King
now supports propagating equalities when a slack variable corresponding to a difference of shared terms must be 0. Similarly disequalities are propagated when these variables cannot be zero.
2011-11-15Bindings work (ocaml bindings are now sort of working); also minor cleanupMorgan Deters
2011-11-02fully implement the always-check-again-after-the-output-channel-is-used fix ↵Morgan Deters
for bug #275. will finally close #275.
2011-10-28merged the proofgen3 branch into trunk:Liana Hadarean
- can now output LFSC checkable resolution proofs - added configuration option --enable-proof - added command line argument --proof To turn proofs on build with proofs enabled and run with --proof.
2011-10-17Sharing workDejan Jovanović
2011-10-13fix make distMorgan Deters
2011-10-13Interruption, time-out, and deterministic time-out ("resource-out") features.Morgan Deters
Details here: http://goedel.cims.nyu.edu/wiki/Meeting_Minutes_-_October_14,_2011#Resource.2Ftime_limiting_API This will need more work, but it's a start. Also implemented TheoryEngine::properPropagation(). Other minor things.
2011-10-05ensureLiteral() in CNF stream to support Andy's quantifiers work; an update ↵Morgan Deters
to model gen on booleans; and a little cleanup
2011-10-03user push/pop support in minisat and simplification; also bindings workMorgan Deters
2011-09-30fix to CNF undoTranslate(), to support incrementalityMorgan Deters
2011-09-30more push/pop infrastructure, some SAT stuffMorgan Deters
2011-09-30fixes to incremental simplification, cnf routines, other stuff in ↵Morgan Deters
preparation of user push/pop in SAT solver
2011-09-29Some base infrastructure for user push/pop; a few bugfixes to user push/pop ↵Morgan Deters
and model gen also. I also expect this commit to fix bug #273. No performance change is expected on regressions with this commit, see http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
2011-09-16fix numerous documentation issues; doxygen complains much less, nowMorgan Deters
2011-09-15additional stuff for sharing, Dejan Jovanović
2011-09-02Merge from my post-smtcomp branch. Includes:Morgan Deters
Dumping infrastructure. Can dump preprocessed queries and clauses. Can also dump queries (for testing with another solver) to see if any conflicts are missed, T-propagations are missed, all lemmas are T-valid, etc. For a full list of options see --dump=help. CUDD building much cleaner. Documentation and assertion fixes. Printer improvements, printing of commands in language-defined way, etc. Typechecker stuff in expr package now autogenerated, no need to manually edit the expr package when adding a new theory. CVC3 compatibility layer (builds as libcompat). SWIG detection and language binding support (infrastructure). Support for some Z3 extended commands (like datatypes) in SMT-LIBv2 mode (when not in compliance mode). Copyright and file headers regenerated.
2011-09-02Partial merge of integers work; this is simple B&B and some pseudobooleanMorgan Deters
infrastructure, and takes care not to affect CVC4's performance on LRA benchmarks.
2011-09-02* Changing pre-registration to be context dependent -- it is called from the ↵Dejan Jovanović
SAT solver on every backtrack * Updated UF to handle the context dependent pre-registration * Additionally some small changes in order to satisfy warnings of the eclipse code analysis tool
2011-08-30Fixin the SAT solver for Andy. Even if a SAT lemma is added, a FULL-CHECK ↵Dejan Jovanović
will be reissued. Some unexpected slowdowns, but not too much.
2011-08-17new implementation of lemmas on demandDejan Jovanović
comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>
2011-07-11Clark's work on array theory - can now solve all QF_AX problemsClark Barrett
2011-07-11merge from symmetry branchMorgan Deters
2011-07-10changing the sat solver remove clauses constantsDejan Jovanović
with these we get closer to yices on uf and it seems better on lra vs yices uf http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2590&category=&p=5&reference_id=1471 vs trunk on lra http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2591&category=&p=5&reference_id=2576
2011-07-09surprize surprizeDejan Jovanović
2011-07-07removing duplicate clauses in ite cnf conversionDejan Jovanović
2011-07-06Fixing two bugs:Dejan Jovanović
1) arithmetic should check for subterms when solving equations, for instance x = if b then x + 1 else x -1 is not a valid substitution 2) a memory problem in minisat - explanations are constructed during conflict analysis, so the clause database might resize and relocate, which invalidates any references to clauses
2011-07-05updated preprocessing and rewriting input equalities into inequalities for LRADejan Jovanović
2011-04-14reverting back the minisat code and adding a simpler one that shouldn't ↵Dejan Jovanović
change the search
2011-04-14Three things:Morgan Deters
1. Infrastructure for unit T-conflicts added to SAT proxy (and also the theory output channel documentation); previously theories could not communicate unit T-conflicts with the SAT layer because that layer had an implicit assumption (not asserted) that the conflict nodes were an AND. 2. UF now pre-rewrites trivial equalities to "true". These could conceivably occur in artificial benchmarks in this form: (let (?x BIG-HUGE-TERM) ... (= ?x ?x) ... ) 3. The SMT-LIBv2 printer now properly prints Bool constants.
2011-04-14fixing an uninitialized literal variableDejan Jovanović
2011-04-13adding support for unit conflicts in minisat...Dejan Jovanović
2011-04-13fix compiler warning in non-replay buildsMorgan Deters
2011-04-10merge from replay branchMorgan Deters
2011-04-09changing the sat solver to assert propagated literals back to the theoriesDejan Jovanović
2011-04-05Added options for setting the random decision frequency and random seed for ↵Tim King
the sat solver. Also added command line options for setting both.
2011-04-05Minor adjustments to the Registrar commit in 1644, documentation.Morgan Deters
2011-04-04Merging the satliteral-before-prereg branch into trunk. Theory ↵Tim King
preregistration is now called during the conversion to cnf. This fixes bug 257.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback