summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/bvminisat/bvminisat.cpp1
-rw-r--r--src/prop/bvminisat/bvminisat.h1
-rw-r--r--src/prop/bvminisat/core/Solver.cc5
-rw-r--r--src/prop/bvminisat/core/Solver.h15
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.cc3
-rw-r--r--src/prop/bvminisat/simp/SimpSolver.h1
-rw-r--r--src/prop/cnf_stream.cpp27
-rw-r--r--src/prop/cnf_stream.h24
-rw-r--r--src/prop/minisat/core/Solver.cc79
-rw-r--r--src/prop/minisat/core/Solver.h2
-rw-r--r--src/prop/minisat/minisat.cpp1
-rw-r--r--src/prop/minisat/simp/SimpSolver.cc4
-rw-r--r--src/prop/minisat/simp/SimpSolver.h1
-rw-r--r--src/prop/prop_engine.cpp15
-rw-r--r--src/prop/prop_engine.h14
-rw-r--r--src/prop/registrar.h12
-rw-r--r--src/prop/sat_solver.h15
-rw-r--r--src/prop/sat_solver_factory.cpp12
-rw-r--r--src/prop/sat_solver_factory.h12
-rw-r--r--src/prop/sat_solver_types.h12
-rw-r--r--src/prop/theory_proxy.cpp39
-rw-r--r--src/prop/theory_proxy.h12
22 files changed, 171 insertions, 136 deletions
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 936778e0d..54e3f2e8b 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -19,6 +19,7 @@
#include "prop/bvminisat/bvminisat.h"
#include "prop/bvminisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
#include "proof/sat_proof.h"
#include "util/statistics_registry.h"
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index ec8c3455a..20724efd2 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -21,6 +21,7 @@
#pragma once
#include "context/cdo.h"
+#include "proof/clause_id.h"
#include "prop/bvminisat/simp/SimpSolver.h"
#include "prop/sat_solver.h"
#include "util/statistics_registry.h"
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 2100160de..d626a5d15 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -30,11 +30,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "mtl/Sort.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
-#include "theory/interrupted.h"
-#include "proof/proof_manager.h"
#include "proof/bitvector_proof.h"
+#include "proof/clause_id.h"
+#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
#include "proof/sat_proof_implementation.h"
+#include "theory/interrupted.h"
#include "util/utility.h"
namespace CVC4 {
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 019c09bcd..555495149 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -21,20 +21,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#ifndef BVMinisat_Solver_h
#define BVMinisat_Solver_h
+#include <ext/hash_set>
+#include <vector>
+
+#include "context/context.h"
+#include "proof/clause_id.h"
+#include "proof/sat_proof.h"
#include "prop/bvminisat/core/SolverTypes.h"
-#include "prop/bvminisat/mtl/Vec.h"
-#include "prop/bvminisat/mtl/Heap.h"
#include "prop/bvminisat/mtl/Alg.h"
+#include "prop/bvminisat/mtl/Heap.h"
+#include "prop/bvminisat/mtl/Vec.h"
#include "prop/bvminisat/utils/Options.h"
-#include "context/cdhashmap.h"
-#include "proof/sat_proof.h"
-#include <ext/hash_set>
-#include <vector>
namespace CVC4 {
-typedef unsigned ClauseId;
namespace BVMinisat {
class Solver;
}
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index 311ed1dd1..cb5929320 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -23,8 +23,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "mtl/Sort.h"
#include "options/bv_options.h"
#include "options/smt_options.h"
-#include "utils/System.h"
+#include "proof/clause_id.h"
#include "proof/proof.h"
+#include "utils/System.h"
namespace CVC4 {
namespace BVMinisat {
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 5f6f46b91..9854bf77d 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#define BVMinisat_SimpSolver_h
#include "context/context.h"
+#include "proof/clause_id.h"
#include "prop/bvminisat/core/Solver.h"
#include "prop/bvminisat/mtl/Queue.h"
#include "util/statistics_registry.h"
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index d54848d26..aa1fc9587 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file cnf_stream.cpp
** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Kshitij Bansal, Liana Hadarean, Christopher L. Conway, Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Liana Hadarean, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief A CNF converter that takes in asserts and has the side effect
** of given an equisatisfiable stream of assertions to PropEngine.
@@ -15,6 +15,8 @@
** A CNF converter that takes in asserts and has the side effect
** of given an equisatisfiable stream of assertions to PropEngine.
**/
+#include "prop/cnf_stream.h"
+
#include <queue>
#include "base/cvc4_assert.h"
@@ -22,10 +24,10 @@
#include "expr/expr.h"
#include "expr/node.h"
#include "options/bv_options.h"
+#include "proof/clause_id.h"
+#include "proof/cnf_proof.h"
#include "proof/proof_manager.h"
#include "proof/sat_proof.h"
-#include "proof/cnf_proof.h"
-#include "prop/cnf_stream.h"
#include "prop/minisat/minisat.h"
#include "prop/prop_engine.h"
#include "prop/theory_proxy.h"
@@ -672,7 +674,8 @@ void TseitinCnfStream::convertAndAssert(TNode node,
bool removable,
bool negated,
ProofRule proof_id,
- TNode from) {
+ TNode from,
+ theory::TheoryId ownerTheory) {
Debug("cnf") << "convertAndAssert(" << node
<< ", removable = " << (removable ? "true" : "false")
<< ", negated = " << (negated ? "true" : "false") << ")" << endl;
@@ -682,6 +685,7 @@ void TseitinCnfStream::convertAndAssert(TNode node,
Node assertion = negated ? node.notNode() : (Node)node;
Node from_assertion = negated? from.notNode() : (Node) from;
+ d_cnfProof->setExplainerTheory(ownerTheory);
if (proof_id != RULE_INVALID) {
d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
@@ -693,7 +697,10 @@ void TseitinCnfStream::convertAndAssert(TNode node,
});
convertAndAssert(node, negated);
- PROOF(if (d_cnfProof) d_cnfProof->popCurrentAssertion(); );
+ PROOF
+ (if (d_cnfProof) {
+ d_cnfProof->popCurrentAssertion();
+ });
}
void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index a6b6781ca..cf9d519a7 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file cnf_stream.h
** \verbatim
- ** Original author: Tim King
- ** Major contributors: Morgan Deters, Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Andrew Reynolds
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Morgan Deters, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief This class transforms a sequence of formulas into clauses.
**
@@ -207,9 +207,14 @@ public:
* @param node node to convert and assert
* @param removable whether the sat solver can choose to remove the clauses
* @param negated whether we are asserting the node negated
+ * @param ownerTheory indicates the theory that should invoked to prove the formula.
*/
- virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
-
+ virtual void convertAndAssert(TNode node,
+ bool removable,
+ bool negated,
+ ProofRule proof_id,
+ TNode from = TNode::null(),
+ theory::TheoryId ownerTheory = theory::THEORY_LAST) = 0;
/**
* Get the node that is represented by the given SatLiteral.
* @param literal the literal from the sat solver
@@ -278,7 +283,8 @@ public:
* @param negated true if negated
*/
void convertAndAssert(TNode node, bool removable,
- bool negated, ProofRule rule, TNode from = TNode::null());
+ bool negated, ProofRule rule, TNode from = TNode::null(),
+ theory::TheoryId ownerTheory = theory::THEORY_LAST);
/**
* Constructs the stream to use the given sat solver.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b7fb1603d..411b89514 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -18,21 +18,22 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
+#include "prop/minisat/core/Solver.h"
+
#include <math.h>
#include <iostream>
#include "base/output.h"
#include "options/prop_options.h"
+#include "proof/clause_id.h"
#include "proof/proof_manager.h"
#include "proof/sat_proof_implementation.h"
#include "proof/sat_proof.h"
-#include "prop/minisat/core/Solver.h"
#include "prop/minisat/minisat.h"
#include "prop/minisat/mtl/Sort.h"
#include "prop/theory_proxy.h"
-
using namespace CVC4::prop;
namespace CVC4 {
@@ -229,7 +230,7 @@ CRef Solver::reason(Var x) {
proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
explanation_cl);
vec<Lit> explanation;
- MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
+ MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
// Sort the literals by trail index level
lemma_lt lt(*this);
@@ -602,20 +603,20 @@ Lit Solver::pickBranchLit()
/*_________________________________________________________________________________________________
|
| analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&) -> [void]
-|
+|
| Description:
| Analyze conflict and produce a reason clause.
-|
+|
| Pre-conditions:
| * 'out_learnt' is assumed to be cleared.
| * Current decision level must be greater than root level.
-|
+|
| Post-conditions:
| * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
-| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
+| * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the
| rest of literals. There may be others from the same level though.
| * returns the maximal level of the resolved clauses
-|
+|
|________________________________________________________________________________________________@*/
int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
{
@@ -661,14 +662,14 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
}
}
}
-
+
// Select next clause to look at:
while (!seen[var(trail[index--])]);
p = trail[index+1];
confl = reason(var(p));
seen[var(p)] = 0;
pathC--;
-
+
if ( pathC > 0 && confl != CRef_Undef ) {
PROOF( ProofManager::getSatProof()->addResolutionStep(p, confl, sign(p)); )
}
@@ -694,13 +695,13 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
out_learnt[j++] = out_learnt[i];
} else {
PROOF( ProofManager::getSatProof()->storeLitRedundant(out_learnt[i]); )
- // Literal is redundant, to be safe, mark the level as current assertion level
+ // Literal is redundant, to be safe, mark the level as current assertion level
// TODO: maybe optimize
max_resolution_level = std::max(max_resolution_level, user_level(var(out_learnt[i])));
}
}
}
-
+
}else if (ccmin_mode == 1){
Unreachable();
for (i = j = 1; i < out_learnt.size(); i++){
@@ -786,7 +787,7 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
/*_________________________________________________________________________________________________
|
| analyzeFinal : (p : Lit) -> [void]
-|
+|
| Description:
| Specialized analysis procedure to express the final conflict in terms of assumptions.
| Calculates the (possibly empty) set of assumptions that led to the assignment of 'p', and
@@ -865,7 +866,7 @@ CRef Solver::propagate(TheoryCheckType type)
if (lemmas.size() > 0) {
recheck = true;
confl = updateLemmas();
- return confl;
+ return confl;
} else {
recheck = proxy->theoryNeedCheck();
return confl;
@@ -921,7 +922,7 @@ void Solver::propagateTheory() {
proxy->theoryPropagate(propagatedLiteralsClause);
vec<Lit> propagatedLiterals;
- MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
+ MinisatSatSolver::toMinisatClause(propagatedLiteralsClause, propagatedLiterals);
int oldTrailSize = trail.size();
Debug("minisat") << "old trail size is " << oldTrailSize << ", propagating " << propagatedLiterals.size() << " lits..." << std::endl;
@@ -963,11 +964,11 @@ void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
/*_________________________________________________________________________________________________
|
| propagateBool : [void] -> [Clause*]
-|
+|
| Description:
| Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
| otherwise CRef_Undef.
-|
+|
| Post-conditions:
| * the propagation queue is empty, even if there was a conflict.
|________________________________________________________________________________________________@*/
@@ -1037,16 +1038,16 @@ CRef Solver::propagateBool()
/*_________________________________________________________________________________________________
|
| reduceDB : () -> [void]
-|
+|
| Description:
| Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
| clauses are clauses that are reason to some assignment. Binary clauses are never removed.
|________________________________________________________________________________________________@*/
-struct reduceDB_lt {
+struct reduceDB_lt {
ClauseAllocator& ca;
reduceDB_lt(ClauseAllocator& ca_) : ca(ca_) {}
- bool operator () (CRef x, CRef y) {
- return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
+ bool operator () (CRef x, CRef y) {
+ return ca[x].size() > 2 && (ca[y].size() == 2 || ca[x].activity() < ca[y].activity()); }
};
void Solver::reduceDB()
{
@@ -1114,7 +1115,7 @@ void Solver::rebuildOrderHeap()
/*_________________________________________________________________________________________________
|
| simplify : [void] -> [bool]
-|
+|
| Description:
| Simplify the clause database according to the current top-level assigment. Currently, the only
| thing done here is the removal of satisfied clauses, but more things can be put here.
@@ -1146,11 +1147,11 @@ bool Solver::simplify()
/*_________________________________________________________________________________________________
|
| search : (nof_conflicts : int) (params : const SearchParams&) -> [lbool]
-|
+|
| Description:
-| Search for a model the specified number of conflicts.
+| Search for a model the specified number of conflicts.
| NOTE! Use negative value for 'nof_conflicts' indicate infinity.
-|
+|
| Output:
| 'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
| all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
@@ -1219,9 +1220,9 @@ lbool Solver::search(int nof_conflicts)
max_learnts *= learntsize_inc;
if (verbosity >= 1)
- printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
- (int)conflicts,
- (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
+ printf("| %9d | %7d %8d %8d | %8d %8d %6.0f | %6.3f %% |\n",
+ (int)conflicts,
+ (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_literals,
(int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
}
@@ -1417,7 +1418,7 @@ lbool Solver::solve_()
//=================================================================================================
// Writing CNF to DIMACS:
-//
+//
// FIXME: this needs to be rewritten completely.
static Var mapVar(Var x, vec<Var>& map, Var& max)
@@ -1466,7 +1467,7 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
for (int i = 0; i < clauses_persistent.size(); i++)
if (!satisfied(ca[clauses_persistent[i]]))
cnt++;
-
+
for (int i = 0; i < clauses_persistent.size(); i++)
if (!satisfied(ca[clauses_persistent[i]])){
Clause& c = ca[clauses_persistent[i]];
@@ -1537,11 +1538,11 @@ void Solver::garbageCollect()
{
// Initialize the next region to a size corresponding to the estimated utilization degree. This
// is not precise but should avoid some unnecessary reallocations for the new region:
- ClauseAllocator to(ca.size() - ca.wasted());
+ ClauseAllocator to(ca.size() - ca.wasted());
relocAll(to);
if (verbosity >= 2)
- printf("| Garbage collection: %12d bytes => %12d bytes |\n",
+ printf("| Garbage collection: %12d bytes => %12d bytes |\n",
ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
to.moveTo(ca);
}
@@ -1698,7 +1699,7 @@ CRef Solver::updateLemmas() {
int backtrack_index = trail.size();
PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
-
+
// Attach all the clauses and enqueue all the propagations
for (int i = 0; i < lemmas.size(); ++ i)
{
@@ -1739,7 +1740,7 @@ CRef Solver::updateLemmas() {
(
Node cnf_assertion = lemmas_cnf_assertion[i].first;
Node cnf_def = lemmas_cnf_assertion[i].second;
-
+
ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
@@ -1784,20 +1785,20 @@ CRef Solver::updateLemmas() {
void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy)
{
-
+
// FIXME what is this CRef_lazy
if (cr == CRef_Lazy) return;
-
+
CRef old = cr; // save the old reference
Clause& c = operator[](cr);
if (c.reloced()) { cr = c.relocation(); return; }
-
+
cr = to.alloc(c.level(), c, c.removable());
c.relocate(cr);
if (proxy) {
- proxy->updateCRef(old, cr);
+ proxy->updateCRef(old, cr);
}
- // Copy extra data-fields:
+ // Copy extra data-fields:
// (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
to[cr].mark(c.mark());
if (to[cr].removable()) to[cr].activity() = c.activity();
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 777fb1093..99c47e045 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -27,6 +27,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "base/output.h"
#include "context/context.h"
+#include "proof/clause_id.h"
#include "prop/minisat/core/SolverTypes.h"
#include "prop/minisat/mtl/Alg.h"
#include "prop/minisat/mtl/Heap.h"
@@ -43,7 +44,6 @@ namespace prop {
}/* CVC4::prop namespace */
}/* CVC4 namespace */
-typedef unsigned ClauseId;
namespace CVC4 {
namespace Minisat {
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index 739d9087a..bfbf9da6f 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,6 +23,7 @@
#include "options/prop_options.h"
#include "options/smt_options.h"
#include "prop/minisat/simp/SimpSolver.h"
+#include "proof/clause_id.h"
#include "proof/sat_proof.h"
#include "util/statistics_registry.h"
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 5bdaea950..9b551fa70 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -18,10 +18,12 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE,
OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
**************************************************************************************************/
+#include "prop/minisat/simp/SimpSolver.h"
+
#include "options/prop_options.h"
+#include "proof/clause_id.h"
#include "proof/proof.h"
#include "prop/minisat/mtl/Sort.h"
-#include "prop/minisat/simp/SimpSolver.h"
#include "prop/minisat/utils/System.h"
using namespace CVC4;
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index a19bec1ef..a995c1357 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -23,6 +23,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
#include "cvc4_private.h"
+#include "proof/clause_id.h"
#include "prop/minisat/mtl/Queue.h"
#include "prop/minisat/core/Solver.h"
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 583e9da18..54cf4c457 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file prop_engine.cpp
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Kshitij Bansal, Christopher L. Conway, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Implementation of the propositional engine of CVC4
**
@@ -132,12 +132,13 @@ void PropEngine::assertFormula(TNode node) {
void PropEngine::assertLemma(TNode node, bool negated,
bool removable,
ProofRule rule,
+ theory::TheoryId ownerTheory,
TNode from) {
//Assert(d_inCheckSat, "Sat solver should be in solve()!");
Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
// Assert as (possibly) removable
- d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
+ d_cnfStream->convertAndAssert(node, removable, negated, rule, from, ownerTheory);
}
void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a71d4832d..b9ce7ca7e 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file prop_engine.h
** \verbatim
- ** Original author: Morgan Deters
- ** Major contributors: Dejan Jovanovic
- ** Minor contributors (to current version): Clark Barrett, Liana Hadarean, Christopher L. Conway, Kshitij Bansal, Tim King
+ ** Top contributors (to current version):
+ ** Morgan Deters, Dejan Jovanovic, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief The PropEngine (propositional engine); main interface point
** between CVC4's SMT infrastructure and the SAT solver
@@ -134,7 +134,7 @@ public:
* @param removable whether this lemma can be quietly removed based
* on an activity heuristic (or not)
*/
- void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
+ void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, theory::TheoryId ownerTheory, TNode from = TNode::null());
/**
* If ever n is decided upon, it must be in the given phase. This
diff --git a/src/prop/registrar.h b/src/prop/registrar.h
index b6dd021ab..bd8088921 100644
--- a/src/prop/registrar.h
+++ b/src/prop/registrar.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file registrar.h
** \verbatim
- ** Original author: Liana Hadarean
- ** Major contributors: Tim King, Morgan Deters
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief Class to encapsulate preregistration duties
**
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 1383308a3..92696ae25 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Morgan Deters, Liana Hadarean
- ** Minor contributors (to current version): none
+ ** Top contributors (to current version):
+ ** Liana Hadarean, Dejan Jovanovic, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver.
**
@@ -26,6 +26,7 @@
#include "context/cdlist.h"
#include "context/context.h"
#include "expr/node.h"
+#include "proof/clause_id.h"
#include "prop/sat_solver_types.h"
#include "util/statistics_registry.h"
@@ -37,8 +38,6 @@ namespace prop {
class TheoryProxy;
-typedef unsigned ClauseId;
-
class SatSolver {
public:
diff --git a/src/prop/sat_solver_factory.cpp b/src/prop/sat_solver_factory.cpp
index c131ca475..092ec72f2 100644
--- a/src/prop/sat_solver_factory.cpp
+++ b/src/prop/sat_solver_factory.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver_factory.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Tim King
- ** Minor contributors (to current version): Morgan Deters, Liana Hadarean
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver creation facility.
**
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 6a3053a18..7cc23a8e8 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver_factory.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Liana Hadarean, Morgan Deters
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Tim King, Morgan Deters
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver.
**
diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h
index c47c2b67b..557f9af65 100644
--- a/src/prop/sat_solver_types.h
+++ b/src/prop/sat_solver_types.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file sat_solver_types.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters, Liana Hadarean, Kshitij Bansal
+ ** Top contributors (to current version):
+ ** Dejan Jovanovic, Kshitij Bansal, Tim King
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief This class transforms a sequence of formulas into clauses.
**
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 63a09169f..4a4515eb9 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -1,13 +1,13 @@
/********************* */
/*! \file theory_proxy.cpp
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Clark Barrett, Christopher L. Conway, Tim King, Liana Hadarean
+ ** Top contributors (to current version):
+ ** Morgan Deters, Tim King, Liana Hadarean
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief [[ Add one-line brief description here ]]
**
@@ -98,19 +98,30 @@ void TheoryProxy::theoryPropagate(std::vector<SatLiteral>& output) {
void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
TNode lNode = d_cnfStream->getNode(l);
Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
- Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
- PROOF(ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); );
- Debug("prop-explain") << "explainPropagation() => " << theoryExplanation << std::endl;
- if (theoryExplanation.getKind() == kind::AND) {
- Node::const_iterator it = theoryExplanation.begin();
- Node::const_iterator it_end = theoryExplanation.end();
+
+ NodeTheoryPair theoryExplanation = d_theoryEngine->getExplanationAndExplainer(lNode);
+ Node explanationNode = theoryExplanation.node;
+ theory::TheoryId explainerTheory = theoryExplanation.theory;
+
+ PROOF({
+ ProofManager::getCnfProof()->pushCurrentAssertion(explanationNode);
+ ProofManager::getCnfProof()->setExplainerTheory(explainerTheory);
+
+ Debug("pf::sat") << "TheoryProxy::explainPropagation: setting explainer theory to: "
+ << explainerTheory << std::endl;
+ });
+
+ Debug("prop-explain") << "explainPropagation() => " << explanationNode << std::endl;
+ if (explanationNode.getKind() == kind::AND) {
+ Node::const_iterator it = explanationNode.begin();
+ Node::const_iterator it_end = explanationNode.end();
explanation.push_back(l);
for (; it != it_end; ++ it) {
explanation.push_back(~d_cnfStream->getLiteral(*it));
}
} else {
explanation.push_back(l);
- explanation.push_back(~d_cnfStream->getLiteral(theoryExplanation));
+ explanation.push_back(~d_cnfStream->getLiteral(explanationNode));
}
}
@@ -164,7 +175,7 @@ void TheoryProxy::notifyRestart() {
if(lemmaCount % 1 == 0) {
Debug("shared") << "=) " << asNode << std::endl;
}
- d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
+ d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID, theory::THEORY_LAST);
} else {
Debug("shared") << "=(" << asNode << std::endl;
}
diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h
index 0e2b885d9..88c6ca94a 100644
--- a/src/prop/theory_proxy.h
+++ b/src/prop/theory_proxy.h
@@ -1,13 +1,13 @@
/********************* */
/*! \file theory_proxy.h
** \verbatim
- ** Original author: Dejan Jovanovic
- ** Major contributors: Liana Hadarean, Kshitij Bansal, Morgan Deters
- ** Minor contributors (to current version): Christopher L. Conway, Tim King
+ ** Top contributors (to current version):
+ ** Tim King, Morgan Deters, Dejan Jovanovic
** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2014 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
+ ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
**
** \brief SAT Solver.
**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback