diff options
author | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
---|---|---|
committer | PaulMeng <pmtruth@hotmail.com> | 2016-07-05 13:56:53 -0400 |
commit | 36a0d1d948f201471596e092136c5a00103f78af (patch) | |
tree | 7a9b0d79074da1cb0c1cbed986584d50792a30e9 /src/prop/minisat | |
parent | 66525e81928d0d025dbcc197ab3ef772eac31103 (diff) | |
parent | a58abbe71fb1fc07129ff9c7568ac544145fb57c (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4.git
Conflicts:
proofs/signatures/Makefile.am
src/Makefile.am
src/expr/datatype.cpp
src/options/datatypes_options
src/options/options_template.cpp
src/options/quantifiers_options
src/proof/arith_proof.cpp
src/proof/arith_proof.h
src/proof/array_proof.cpp
src/proof/array_proof.h
src/proof/bitvector_proof.cpp
src/proof/bitvector_proof.h
src/proof/cnf_proof.cpp
src/proof/cnf_proof.h
src/proof/proof_manager.cpp
src/proof/proof_manager.h
src/proof/sat_proof.h
src/proof/sat_proof_implementation.h
src/proof/skolemization_manager.h
src/proof/theory_proof.cpp
src/proof/theory_proof.h
src/proof/uf_proof.cpp
src/proof/uf_proof.h
src/prop/cnf_stream.cpp
src/prop/cnf_stream.h
src/prop/minisat/core/Solver.cc
src/prop/prop_engine.cpp
src/prop/prop_engine.h
src/prop/theory_proxy.cpp
src/smt/smt_engine.cpp
src/smt/smt_engine_check_proof.cpp
src/theory/arrays/array_proof_reconstruction.cpp
src/theory/arrays/theory_arrays.cpp
src/theory/bv/eager_bitblaster.cpp
src/theory/bv/lazy_bitblaster.cpp
src/theory/datatypes/theory_datatypes.cpp
src/theory/quantifiers/alpha_equivalence.cpp
src/theory/quantifiers/candidate_generator.cpp
src/theory/quantifiers/candidate_generator.h
src/theory/quantifiers/ce_guided_single_inv.cpp
src/theory/quantifiers/ceg_instantiator.cpp
src/theory/quantifiers/conjecture_generator.cpp
src/theory/quantifiers/equality_infer.cpp
src/theory/quantifiers/equality_infer.h
src/theory/quantifiers/inst_match_generator.cpp
src/theory/quantifiers/inst_propagator.cpp
src/theory/quantifiers/inst_propagator.h
src/theory/quantifiers/inst_strategy_e_matching.cpp
src/theory/quantifiers/inst_strategy_e_matching.h
src/theory/quantifiers/instantiation_engine.cpp
src/theory/quantifiers/model_builder.cpp
src/theory/quantifiers/model_engine.cpp
src/theory/quantifiers/quant_conflict_find.cpp
src/theory/quantifiers/quant_conflict_find.h
src/theory/quantifiers/quant_split.cpp
src/theory/quantifiers/quant_util.cpp
src/theory/quantifiers/quantifiers_rewriter.cpp
src/theory/quantifiers/quantifiers_rewriter.h
src/theory/quantifiers/term_database.cpp
src/theory/quantifiers/term_database.h
src/theory/quantifiers/trigger.cpp
src/theory/quantifiers/trigger.h
src/theory/quantifiers_engine.cpp
src/theory/quantifiers_engine.h
src/theory/sets/kinds
src/theory/sets/theory_sets_private.cpp
src/theory/sets/theory_sets_private.h
src/theory/sets/theory_sets_rewriter.cpp
src/theory/sets/theory_sets_type_rules.h
src/theory/strings/theory_strings.cpp
src/theory/strings/theory_strings.h
src/theory/theory_engine.cpp
src/theory/theory_engine.h
src/theory/uf/equality_engine.cpp
test/regress/regress0/fmf/Makefile.am
test/regress/regress0/quantifiers/Makefile.am
test/regress/regress0/strings/Makefile.am
test/regress/regress0/sygus/Makefile.am
test/regress/regress0/sygus/max2-univ.sy
Diffstat (limited to 'src/prop/minisat')
-rw-r--r-- | src/prop/minisat/core/Solver.cc | 32 | ||||
-rw-r--r-- | src/prop/minisat/minisat.cpp | 16 | ||||
-rw-r--r-- | src/prop/minisat/minisat.h | 3 |
3 files changed, 38 insertions, 13 deletions
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc index 411b89514..a682a893b 100644 --- a/src/prop/minisat/core/Solver.cc +++ b/src/prop/minisat/core/Solver.cc @@ -232,6 +232,8 @@ CRef Solver::reason(Var x) { vec<Lit> explanation; MinisatSatSolver::toMinisatClause(explanation_cl, explanation); + Debug("pf::sat") << "Solver::reason: explanation_cl = " << explanation_cl << std::endl; + // Sort the literals by trail index level lemma_lt lt(*this); sort(explanation, lt); @@ -266,6 +268,12 @@ CRef Solver::reason(Var x) { } explanation.shrink(i - j); + Debug("pf::sat") << "Solver::reason: explanation = " ; + for (int i = 0; i < explanation.size(); ++i) { + Debug("pf::sat") << explanation[i] << " "; + } + Debug("pf::sat") << std::endl; + // We need an explanation clause so we add a fake literal if (j == 1) { // Add not TRUE to the clause @@ -276,6 +284,7 @@ CRef Solver::reason(Var x) { CRef real_reason = ca.alloc(explLevel, explanation, true); // FIXME: at some point will need more information about where this explanation // came from (ie. the theory/sharing) + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (1)" << std::endl; PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); ProofManager::getCnfProof()->registerConvertedClause(id, true); // no need to pop current assertion as this is not converted to cnf @@ -336,6 +345,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) // If we are in solve or decision level > 0 if (minisat_busy || decisionLevel() > 0) { + Debug("pf::sat") << "Add clause adding a new lemma: "; + for (int k = 0; k < ps.size(); ++k) { + Debug("pf::sat") << ps[k] << " "; + } + Debug("pf::sat") << std::endl; + lemmas.push(); ps.copyTo(lemmas.last()); lemmas_removable.push(removable); @@ -379,7 +394,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id) cr = ca.alloc(clauseLevel, ps, false); clauses_persistent.push(cr); - attachClause(cr); + attachClause(cr); if(PROOF_ON()) { PROOF( @@ -1234,12 +1249,12 @@ lbool Solver::search(int nof_conflicts) } else { - // If this was a final check, we are satisfiable + // If this was a final check, we are satisfiable if (check_type == CHECK_FINAL) { - bool decisionEngineDone = proxy->isDecisionEngineDone(); + bool decisionEngineDone = proxy->isDecisionEngineDone(); // Unless a lemma has added more stuff to the queues if (!decisionEngineDone && - (!order_heap.empty() || qhead < trail.size()) ) { + (!order_heap.empty() || qhead < trail.size()) ) { check_type = CHECK_WITH_THEORY; continue; } else if (recheck) { @@ -1666,6 +1681,13 @@ CRef Solver::updateLemmas() { { // The current lemma vec<Lit>& lemma = lemmas[i]; + + Debug("pf::sat") << "Solver::updateLemmas: working on lemma: "; + for (int k = 0; k < lemma.size(); ++k) { + Debug("pf::sat") << lemma[k] << " "; + } + Debug("pf::sat") << std::endl; + // If it's an empty lemma, we have a conflict at zero level if (lemma.size() == 0) { Assert (! PROOF_ON()); @@ -1725,6 +1747,7 @@ CRef Solver::updateLemmas() { TNode cnf_assertion = lemmas_cnf_assertion[i].first; TNode cnf_def = lemmas_cnf_assertion[i].second; + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (2)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); @@ -1741,6 +1764,7 @@ CRef Solver::updateLemmas() { Node cnf_assertion = lemmas_cnf_assertion[i].first; Node cnf_def = lemmas_cnf_assertion[i].second; + Debug("pf::sat") << "Minisat::Solver registering a THEORY_LEMMA (3)" << std::endl; ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion); ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def); diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index bfbf9da6f..ff726e299 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -150,7 +150,7 @@ ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) { // FIXME: This relies on the invariant that when ok() is false // the SAT solver does not add the clause (which is what Minisat currently does) if (!ok()) { - return ClauseIdUndef; + return ClauseIdUndef; } d_minisat->addClause(minisat_clause, removable, clause_id); PROOF( Assert (clause_id != ClauseIdError);); @@ -185,7 +185,7 @@ SatValue MinisatSatSolver::solve() { } bool MinisatSatSolver::ok() const { - return d_minisat->okay(); + return d_minisat->okay(); } void MinisatSatSolver::interrupt() { @@ -204,20 +204,20 @@ bool MinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const return true; } -void MinisatSatSolver::requirePhase(SatLiteral lit) { +void MinisatSatSolver::requirePhase(SatLiteral lit) { Assert(!d_minisat->rnd_pol); Debug("minisat") << "requirePhase(" << lit << ")" << " " << lit.getSatVariable() << " " << lit.isNegated() << std::endl; SatVariable v = lit.getSatVariable(); d_minisat->freezePolarity(v, lit.isNegated()); } -bool MinisatSatSolver::flipDecision() { +bool MinisatSatSolver::flipDecision() { Debug("minisat") << "flipDecision()" << std::endl; return d_minisat->flipDecision(); } -bool MinisatSatSolver::isDecision(SatVariable decn) const { - return d_minisat->isDecision( decn ); +bool MinisatSatSolver::isDecision(SatVariable decn) const { + return d_minisat->isDecision( decn ); } /** Incremental interface */ @@ -291,7 +291,7 @@ namespace CVC4 { template<> prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) { return prop::MinisatSatSolver::toSatLiteral(lit); -} +} template<> void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl, @@ -300,5 +300,3 @@ void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& } } /* namespace CVC4 */ - - diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 535ce1a47..ec5297bb7 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -44,6 +44,9 @@ public: void initialize(context::Context* context, TheoryProxy* theoryProxy); ClauseId addClause(SatClause& clause, bool removable); + ClauseId addXorClause(SatClause& clause, bool rhs, bool removable) { + Unreachable("Minisat does not support native XOR reasoning"); + } SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase); SatVariable trueVar() { return d_minisat->trueVar(); } |