// literals, which could themselves add crowding literals.
if (chainConclusion == args[0])
{
+ Trace("smt-proof-pp-debug") << "..same conclusion, DONE.\n";
cdp->addStep(
chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);
return chainConclusion;
// chain.
if (chainConclusionLitsSet != conclusionLitsSet)
{
+ Trace("smt-proof-pp-debug") << "..need to eliminate crowding lits.\n";
chainConclusion = eliminateCrowdingLits(
chainConclusionLits, conclusionLits, children, args, cdp);
// update vector of lits. Note that the set is no longer used, so we don't
}
else
{
+ Trace("smt-proof-pp-debug") << "..add chainRes step directly.\n";
cdp->addStep(
chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);
}
// factoring
if (chainConclusionLits.size() != conclusionLits.size())
{
+ Trace("smt-proof-pp-debug") << "..add factoring step.\n";
// We build it rather than taking conclusionLits because the order may be
// different
std::vector<Node> factoredLits;
// reordering
if (n != args[0])
{
+ Trace("smt-proof-pp-debug") << "..add reordering step.\n";
cdp->addStep(args[0], PfRule::REORDERING, {n}, {args[0]});
}
return args[0];
NodeManager* nm = NodeManager::currentNM();
Node trueNode = nm->mkConst(true);
Node falseNode = nm->mkConst(false);
- std::vector<Node> clauseNodes;
- for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize;
- ++i)
+ // The lhs and rhs clauses in a binary resolution step, respectively. Since
+ // children correspond to the premises in the resolution chain, the first
+ // lhs clause is the first premise, the first rhs clause is the second
+ // premise. Each subsequent lhs clause will be the result of the previous
+ // binary resolution step in the chain, while each subsequent rhs clause
+ // will be respectively the second, third etc premises.
+ std::vector<Node> lhsClause, rhsClause;
+ // The pivots to be eliminated to the lhs clause and rhs clause in a binary
+ // resolution step, respectively
+ Node lhsElim, rhsElim;
+ // Get lhsClause of first resolution.
+ //
+ // Since a Node cannot hold an OR with a single child we need to
+ // disambiguate singleton clauses that are OR nodes from non-singleton
+ // clauses (i.e. unit clauses in the SAT solver).
+ //
+ // If the child is not an OR, it is a singleton clause and we take the
+ // child itself as the clause. Otherwise the child can only be a singleton
+ // clause if the child itself is used as a resolution literal, i.e. if the
+ // first child equal to the first pivot (which is args[1] or
+ // args[1].notNote() depending on the polarity).
+ if (children[0].getKind() != kind::OR
+ || (args[0] == trueNode && children[0] == args[1])
+ || (args[0] == falseNode && children[0] == args[1].notNode()))
+ {
+ lhsClause.push_back(children[0]);
+ }
+ else
{
- // Literals to be removed from the current clause, according to this
- // clause being in the lhs or the rhs of a resolution. The first clause
- // has no rhsElim and the last clause has no lhsElim. The literal to be
- // eliminated depends ond the pivot and the polarity stored in the
- // arguments.
- Node lhsElim = Node::null();
- Node rhsElim = Node::null();
- if (i < childrenSize - 1)
+ lhsClause.insert(lhsClause.end(), children[0].begin(), children[0].end());
+ }
+ // Traverse the links, which amounts to for each pair of args removing a
+ // literal from the lhs and a literal from the lhs.
+ for (size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2)
+ {
+ // Polarity determines how the pivot occurs in lhs and rhs
+ if (args[i] == trueNode)
{
- std::size_t index = 2 * i;
- lhsElim = args[index] == trueNode ? args[index + 1]
- : args[index + 1].notNode();
- Trace("bool-pfcheck") << i << ": lhsElim: " << lhsElim << "\n";
+ lhsElim = args[i + 1];
+ rhsElim = args[i + 1].notNode();
}
- if (i > 0)
+ else
{
- std::size_t index = 2 * (i - 1);
- rhsElim = args[index] == trueNode ? args[index + 1].notNode()
- : args[index + 1];
- Trace("bool-pfcheck") << i << ": rhsElim: " << rhsElim << "\n";
+ Assert(args[i] == falseNode);
+ lhsElim = args[i + 1].notNode();
+ rhsElim = args[i + 1];
}
- // The current set of literals is what we had before plus those in the
- // current child.
- //
- // Since a Node cannot hold an OR with a single child we need to
- // disambiguate singleton clauses that are OR nodes from non-singleton
- // clauses (i.e. unit clauses in the SAT solver).
- //
- // If the child is not an OR, it is a singleton clause and we take the
- // child itself as the clause. Otherwise the child can only be a singleton
- // clause if the child itself is used as a resolution literal, i.e. if the
- // child equal to the lhsElim or to the rhsElim (which means that the
- // negation of the child is in lhsElim).
- std::vector<Node> lits{clauseNodes};
- if (children[i].getKind() == kind::OR && children[i] != lhsElim
- && children[i] != rhsElim)
+ // The index of the child corresponding to the current rhs clause
+ size_t childIndex = i / 2 + 1;
+ // Get rhs clause. It's a singleton if not an OR node or if equal to
+ // rhsElim
+ if (children[childIndex].getKind() != kind::OR
+ || children[childIndex] == rhsElim)
{
- lits.insert(lits.end(), children[i].begin(), children[i].end());
+ rhsClause.push_back(children[childIndex]);
}
else
{
- lits.push_back(children[i]);
+ rhsClause = {children[childIndex].begin(), children[childIndex].end()};
}
- Trace("bool-pfcheck") << i << ": clause lits: " << lits << "\n";
- // We now compute the set of literals minus those to be eliminated in this
- // step
- std::vector<Node> curr;
- for (std::size_t j = 0, size = lits.size(); j < size; ++j)
- {
- if (lits[j] == lhsElim)
- {
- lhsElim = Node::null();
- Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n";
- continue;
- }
- if (lits[j] == rhsElim)
- {
- rhsElim = Node::null();
- Trace("bool-pfcheck") << "\t removed lit: " << lits[j] << "\n";
- continue;
- }
- curr.push_back(lits[j]);
- }
- Trace("bool-pfcheck") << "\n";
- clauseNodes.clear();
- clauseNodes.insert(clauseNodes.end(), curr.begin(), curr.end());
- }
- Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n" << pop;
- return nm->mkOr(clauseNodes);
+ Trace("bool-pfcheck") << i / 2 << "-th res link:\n";
+ Trace("bool-pfcheck") << "\t - lhsClause: " << lhsClause << "\n";
+ Trace("bool-pfcheck") << "\t\t - lhsElim: " << lhsElim << "\n";
+ Trace("bool-pfcheck") << "\t - rhsClause: " << rhsClause << "\n";
+ Trace("bool-pfcheck") << "\t\t - rhsElim: " << rhsElim << "\n";
+ // Compute the resulting clause, which will be the next lhsClause, as
+ // follows:
+ // - remove lhsElim from lhsClause
+ // - remove rhsElim from rhsClause and add the lits to lhsClause
+ auto itlhs = std::find(lhsClause.begin(), lhsClause.end(), lhsElim);
+ AlwaysAssert(itlhs != lhsClause.end());
+ lhsClause.erase(itlhs);
+ Trace("bool-pfcheck") << "\t.. after lhsClause: " << lhsClause << "\n";
+ auto itrhs = std::find(rhsClause.begin(), rhsClause.end(), rhsElim);
+ AlwaysAssert(itrhs != rhsClause.end());
+ lhsClause.insert(lhsClause.end(), rhsClause.begin(), itrhs);
+ lhsClause.insert(lhsClause.end(), itrhs + 1, rhsClause.end());
+ Trace("bool-pfcheck") << "\t.. after rhsClause: " << lhsClause << "\n";
+ rhsClause.clear();
+ }
+ Trace("bool-pfcheck") << "\n resulting clause: " << lhsClause << "\n"
+ << pop;
+ return nm->mkOr(lhsClause);
}
if (id == PfRule::MACRO_RESOLUTION_TRUST)
{
projects / cvc5.git / commitdiff