Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Implementation of quantifiers proof checker.
11 : : */
12 : :
13 : : #include "theory/quantifiers/proof_checker.h"
14 : :
15 : : #include "expr/node_algorithm.h"
16 : : #include "expr/skolem_manager.h"
17 : : #include "proof/valid_witness_proof_generator.h"
18 : : #include "theory/builtin/proof_checker.h"
19 : : #include "theory/quantifiers/skolemize.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : :
23 : : namespace cvc5::internal {
24 : : namespace theory {
25 : : namespace quantifiers {
26 : :
27 : 49981 : QuantifiersProofRuleChecker::QuantifiersProofRuleChecker(NodeManager* nm)
28 : 49981 : : ProofRuleChecker(nm)
29 : : {
30 : 49981 : }
31 : :
32 : 18917 : void QuantifiersProofRuleChecker::registerTo(ProofChecker* pc)
33 : : {
34 : : // add checkers
35 : 18917 : pc->registerChecker(ProofRule::SKOLEM_INTRO, this);
36 : 18917 : pc->registerChecker(ProofRule::SKOLEMIZE, this);
37 : 18917 : pc->registerChecker(ProofRule::INSTANTIATE, this);
38 : 18917 : pc->registerChecker(ProofRule::ALPHA_EQUIV, this);
39 : 18917 : pc->registerChecker(ProofRule::QUANT_VAR_REORDERING, this);
40 : 18917 : pc->registerChecker(ProofRule::EXISTS_STRING_LENGTH, this);
41 : 18917 : }
42 : :
43 : 27110 : Node QuantifiersProofRuleChecker::checkInternal(
44 : : ProofRule id,
45 : : const std::vector<Node>& children,
46 : : const std::vector<Node>& args)
47 : : {
48 [ + + ]: 27110 : if (id == ProofRule::SKOLEM_INTRO)
49 : : {
50 [ - + ][ - + ]: 18236 : Assert(children.empty());
[ - - ]
51 [ - + ][ - + ]: 18236 : Assert(args.size() == 1);
[ - - ]
52 : 18236 : Node t = SkolemManager::getUnpurifiedForm(args[0]);
53 : 18236 : return args[0].eqNode(t);
54 : 18236 : }
55 [ + + ]: 8874 : else if (id == ProofRule::SKOLEMIZE)
56 : : {
57 [ - + ][ - + ]: 704 : Assert(children.size() == 1);
[ - - ]
58 [ - + ][ - + ]: 704 : Assert(args.empty());
[ - - ]
59 : : // must use negated FORALL
60 : 704 : if (children[0].getKind() != Kind::NOT
61 [ + - ][ - + ]: 1408 : || children[0][0].getKind() != Kind::FORALL)
[ + - ][ - + ]
[ - - ]
62 : : {
63 : 0 : return Node::null();
64 : : }
65 : 704 : Node q = children[0][0];
66 : 1408 : std::vector<Node> vars(q[0].begin(), q[0].end());
67 : 704 : std::vector<Node> skolems = Skolemize::getSkolemConstants(q);
68 : : Node res = q[1].substitute(
69 : 704 : vars.begin(), vars.end(), skolems.begin(), skolems.end());
70 : 704 : res = res.notNode();
71 : 704 : return res;
72 : 704 : }
73 [ + + ]: 8170 : else if (id == ProofRule::INSTANTIATE)
74 : : {
75 [ - + ][ - + ]: 4174 : Assert(children.size() == 1);
[ - - ]
76 : : // note we may have more arguments than just the term vector
77 [ + - ][ - + ]: 4174 : if (children[0].getKind() != Kind::FORALL || args.empty())
[ - + ]
78 : : {
79 : 0 : return Node::null();
80 : : }
81 : 4174 : if (args[0].getKind() != Kind::SEXPR
82 [ + - ][ - + ]: 8348 : || args[0].getNumChildren() != children[0][0].getNumChildren())
[ + - ][ - + ]
[ - - ]
83 : : {
84 : 0 : return Node::null();
85 : : }
86 : 4174 : Node body = children[0][1];
87 : 4174 : std::vector<Node> vars;
88 : 4174 : std::vector<Node> subs;
89 [ + + ]: 13779 : for (size_t i = 0, nc = children[0][0].getNumChildren(); i < nc; i++)
90 : : {
91 : 9605 : vars.push_back(children[0][0][i]);
92 : 9605 : subs.push_back(args[0][i]);
93 : : }
94 : : Node inst =
95 : 4174 : body.substitute(vars.begin(), vars.end(), subs.begin(), subs.end());
96 : 4174 : return inst;
97 : 4174 : }
98 [ + + ]: 3996 : else if (id == ProofRule::ALPHA_EQUIV)
99 : : {
100 [ - + ][ - + ]: 3861 : Assert(children.empty());
[ - - ]
101 [ - + ][ - + ]: 3861 : Assert(args.size() == 3);
[ - - ]
102 : : // must be lists of the same length
103 [ + - ]: 7722 : if (args[1].getKind() != Kind::SEXPR || args[2].getKind() != Kind::SEXPR
104 [ + - ][ - + ]: 7722 : || args[1].getNumChildren() != args[2].getNumChildren())
[ - + ]
105 : : {
106 : 0 : return Node::null();
107 : : }
108 : : // arguments must be lists of bound variables that are pairwise unique
109 [ + + ]: 23166 : std::unordered_set<Node> allVars[2];
110 : 3861 : std::vector<Node> vars;
111 : 3861 : std::vector<Node> newVars;
112 [ + + ]: 12217 : for (size_t i = 0, nargs = args[1].getNumChildren(); i < nargs; i++)
113 : : {
114 [ + + ]: 25068 : for (size_t j = 1; j <= 2; j++)
115 : : {
116 : 16712 : Node v = args[j][i];
117 : 16712 : std::unordered_set<Node>& av = allVars[j - 1];
118 [ + - ][ - + ]: 16712 : if (v.getKind() != Kind::BOUND_VARIABLE || av.find(v) != av.end())
[ - + ]
119 : : {
120 : 0 : return Node::null();
121 : : }
122 : 16712 : av.insert(v);
123 [ + - ]: 16712 : }
124 : 8356 : vars.push_back(args[1][i]);
125 : 8356 : newVars.push_back(args[2][i]);
126 : : }
127 : 3861 : Node renamedBody = args[0].substitute(
128 : 3861 : vars.begin(), vars.end(), newVars.begin(), newVars.end());
129 : 3861 : return args[0].eqNode(renamedBody);
130 [ + + ][ - - ]: 15444 : }
131 [ + + ]: 135 : else if (id == ProofRule::QUANT_VAR_REORDERING)
132 : : {
133 [ - + ][ - + ]: 125 : Assert(children.empty());
[ - - ]
134 [ - + ][ - + ]: 125 : Assert(args.size() == 1);
[ - - ]
135 : 125 : Node eq = args[0];
136 [ + - ][ - + ]: 250 : if (eq.getKind() != Kind::EQUAL || eq[0].getKind() != Kind::FORALL
[ - - ]
137 : 250 : || eq[1].getKind() != Kind::FORALL || eq[0][1] != eq[1][1])
138 : : {
139 : 0 : return Node::null();
140 : : }
141 : 250 : std::unordered_set<Node> varSet1(eq[0][0].begin(), eq[0][0].end());
142 : 250 : std::unordered_set<Node> varSet2(eq[1][0].begin(), eq[1][0].end());
143 : : // cannot have repetition
144 : 250 : if (varSet1.size() != eq[0][0].getNumChildren()
145 : 250 : || varSet2.size() != eq[1][0].getNumChildren())
146 : : {
147 : 0 : return Node::null();
148 : : }
149 [ - + ]: 125 : if (varSet1 != varSet2)
150 : : {
151 : 0 : return Node::null();
152 : : }
153 : 125 : return eq;
154 : 125 : }
155 [ + - ]: 10 : else if (id == ProofRule::EXISTS_STRING_LENGTH)
156 : : {
157 : 10 : Node k = ValidWitnessProofGenerator::mkSkolem(nodeManager(), id, args);
158 : : Node exists =
159 : 10 : ValidWitnessProofGenerator::mkAxiom(nodeManager(), k, id, args);
160 : 10 : return exists;
161 : 10 : }
162 : :
163 : : // no rule
164 : 0 : return Node::null();
165 : : }
166 : :
167 : : } // namespace quantifiers
168 : : } // namespace theory
169 : : } // namespace cvc5::internal
|
