Skip to content

Commit

Permalink
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Cycle rule
Browse files Browse the repository at this point in the history
ajreynol committed Nov 16, 2024
1 parent ef0dc50 commit 8065f69
Showing 4 changed files with 78 additions and 1 deletion.
13 changes: 13 additions & 0 deletions include/cvc5/cvc5_proof_rule.h
Original file line number Diff line number Diff line change
@@ -2677,6 +2677,19 @@ enum ENUM(ProofRewriteRule)
* \endverbatim
*/
EVALUE(DT_CONS_EQ),
/**
* \verbatim embed:rst:leading-asterisk
* **Datatypes -- cycle**
*
* .. math::
* (x = t[x]) = \bot
*
* where all terms on the path to :math:`x` in :math:`t[x]` are applications
* of constructors, and this path is non-empty.
*
* \endverbatim
*/
EVALUE(DT_CYCLE),
/**
* \verbatim embed:rst:leading-asterisk
* **Datatypes -- collapse tester**
1 change: 1 addition & 0 deletions src/api/cpp/cvc5_proof_rule_template.cpp
Original file line number Diff line number Diff line change
@@ -257,6 +257,7 @@ const char* toString(cvc5::ProofRewriteRule rule)
case ProofRewriteRule::DT_COLLAPSE_TESTER_SINGLETON:
return "dt-collapse-tester-singleton";
case ProofRewriteRule::DT_CONS_EQ: return "dt-cons-eq";
case ProofRewriteRule::DT_CYCLE: return "dt-cycle";
case ProofRewriteRule::DT_COLLAPSE_UPDATER: return "dt-collapse-updater";
case ProofRewriteRule::DT_UPDATER_ELIM: return "dt-updater-elim";
case ProofRewriteRule::DT_MATCH_ELIM: return "dt-match-elim";
30 changes: 30 additions & 0 deletions src/theory/datatypes/datatypes_rewriter.cpp
Original file line number Diff line number Diff line change
@@ -57,6 +57,8 @@ DatatypesRewriter::DatatypesRewriter(NodeManager* nm,
TheoryRewriteCtx::PRE_DSL);
registerProofRewriteRule(ProofRewriteRule::DT_MATCH_ELIM,
TheoryRewriteCtx::PRE_DSL);
registerProofRewriteRule(ProofRewriteRule::DT_CYCLE,
TheoryRewriteCtx::PRE_DSL);
}

Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
@@ -184,6 +186,34 @@ Node DatatypesRewriter::rewriteViaRule(ProofRewriteRule id, const Node& n)
}
}
break;
case ProofRewriteRule::DT_CYCLE:
{
if (n.getKind() == Kind::EQUAL && n[0] != n[1])
{
std::unordered_set<TNode> visited;
std::vector<TNode> visit;
TNode cur;
visit.push_back(n[1]);
do
{
cur = visit.back();
visit.pop_back();
if (visited.find(cur) == visited.end())
{
visited.insert(cur);
if (cur == n[0])
{
return d_nm->mkConst(false);
}
if (cur.getKind() == Kind::APPLY_CONSTRUCTOR)
{
visit.insert(visit.end(), cur.begin(), cur.end());
}
}
} while (!visit.empty());
}
}
break;
default: break;
}
return Node::null();
35 changes: 34 additions & 1 deletion src/theory/datatypes/infer_proof_cons.cpp
Original file line number Diff line number Diff line change
@@ -317,9 +317,42 @@ void InferProofCons::convert(InferenceId infer, TNode conc, TNode exp, CDProof*
}
}
break;
case InferenceId::DATATYPES_CYCLE:
{
Assert(!expv.empty());
Node lastEq = expv[expv.size() - 1];
Assert(lastEq.getKind() == Kind::EQUAL);
std::vector<Node> subs(expv.begin(), expv.begin() + expv.size() - 1);
ProofChecker* pc = d_env.getProofNodeManager()->getChecker();
Node eq;
if (!subs.empty())
{
eq = pc->checkDebug(ProofRule::SUBS, subs, {lastEq[1]});
Assert(!eq.isNull());
cdp->addStep(eq, ProofRule::SUBS, subs, {lastEq[1]});
}
else
{
eq = lastEq[1].eqNode(lastEq[1]);
}
Node eq1 = lastEq[0].eqNode(eq[1]);
Trace("dt-ipc-cycle") << "Cycle eq? " << eq1 << std::endl;
Node falsen =
d_env.getRewriter()->rewriteViaRule(ProofRewriteRule::DT_CYCLE, eq1);
if (!falsen.isNull())
{
Node eqq = eq1.eqNode(falsen);
cdp->addTheoryRewriteStep(eqq, ProofRewriteRule::DT_CYCLE);
cdp->addStep(falsen, ProofRule::EQ_RESOLVE, {eq1, eqq}, {});
if (eq1 != lastEq)
{
cdp->addStep(eq1, ProofRule::TRANS, {lastEq, eq}, {});
}
}
}
break;
// inferences currently not supported
case InferenceId::DATATYPES_BISIMILAR:
case InferenceId::DATATYPES_CYCLE:
default:
Trace("dt-ipc") << "...no conversion for inference " << infer
<< std::endl;

0 comments on commit 8065f69

Please sign in to comment.