Skip to content

Commit

Permalink
no longer use dedicate assume rule for Alethe backend
Browse files Browse the repository at this point in the history
  • Loading branch information
@HanielB
HanielB committed Feb 16, 2024
1 parent 3809b90 commit 46bab12
Show file tree
Hide file tree
Showing 2 changed files with 66 additions and 56 deletions.
58 changes: 33 additions & 25 deletions src/proof/alethe/alethe_post_processor.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -74,7 +74,10 @@ bool AletheProofPostprocessCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
bool AletheProofPostprocessCallback::shouldUpdatePost(
std::shared_ptr<ProofNode> pn, const std::vector<Node>& fa)
{
Assert(!pn->getArguments().empty());
if (pn->getArguments().empty())
{
return false;
}
AletheRule rule = getAletheRule(pn->getArguments()[0]);
return rule == AletheRule::RESOLUTION_OR || rule == AletheRule::REORDERING
|| rule == AletheRule::CONTRACTION;
Expand Down Expand Up @@ -176,6 +179,7 @@ bool AletheProofPostprocessCallback::update(Node res,
//
//================================================= Core rules
//======================== Assume and Scope
// nothing happens
case ProofRule::ASSUME:
{
return false;
Expand Down Expand Up @@ -2009,8 +2013,12 @@ bool AletheProofPostprocessCallback::maybeReplacePremiseProof(Node premise,
{
// This method is called only when the premise is used as a singleton
// clause. If its proof however concludes a non-singleton clause it'll fail
// the test below and we must change its proof.
// the test below and we must change its proof. Assumptions are ignored.
std::shared_ptr<ProofNode> premisePf = cdp->getProofFor(premise);
if (premisePf->getRule() == ProofRule::ASSUME)
{
return false;
}
Node premisePfConclusion = premisePf->getArguments()[2];
if (premisePfConclusion.getNumChildren() <= 2
|| premisePfConclusion[0] != d_cl)
Expand Down Expand Up @@ -2136,19 +2144,19 @@ bool AletheProofPostprocessCallback::updatePost(
&& (args[polIdx] != d_true || args[pivIdx] != children[0]))
{
std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
Node childConclusion = childPf->getArguments()[2];
AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
bool childPfIsAssume = childPf->getRule() == ProofRule::ASSUME;
Node childConclusion = childPfIsAssume? childPf->getResult() : childPf->getArguments()[2];
// if child conclusion is of the form (sexpr cl (or ...)), then we need
// to add an OR step, since this child must not be a singleton
if ((childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
&& childConclusion[1].getKind() == Kind::OR)
|| (childRule == AletheRule::ASSUME
&& childConclusion.getKind() == Kind::OR))
if ((childPfIsAssume && childConclusion.getKind() == Kind::OR)
|| (childConclusion.getNumChildren() == 2
&& childConclusion[0] == d_cl
&& childConclusion[1].getKind() == Kind::OR))
{
hasUpdated = true;
// Add or step
std::vector<Node> subterms{d_cl};
if (childRule == AletheRule::ASSUME)
if (childPfIsAssume)
{
subterms.insert(
subterms.end(), childConclusion.begin(), childConclusion.end());
Expand Down Expand Up @@ -2205,18 +2213,17 @@ bool AletheProofPostprocessCallback::updatePost(
continue;
}
std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[i]);
Node childConclusion = childPf->getArguments()[2];
AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
bool childPfIsAssume = childPf->getRule() == ProofRule::ASSUME;
Node childConclusion = childPfIsAssume? childPf->getResult() : childPf->getArguments()[2];
// Add or step
if ((childConclusion.getNumChildren() == 2
&& childConclusion[0] == d_cl
&& childConclusion[1].getKind() == Kind::OR)
|| (childRule == AletheRule::ASSUME
&& childConclusion.getKind() == Kind::OR))
if ((childPfIsAssume && childConclusion.getKind() == Kind::OR)
|| (childConclusion.getNumChildren() == 2
&& childConclusion[0] == d_cl
&& childConclusion[1].getKind() == Kind::OR))
{
hasUpdated = true;
std::vector<Node> lits{d_cl};
if (childRule == AletheRule::ASSUME)
if (childPfIsAssume)
{
lits.insert(
lits.end(), childConclusion.begin(), childConclusion.end());
Expand Down Expand Up @@ -2295,16 +2302,17 @@ bool AletheProofPostprocessCallback::updatePost(
case AletheRule::CONTRACTION:
{
std::shared_ptr<ProofNode> childPf = cdp->getProofFor(children[0]);
Node childConclusion = childPf->getArguments()[2];
AletheRule childRule = getAletheRule(childPf->getArguments()[0]);
if ((childConclusion.getNumChildren() == 2 && childConclusion[0] == d_cl
&& childConclusion[1].getKind() == Kind::OR)
|| (childRule == AletheRule::ASSUME
&& childConclusion.getKind() == Kind::OR))
bool childPfIsAssume = childPf->getRule() == ProofRule::ASSUME;
Node childConclusion =
childPfIsAssume ? childPf->getResult() : childPf->getArguments()[2];
if ((childPfIsAssume && childConclusion.getKind() == Kind::OR)
|| (childConclusion.getNumChildren() == 2
&& childConclusion[0] == d_cl
&& childConclusion[1].getKind() == Kind::OR))
{
// Add or step for child
std::vector<Node> subterms{d_cl};
if (getAletheRule(childPf->getArguments()[0]) == AletheRule::ASSUME)
if (childPfIsAssume)
{
subterms.insert(
subterms.end(), childConclusion.begin(), childConclusion.end());
Expand Down Expand Up @@ -2373,7 +2381,7 @@ bool AletheProofPostprocessCallback::finalStep(Node res,
if (childPf->getRule() == ProofRule::ALETHE_RULE
&& ((childPf->getArguments()[2].getNumChildren() == 2
&& childPf->getArguments()[2][1] == d_false)
|| childPf->getArguments()[2] == d_false))
|| childPf->getResult() == d_false))
{
Node notFalse =
nm->mkNode(Kind::SEXPR, d_cl, d_false.notNode()); // (cl (not false))
Expand Down
64 changes: 33 additions & 31 deletions src/proof/alethe/alethe_printer.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -37,12 +37,26 @@ bool LetUpdaterPfCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
const std::vector<Node>& fa,
bool& continueUpdate)
{
ProofRule r = pn->getRule();
if (r == ProofRule::ASSUME)
{
d_lbind.process(pn->getResult());
return false;
}
const std::vector<Node>& args = pn->getArguments();
if (r == ProofRule::SCOPE)
{
for (size_t i = 0, size = args.size(); i < size; ++i)
{
d_lbind.process(args[i]);
}
return false;
}
// Letification done on the converted terms (thus from the converted
// conclusion) and potentially on arguments, which means to ignore the first
// two arguments (which are the Alethe rule and the original conclusion).
AlwaysAssert(args.size() > 2)
<< "res: " << pn->getResult() << "\nid: " << getAletheRule(args[0]);
<< "res: " << pn->getResult() << "\nid: " << pn->getRule();
for (size_t i = 2, size = args.size(); i < size; ++i)
{
Trace("alethe-printer") << "Process " << args[i] << "\n";
Expand All @@ -60,7 +74,6 @@ bool LetUpdaterPfCallback::shouldUpdate(std::shared_ptr<ProofNode> pn,
}
d_lbind.process(args[i]);
}

return false;
}

Expand Down Expand Up @@ -89,6 +102,8 @@ void AletheProofPrinter::print(
const std::map<Node, std::string>& assertionNames)
{
Trace("alethe-printer") << "- Print proof in Alethe format. " << std::endl;
// ignore outer scope
pfn = pfn->getChildren()[0];
std::shared_ptr<ProofNode> innerPf = pfn->getChildren()[0];
AlwaysAssert(innerPf);

Expand Down Expand Up @@ -120,7 +135,7 @@ void AletheProofPrinter::print(
const std::vector<Node>& args = pfn->getArguments();
// Special handling for the first scope
// Print assumptions and add them to the list but do not print anchor.
for (size_t i = 3, size = args.size(); i < size; i++)
for (size_t i = 0, size = args.size(); i < size; i++)
{
auto it = assertionNames.find(args[i]);
if (it != assertionNames.end())
Expand All @@ -130,8 +145,8 @@ void AletheProofPrinter::print(
}
else
{ // assumptions are always being declared
out << "(assume a" << i - 3 << " ";
assumptions[args[i]] = "a" + std::to_string(i - 3);
out << "(assume a" << i << " ";
assumptions[args[i]] = "a" + std::to_string(i);
}
printTerm(out, args[i]);
out << ")\n";
Expand All @@ -153,38 +168,25 @@ std::string AletheProofPrinter::printInternal(
int step_id = current_step_id;
const std::vector<Node>& args = pfn->getArguments();

// If the proof node is untranslated a problem might have occured during
// postprocessing
if (args.size() < 3 || pfn->getRule() != ProofRule::ALETHE_RULE)
{
Trace("alethe-printer")
<< "... printing failed! Encountered untranslated Node. "
<< pfn->getResult() << " " << pfn->getRule() << " "
<< " / " << args << std::endl;
return "";
}

// Get the alethe proof rule
AletheRule arule = getAletheRule(args[0]);

// Assumptions are printed at the anchor and therefore have to be in the list
// of assumptions when an assume is reached.
if (arule == AletheRule::ASSUME)
// of assumptions when an assume is reached. Since assumptions are
// untranslated, it's handled as a special case here.
if (pfn->getRule() == ProofRule::ASSUME)
{
Trace("alethe-printer")
<< "... reached assumption " << pfn->getResult() << " " << arule << " "
<< " / " << args << " " << std::endl;

auto it = assumptions.find(args[2]);
Assert(it != assumptions.end())
<< "Assumption has not been printed yet! " << args[2] << "/"
<< assumptions << std::endl;
Trace("alethe-printer")
<< "... found assumption in list " << it->second << ": " << args[2]
<< "/" << assumptions << std::endl;
<< "... reached assumption " << pfn->getResult() << std::endl;
Node res = pfn->getResult();

auto it = assumptions.find(res);
Assert(it != assumptions.end()) << "Assumption has not been printed yet! "
<< res << "/" << assumptions << std::endl;
Trace("alethe-printer") << "... found assumption in list " << it->second
<< ": " << res << "/" << assumptions << std::endl;
return it->second;
}

// Get the alethe proof rule
AletheRule arule = getAletheRule(args[0]);
// If the current step is already printed return its id
auto it = steps.find(pfn);
if (it != steps.end())
Expand Down

0 comments on commit 46bab12

Please sign in to comment.