For some benchmarks, checking MACRO_RESOLUTION can be up to 80% (!!!) of the running time. This commit introduces a new rule that does not perform checking. The old rule and checker are kept for ground truth. Some miscellaneous minor changes are also made in the PR.
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;
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)
// 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
// 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
// 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
d_assumptions(userContext),
d_conflictLit(undefSatVariable)
{
+ d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
}
}
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};
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 << "] ";
}
// 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
// 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)
{
// 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());
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
// 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)
// 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])
// 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());
}
// 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
/** 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.
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)
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()};
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);
: 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);
projects / cvc5.git / commitdiff