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 the theory of quantifiers.
11 : : */
12 : :
13 : : #include "theory/quantifiers/theory_quantifiers.h"
14 : :
15 : : #include "options/quantifiers_options.h"
16 : : #include "proof/proof_node_manager.h"
17 : : #include "theory/quantifiers/quantifiers_macros.h"
18 : : #include "theory/quantifiers/quantifiers_modules.h"
19 : : #include "theory/quantifiers/quantifiers_rewriter.h"
20 : : #include "theory/trust_substitutions.h"
21 : : #include "theory/valuation.h"
22 : :
23 : : using namespace cvc5::internal::kind;
24 : : using namespace cvc5::context;
25 : :
26 : : namespace cvc5::internal {
27 : : namespace theory {
28 : : namespace quantifiers {
29 : :
30 : 51092 : TheoryQuantifiers::TheoryQuantifiers(Env& env,
31 : : OutputChannel& out,
32 : 51092 : Valuation valuation)
33 : : : Theory(THEORY_QUANTIFIERS, env, out, valuation),
34 : 51092 : d_rewriter(nodeManager(), env.getRewriter(), options()),
35 : 51092 : d_checker(nodeManager()),
36 : 51092 : d_qstate(env, valuation, logicInfo()),
37 : 51092 : d_qreg(env),
38 : 51092 : d_treg(env, d_qstate, d_qreg),
39 : 51092 : d_qim(env, *this, d_qstate, d_qreg, d_treg),
40 : 102184 : d_qengine(nullptr)
41 : : {
42 : : // construct the quantifiers engine
43 : 51092 : d_qengine.reset(
44 : 51092 : new QuantifiersEngine(env, d_qstate, d_qreg, d_treg, d_qim, d_pnm));
45 : :
46 : : // indicate we are using the quantifiers theory state object
47 : 51092 : d_theoryState = &d_qstate;
48 : : // use the inference manager as the official inference manager
49 : 51092 : d_inferManager = &d_qim;
50 : : // Set the pointer to the quantifiers engine, which this theory owns. This
51 : : // pointer will be retreived by TheoryEngine and set to all theories
52 : : // post-construction.
53 : 51092 : d_quantEngine = d_qengine.get();
54 : :
55 [ + + ]: 51092 : if (options().quantifiers.macrosQuant)
56 : : {
57 : 40 : d_qmacros.reset(new QuantifiersMacros(env, d_qreg));
58 : : }
59 : 51092 : }
60 : :
61 : 101488 : TheoryQuantifiers::~TheoryQuantifiers() {}
62 : :
63 : 51092 : TheoryRewriter* TheoryQuantifiers::getTheoryRewriter() { return &d_rewriter; }
64 : :
65 : 19899 : ProofRuleChecker* TheoryQuantifiers::getProofChecker() { return &d_checker; }
66 : :
67 : 51092 : void TheoryQuantifiers::finishInit()
68 : : {
69 : : // quantifiers are not evaluated in getModelValue
70 : 51092 : d_valuation.setUnevaluatedKind(Kind::EXISTS);
71 : 51092 : d_valuation.setUnevaluatedKind(Kind::FORALL);
72 : : // witness is used in several instantiation strategies
73 : 51092 : d_valuation.setUnevaluatedKind(Kind::WITNESS);
74 : 51092 : }
75 : :
76 : 51092 : bool TheoryQuantifiers::needsEqualityEngine(EeSetupInfo& esi)
77 : : {
78 : : // use the master equality engine
79 : 51092 : esi.d_useMaster = true;
80 : 51092 : return true;
81 : : }
82 : :
83 : 66756 : void TheoryQuantifiers::preRegisterTerm(TNode n)
84 : : {
85 [ - + ]: 66756 : if (n.getKind() != Kind::FORALL)
86 : : {
87 : 0 : return;
88 : : }
89 [ + - ]: 133512 : Trace("quantifiers-prereg")
90 : 66756 : << "TheoryQuantifiers::preRegisterTerm() " << n << std::endl;
91 : : // Preregister the quantified formula.
92 : : // This initializes the modules used for handling n in this user context.
93 : 66756 : getQuantifiersEngine()->preRegisterQuantifier(n);
94 [ + - ]: 133512 : Trace("quantifiers-prereg")
95 : 66756 : << "TheoryQuantifiers::preRegisterTerm() done " << n << std::endl;
96 : : }
97 : :
98 : 50519 : void TheoryQuantifiers::presolve()
99 : : {
100 [ + - ]: 50519 : Trace("quantifiers-presolve") << "TheoryQuantifiers::presolve()" << std::endl;
101 [ + + ]: 50519 : if (getQuantifiersEngine())
102 : : {
103 : 40147 : getQuantifiersEngine()->presolve();
104 : : }
105 : 50519 : }
106 : :
107 : 43449 : bool TheoryQuantifiers::ppAssert(TrustNode tin,
108 : : TrustSubstitutionMap& outSubstitutions)
109 : : {
110 [ + + ]: 43449 : if (d_qmacros != nullptr)
111 : : {
112 : : bool reqGround =
113 : 71 : options().quantifiers.macrosQuantMode != options::MacrosQuantMode::ALL;
114 : 71 : Node eq = d_qmacros->solve(tin.getProven(), reqGround);
115 [ + + ]: 71 : if (!eq.isNull())
116 : : {
117 : : // must be legal
118 [ + - ]: 38 : if (d_valuation.isLegalElimination(eq[0], eq[1]))
119 : : {
120 : : // add substitution solved, which ensures we track that eq depends on
121 : : // tin, which can impact unsat cores.
122 : 38 : outSubstitutions.addSubstitutionSolved(eq[0], eq[1], tin);
123 : 38 : return true;
124 : : }
125 : : }
126 [ + + ]: 71 : }
127 : 43411 : return false;
128 : : }
129 : :
130 : 65677 : void TheoryQuantifiers::ppNotifyAssertions(const std::vector<Node>& assertions)
131 : : {
132 [ + - ]: 131354 : Trace("quantifiers-presolve")
133 : 65677 : << "TheoryQuantifiers::ppNotifyAssertions" << std::endl;
134 [ + + ]: 65677 : if (getQuantifiersEngine())
135 : : {
136 : 49741 : getQuantifiersEngine()->ppNotifyAssertions(assertions);
137 : : }
138 : 65677 : }
139 : :
140 : 34077 : bool TheoryQuantifiers::collectModelValues(
141 : : TheoryModel* m, CVC5_UNUSED const std::set<Node>& termSet)
142 : : {
143 [ + + ]: 115444 : for (assertions_iterator i = facts_begin(); i != facts_end(); ++i)
144 : : {
145 [ + + ]: 81367 : if ((*i).d_assertion.getKind() == Kind::NOT)
146 : : {
147 [ + - ]: 21986 : Trace("quantifiers::collectModelInfo")
148 [ - + ][ - - ]: 10993 : << "got quant FALSE: " << (*i).d_assertion[0] << std::endl;
149 [ - + ]: 10993 : if (!m->assertPredicate((*i).d_assertion[0], false))
150 : : {
151 : 0 : return false;
152 : : }
153 : : }
154 : : else
155 : : {
156 [ + - ]: 140748 : Trace("quantifiers::collectModelInfo")
157 : 70374 : << "got quant TRUE : " << *i << std::endl;
158 [ - + ]: 70374 : if (!m->assertPredicate(*i, true))
159 : : {
160 : 0 : return false;
161 : : }
162 : : }
163 : : }
164 : 34077 : return true;
165 : : }
166 : :
167 : 186380 : void TheoryQuantifiers::postCheck(Effort level)
168 : : {
169 : : // call the quantifiers engine to check
170 : 186380 : getQuantifiersEngine()->check(level);
171 : 186380 : }
172 : :
173 : 143221 : bool TheoryQuantifiers::preNotifyFact(TNode atom,
174 : : bool polarity,
175 : : TNode fact,
176 : : CVC5_UNUSED bool isPrereg,
177 : : CVC5_UNUSED bool isInternal)
178 : : {
179 : 143221 : Kind k = atom.getKind();
180 [ + - ]: 143221 : if (k == Kind::FORALL)
181 : : {
182 : 143221 : getQuantifiersEngine()->assertQuantifier(atom, polarity);
183 : : }
184 : : else
185 : : {
186 : 0 : Unhandled() << "Unexpected fact " << fact;
187 : : }
188 : : // don't use equality engine, always return true
189 : 143221 : return true;
190 : : }
191 : :
192 : : } // namespace quantifiers
193 : : } // namespace theory
194 : : } // namespace cvc5::internal
|
