8000 Add ProofRule::CHAIN_M_RESOLUTION, disabled by default by ajreynol · Pull Request #11984 · cvc5/cvc5 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Add ProofRule::CHAIN_M_RESOLUTION, disabled by default #11984

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Add ProofRule::CHAIN_M_RESOLUTION, disabled by default #11984

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8c8bf98
More
ajreynol Jun 16, 2025
bec8d5d
More
ajreynol Jun 16, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
27 changes: 27 additions & 0 deletions include/cvc5/cvc5_proof_rule.h
View file 8000
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -584,6 +584,33 @@ enum ENUM(ProofRule)
* \endverbatim
*/
EVALUE(MACRO_RESOLUTION_TRUST),
/**
* \verbatim embed:rst:leading-asterisk
* **Boolean -- Chain multiset resolution**
*
* This rule combines Resolution + Factoring + Reordering.
*
* .. math::
* \inferrule{C_1 \dots C_n \mid C, (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C}
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

$$\frac{C_1 \dots C_n \mid C, (pol_1 \dots pol_{n-1}), (L_1 \dots L_{n-1})}{C}$$

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is this a suggestion? Or just a comment?

Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just a comment.

*
* where
*
* - let :math:`C_1 \dots C_n` be nodes viewed as clauses, as defined in
* :cpp:enumerator:`RESOLUTION <cvc5::ProofRule::RESOLUTION>`
* - let :math:`C_1 \diamond_{L,\mathit{pol}} C_2` represent the resolution of
* :math:`C_1` with :math:`C_2` with pivot :math:`L` and polarity
* :math:`pol`, as defined in
* :cpp:enumerator:`RESOLUTION <cvc5::ProofRule::RESOLUTION>`
* - let :math:`C_1'` be equal, in its set representation, to :math:`C_1`,
* - for each :math:`i > 1`, let :math:`C_i'` be equal, in its set
* representation, to :math:`C_{i-1} \diamond_{L_{i-1},\mathit{pol}_{i-1}}
* C_i'`
*
* The result of the chain resolution is :math:`C`, which is equal, in its set
* representation, to :math:`C_n'`.
* \endverbatim
*/
EVALUE(CHAIN_M_RESOLUTION),

/**
* \verbatim embed:rst:leading-asterisk
Expand Down
1 change: 1 addition & 0 deletions src/api/cpp/cvc5_proof_rule_template.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -53,6 +53,7 @@ const char* toString(ProofRule rule)
case ProofRule::REORDERING: return "REORDERING";
case ProofRule::MACRO_RESOLUTION: return "MACRO_RESOLUTION";
case ProofRule::MACRO_RESOLUTION_TRUST: return "MACRO_RESOLUTION_TRUST";
case ProofRule::CHAIN_M_RESOLUTION: return "CHAIN_M_RESOLUTION";
case ProofRule::SPLIT: return "SPLIT";
case ProofRule::EQ_RESOLVE: return "EQ_RESOLVE";
case ProofRule::MODUS_PONENS: return "MODUS_PONENS";
Expand Down
8 changes: 8 additions & 0 deletions src/options/proof_options.toml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -127,6 +127,14 @@ name = "Proof"
default = "5"
help = "the matching recursion limit for reconstructing proofs of theory rewrites"
< 10000 br>
[[option]]
name = "proofChainMRes"
category = "expert"
long = "proof-chain-m-res"
type = "bool"
default = "false"
help = "Use chain multiset resolution"

[[option]]
name = "proofRewriteRconsStepLimit"
category = "regular"
Expand Down
7 changes: 7 additions & 0 deletions src/smt/proof_post_processor.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -495,6 +495,13 @@ Node ProofPostprocessCallback::expandMacros(ProofRule id,
std::vector<Node> chainResArgs;
chainResArgs.push_back(nm->mkNode(Kind::SEXPR, pols));
chainResArgs.push_back(nm->mkNode(Kind::SEXPR, lits));
if (options().proof.proofChainMRes)
{
chainResArgs.insert(chainResArgs.begin(), args[0]);
cdp->addStep(
args[0], ProofRule::CHAIN_M_RESOLUTION, children, chainResArgs);
return args[0];
}
Node chainConclusion = d_pc->checkDebug(
ProofRule::CHAIN_RESOLUTION, children, chainResArgs, Node::null(), "");
Trace("smt-proof-pp-debug") << "Original conclusion: " << args[0] << "\n";
Expand Down
22 changes: 16 additions & 6 deletions src/theory/booleans/proof_checker.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,6 +33,7 @@ void BoolProofRuleChecker::registerTo(ProofChecker* pc)
pc->registerChecker(ProofRule::CHAIN_RESOLUTION, this);
pc->registerTrustedChecker(ProofRule::MACRO_RESOLUTION_TRUST, this, 3);
pc->registerChecker(ProofRule::MACRO_RESOLUTION, this);
pc->registerChecker(ProofRule::CHAIN_M_RESOLUTION, this);
pc->registerChecker(ProofRule::FACTORING, this);
pc->registerChecker(ProofRule::REORDERING, this);
pc->registerChecker(ProofRule::EQ_RESOLVE, this);
Expand Down Expand Up @@ -303,23 +304,32 @@ Node BoolProofRuleChecker::checkInternal(ProofRule id,
Assert(args.size() == 2 * (children.size() - 1) + 1);
return args[0];
}
if (id == ProofRule::MACRO_RESOLUTION)
if (id == ProofRule::MACRO_RESOLUTION || id == ProofRule::CHAIN_M_RESOLUTION)
{
Assert(children.size() > 1);
Assert(args.size() == 2 * (children.size() - 1) + 1);
Trace("bool-pfcheck") << "macro_res: " << args[0] << "\n" << push;
NodeManager* nm = nodeManager();
Node trueNode = nm->mkConst(true);
Node falseNode = nm->mkConst(false);
std::vector<Node> lhsClause, rhsClause;
Node lhsElim, rhsElim;
std::vector<Node> pols, lits;
for (size_t i = 1, nargs = args.size(); i < nargs; i = i + 2)
if (id == ProofRule::MACRO_RESOLUTION)
{
pols.push_back(args[i]);
lits.push_back(args[i + 1]);
Assert(args.size() == 2 * (children.size() - 1) + 1);
for (size_t i = 1, nargs = args.size(); i < nargs; i = i + 2)
{
pols.push_back(args[i]);
lits.push_back(args[i + 1]);
}
}
else
{
Assert(args.size() == 3);
Assert (id==ProofRule::CHAIN_M_RESOLUTION);
pols.insert(pols.end(), args[1].begin(), args[1].end());
lits.insert(lits.end(), args[2].begin(), args[2].end());
}

if (children[0].getKind() != Kind::OR
|| (pols[0] == trueNode && children[0] == lits[0])
|| (pols[0] == falseNode && children[0] == lits[0].notNode()))
Expand Down
Loading
0