summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/expr/lazy_proof_chain.cpp13
-rw-r--r--src/expr/proof_rule.h12
-rw-r--r--src/prop/sat_proof_manager.cpp18
-rw-r--r--src/prop/sat_proof_manager.h3
-rw-r--r--src/smt/proof_manager.cpp1
-rw-r--r--src/smt/proof_post_processor.cpp3
-rw-r--r--src/theory/booleans/proof_checker.cpp7
7 files changed, 39 insertions, 18 deletions
diff --git a/src/expr/lazy_proof_chain.cpp b/src/expr/lazy_proof_chain.cpp
index 7f14adc38..5e638b55f 100644
--- a/src/expr/lazy_proof_chain.cpp
+++ b/src/expr/lazy_proof_chain.cpp
@@ -67,7 +67,7 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
std::vector<std::shared_ptr<ProofNode>>,
NodeHashFunction>
assumptionsToExpand;
- // invariant of the loop below, the first iteration notwhistanding:
+ // invariant of the loop below, the first iteration notwithstanding:
// visit = domain(assumptionsToExpand) \ domain(toConnect)
std::vector<Node> visit{fact};
std::unordered_map<Node, bool, NodeHashFunction> visited;
@@ -121,13 +121,22 @@ std::shared_ptr<ProofNode> LazyCDProofChain::getProofFor(Node fact)
expr::getFreeAssumptionsMap(curPfn, famap);
if (Trace.isOn("lazy-cdproofchain"))
{
+ unsigned alreadyToVisit = 0;
Trace("lazy-cdproofchain")
- << "LazyCDProofChain::getProofFor: free assumptions:\n";
+ << "LazyCDProofChain::getProofFor: " << famap.size()
+ << " free assumptions:\n";
for (auto fap : famap)
{
Trace("lazy-cdproofchain")
<< "LazyCDProofChain::getProofFor: - " << fap.first << "\n";
+ alreadyToVisit +=
+ std::find(visit.begin(), visit.end(), fap.first) != visit.end()
+ ? 1
+ : 0;
}
+ Trace("lazy-cdproofchain")
+ << "LazyCDProofChain::getProofFor: " << alreadyToVisit
+ << " already to visit\n";
}
// mark for post-traversal if we are controlling cycles
if (d_cyclic)
diff --git a/src/expr/proof_rule.h b/src/expr/proof_rule.h
index 7e0fc31fe..cec85cc99 100644
--- a/src/expr/proof_rule.h
+++ b/src/expr/proof_rule.h
@@ -320,6 +320,8 @@ enum class PfRule : uint32_t
// The result of the chain resolution is C, which is equal, in its set
// representation, to C_n'
MACRO_RESOLUTION,
+ // As above but not checked
+ MACRO_RESOLUTION_TRUST,
// ======== Split
// Children: none
@@ -1048,8 +1050,9 @@ enum class PfRule : uint32_t
// its ki is negative). >< is always one of <, <=
// NB: this implies that lower bounds must have negative ki,
// and upper bounds must have positive ki.
- // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n * poly_n)
- // t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n * const_n)
+ // t1 is the sum of the scaled polynomials (k_1 * poly_1 + ... + k_n *
+ // poly_n) t2 is the sum of the scaled constants (k_1 * const_1 + ... + k_n
+ // * const_n)
ARITH_SCALE_SUM_UPPER_BOUNDS,
// ======== Sum Upper Bounds
@@ -1134,8 +1137,9 @@ enum class PfRule : uint32_t
// Arguments: (t, x, y, a, b, sgn)
// ---------------------
// Conclusion:
- // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y b)))
- // sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a) (>= y b)))
+ // sgn=-1: (= (<= t tplane) (or (and (<= x a) (>= y b)) (and (>= x a) (<= y
+ // b))) sgn= 1: (= (>= t tplane) (or (and (<= x a) (<= y b)) (and (>= x a)
+ // (>= y b)))
// Where x,y are real terms (variables or extended terms), t = (* x y)
// (possibly under rewriting), a,b are real constants, and sgn is either -1
// or 1. tplane is the tangent plane of x*y at (a,b): b*x + a*y - a*b
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp
index da9354c2f..0d075de45 100644
--- a/src/prop/sat_proof_manager.cpp
+++ b/src/prop/sat_proof_manager.cpp
@@ -35,6 +35,7 @@ SatProofManager::SatProofManager(Minisat::Solver* solver,
d_assumptions(userContext),
d_conflictLit(undefSatVariable)
{
+ d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
@@ -169,7 +170,6 @@ void SatProofManager::endResChain(Node conclusion,
}
d_redundantLits.clear();
// build resolution chain
- NodeManager* nm = NodeManager::currentNM();
// the conclusion is stored already in the arguments because of the
// possibility of reordering
std::vector<Node> children, args{conclusion};
@@ -212,7 +212,7 @@ void SatProofManager::endResChain(Node conclusion,
Trace("sat-proof") << " : ";
if (i > 0)
{
- args.push_back(nm->mkConst(posFirst));
+ args.push_back(posFirst ? d_true : d_false);
args.push_back(pivot);
Trace("sat-proof") << "{" << posFirst << "} [" << pivot << "] ";
}
@@ -249,7 +249,7 @@ void SatProofManager::endResChain(Node conclusion,
// step, which bypasses these. Note that we could generate a chain resolution
// rule here by explicitly computing the detailed steps, but leave this for
// post-processing.
- ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
+ ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
d_resChainPg.addStep(conclusion, ps);
// the premises of this resolution may not have been justified yet, so we do
// not pass assumptions to check closedness
@@ -369,7 +369,6 @@ void SatProofManager::explainLit(
// SAT solver, we directly get the literals we need to explain so we no
// longer depend on the reference to reason
std::vector<Node> toExplain{children.back().begin(), children.back().end()};
- NodeManager* nm = NodeManager::currentNM();
Trace("sat-proof") << push;
for (unsigned i = 0; i < size; ++i)
{
@@ -397,7 +396,7 @@ void SatProofManager::explainLit(
// note this is the opposite of what is done in addResolutionStep. This is
// because here the clause, which contains the literal being analyzed, is
// the first clause rather than the second
- args.push_back(nm->mkConst(!negated));
+ args.push_back(!negated ? d_true : d_false);
args.push_back(negated ? currLitNode[0] : currLitNode);
// add child premises and the child itself
premises.insert(childPremises.begin(), childPremises.end());
@@ -429,7 +428,7 @@ void SatProofManager::explainLit(
Trace("sat-proof") << pop;
// create step
args.insert(args.begin(), litNode);
- ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
+ ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
d_resChainPg.addStep(litNode, ps);
// the premises in the limit of the justification may correspond to other
// links in the chain which have, themselves, literals yet to be justified. So
@@ -490,7 +489,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
// get resolution
Node cur = link.first;
std::shared_ptr<ProofNode> pfn = link.second;
- while (pfn->getRule() != PfRule::MACRO_RESOLUTION)
+ while (pfn->getRule() != PfRule::MACRO_RESOLUTION_TRUST)
{
Assert(pfn->getChildren().size() == 1
&& pfn->getChildren()[0]->getRule() == PfRule::ASSUME)
@@ -539,7 +538,6 @@ void SatProofManager::finalizeProof(Node inConflictNode,
// arguments for the resolution step to conclude false.
std::vector<Node> children{inConflictNode}, args;
std::unordered_set<TNode, TNodeHashFunction> premises;
- NodeManager* nm = NodeManager::currentNM();
for (unsigned i = 0, size = inConflict.size(); i < size; ++i)
{
Assert(d_cnfStream->getNodeCache().find(inConflict[i])
@@ -555,7 +553,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
// note this is the opposite of what is done in addResolutionStep. This is
// because here the clause, which contains the literal being analyzed, is
// the first clause rather than the second
- args.push_back(nm->mkConst(!negated));
+ args.push_back(!negated ? d_true : d_false);
args.push_back(negated ? litNode[0] : litNode);
// add child premises and the child itself
premises.insert(childPremises.begin(), childPremises.end());
@@ -578,7 +576,7 @@ void SatProofManager::finalizeProof(Node inConflictNode,
}
// create step
args.insert(args.begin(), d_false);
- ProofStep ps(PfRule::MACRO_RESOLUTION, children, args);
+ ProofStep ps(PfRule::MACRO_RESOLUTION_TRUST, children, args);
d_resChainPg.addStep(d_false, ps);
// not yet ready to check closedness because maybe only now we will justify
// literals used in resolutions
diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h
index 4d45ce3b7..6407939c7 100644
--- a/src/prop/sat_proof_manager.h
+++ b/src/prop/sat_proof_manager.h
@@ -561,7 +561,8 @@ class SatProofManager
/** The proof generator for resolution chains */
BufferedProofGenerator d_resChainPg;
- /** The false node */
+ /** The true/false nodes */
+ Node d_true;
Node d_false;
/** All clauses added to the SAT solver, kept in a context-dependent manner.
diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 846df7e41..549f10008 100644
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -64,6 +64,7 @@ PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_INTRO);
d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_ELIM);
d_pfpp->setEliminateRule(PfRule::MACRO_SR_PRED_TRANSFORM);
+ d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION_TRUST);
d_pfpp->setEliminateRule(PfRule::MACRO_RESOLUTION);
if (options::proofGranularityMode()
!= options::ProofGranularityMode::REWRITE)
diff --git a/src/smt/proof_post_processor.cpp b/src/smt/proof_post_processor.cpp
index a27a5697e..19ca089d3 100644
--- a/src/smt/proof_post_processor.cpp
+++ b/src/smt/proof_post_processor.cpp
@@ -648,7 +648,8 @@ Node ProofPostprocessCallback::expandMacros(PfRule id,
cdp->addStep(args[0], PfRule::EQ_RESOLVE, {children[0], eq}, {});
return args[0];
}
- else if (id == PfRule::MACRO_RESOLUTION)
+ else if (id == PfRule::MACRO_RESOLUTION
+ || id == PfRule::MACRO_RESOLUTION_TRUST)
{
// first generate the naive chain_resolution
std::vector<Node> chainResArgs{args.begin() + 1, args.end()};
diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp
index d6600f14d..6b9d3e44e 100644
--- a/src/theory/booleans/proof_checker.cpp
+++ b/src/theory/booleans/proof_checker.cpp
@@ -25,6 +25,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(PfRule::SPLIT, this);
pc->registerChecker(PfRule::RESOLUTION, this);
pc->registerChecker(PfRule::CHAIN_RESOLUTION, this);
+ pc->registerTrustedChecker(PfRule::MACRO_RESOLUTION_TRUST, this, 3);
pc->registerChecker(PfRule::MACRO_RESOLUTION, this);
pc->registerChecker(PfRule::FACTORING, this);
pc->registerChecker(PfRule::REORDERING, this);
@@ -299,6 +300,12 @@ Node BoolProofRuleChecker::checkInternal(PfRule id,
: clauseNodes.size() == 1 ? clauseNodes[0]
: nm->mkNode(kind::OR, clauseNodes);
}
+ if (id == PfRule::MACRO_RESOLUTION_TRUST)
+ {
+ Assert(children.size() > 1);
+ Assert(args.size() == 2 * (children.size() - 1) + 1);
+ return args[0];
+ }
if (id == PfRule::MACRO_RESOLUTION)
{
Assert(children.size() > 1);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback