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 : : * [[ Add one-line brief description here ]]
11 : : *
12 : : * [[ Add lengthier description here ]]
13 : : * \todo document this file
14 : : */
15 : :
16 : : #include "theory/arith/linear/callbacks.h"
17 : :
18 : : #include "expr/skolem_manager.h"
19 : : #include "proof/proof_node.h"
20 : : #include "theory/arith/linear/theory_arith_private.h"
21 : :
22 : : namespace cvc5::internal {
23 : : namespace theory {
24 : : namespace arith::linear {
25 : :
26 : 28697 : SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta) : d_arith(ta)
27 : : {
28 : 28697 : }
29 : 40193 : void SetupLiteralCallBack::operator()(TNode lit)
30 : : {
31 [ + + ]: 40193 : TNode atom = (lit.getKind() == Kind::NOT) ? lit[0] : lit;
32 [ + - ]: 40193 : if (!d_arith.isSetup(atom))
33 : : {
34 : 40193 : d_arith.setupAtom(atom);
35 : : }
36 : 40193 : }
37 : :
38 : 28697 : DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
39 : 28697 : : d_ta(ta)
40 : : {
41 : 28697 : }
42 : 100943 : Rational DeltaComputeCallback::operator()() const
43 : : {
44 : 100943 : return d_ta.deltaValueForTotalOrder();
45 : : }
46 : :
47 : 114788 : TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta) : d_ta(ta) {}
48 : 4096 : ArithVar TempVarMalloc::request()
49 : : {
50 : 4096 : NodeManager* nm = d_ta.getNodeManager();
51 : 8192 : Node skolem = NodeManager::mkDummySkolem("tmpVar", nm->realType());
52 : 8192 : return d_ta.requestArithVar(skolem, false, true);
53 : 4096 : }
54 : 4096 : void TempVarMalloc::release(ArithVar v) { d_ta.releaseArithVar(v); }
55 : :
56 : 28697 : BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
57 : 28697 : : d_ta(ta)
58 : : {
59 : 28697 : }
60 : 9984823 : void BasicVarModelUpdateCallBack::operator()(ArithVar x) { d_ta.signal(x); }
61 : :
62 : 143485 : RaiseConflict::RaiseConflict(TheoryArithPrivate& ta) : d_ta(ta) {}
63 : :
64 : 102961 : void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const
65 : : {
66 [ - + ][ - + ]: 102961 : Assert(c->inConflict());
[ - - ]
67 : 102961 : d_ta.raiseConflict(c, id);
68 : 102961 : }
69 : :
70 : 114788 : FarkasConflictBuilder::FarkasConflictBuilder(bool produceProofs)
71 : 114788 : : d_farkas(),
72 : 114788 : d_constraints(),
73 : 114788 : d_consequent(NullConstraint),
74 : 114788 : d_consequentSet(false),
75 : 114788 : d_produceProofs(produceProofs)
76 : : {
77 : 114788 : reset();
78 : 114788 : }
79 : :
80 : 1773373 : bool FarkasConflictBuilder::underConstruction() const
81 : : {
82 : 1773373 : return d_consequent != NullConstraint;
83 : : }
84 : :
85 : 102959 : bool FarkasConflictBuilder::consequentIsSet() const { return d_consequentSet; }
86 : :
87 : 217747 : void FarkasConflictBuilder::reset()
88 : : {
89 : 217747 : d_consequent = NullConstraint;
90 : 217747 : d_constraints.clear();
91 : 217747 : d_consequentSet = false;
92 [ + + ]: 217747 : if (d_produceProofs)
93 : : {
94 : 128698 : d_farkas.clear();
95 : : }
96 [ - + ][ - + ]: 217747 : Assert(!underConstruction());
[ - - ]
97 : 217747 : }
98 : :
99 : : /* Adds a constraint to the constraint under construction. */
100 : 1139352 : void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc)
101 : : {
102 [ + + ][ + + ]: 1139352 : Assert(
[ + - ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
103 : : !d_produceProofs
104 : : || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
105 : : || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
106 [ + + ][ + - ]: 1139352 : Assert(d_produceProofs || d_farkas.empty());
[ - + ][ - + ]
[ - - ]
107 [ - + ][ - + ]: 1139352 : Assert(c->isTrue());
[ - - ]
108 : :
109 [ + + ]: 1139352 : if (d_consequent == NullConstraint)
110 : : {
111 : 102959 : d_consequent = c;
112 : : }
113 : : else
114 : : {
115 : 1036393 : d_constraints.push_back(c);
116 : : }
117 [ + + ]: 1139352 : if (d_produceProofs)
118 : : {
119 : 537831 : d_farkas.push_back(fc);
120 : : }
121 [ + + ][ + - ]: 1139352 : Assert(!d_produceProofs || d_constraints.size() + 1 == d_farkas.size());
[ - + ][ - + ]
[ - - ]
122 [ + + ][ + - ]: 1139352 : Assert(d_produceProofs || d_farkas.empty());
[ - + ][ - + ]
[ - - ]
123 : 1139352 : }
124 : :
125 : 1138651 : void FarkasConflictBuilder::addConstraint(ConstraintCP c,
126 : : const Rational& fc,
127 : : const Rational& mult)
128 : : {
129 [ - + ][ - + ]: 1138651 : Assert(!mult.isZero());
[ - - ]
130 [ + + ][ + + ]: 1138651 : if (d_produceProofs && !mult.isOne())
[ + + ]
131 : : {
132 : 227833 : Rational prod = fc * mult;
133 : 227833 : addConstraint(c, prod);
134 : 227833 : }
135 : : else
136 : : {
137 : 910818 : addConstraint(c, fc);
138 : : }
139 : 1138651 : }
140 : :
141 : 102959 : void FarkasConflictBuilder::makeLastConsequent()
142 : : {
143 [ - + ][ - + ]: 102959 : Assert(!d_consequentSet);
[ - - ]
144 [ - + ][ - + ]: 102959 : Assert(underConstruction());
[ - - ]
145 : :
146 [ + + ]: 102959 : if (d_constraints.empty())
147 : : {
148 : : // no-op
149 : 4205 : d_consequentSet = true;
150 : : }
151 : : else
152 : : {
153 [ - + ][ - + ]: 98754 : Assert(d_consequent != NullConstraint);
[ - - ]
154 : 98754 : ConstraintCP last = d_constraints.back();
155 : 98754 : d_constraints.back() = d_consequent;
156 : 98754 : d_consequent = last;
157 [ + + ]: 98754 : if (d_produceProofs)
158 : : {
159 : 65901 : std::swap(d_farkas.front(), d_farkas.back());
160 : : }
161 : 98754 : d_consequentSet = true;
162 : : }
163 : :
164 [ - + ][ - + ]: 102959 : Assert(!d_consequent->negationHasProof());
[ - - ]
165 [ - + ][ - + ]: 102959 : Assert(d_consequentSet);
[ - - ]
166 : 102959 : }
167 : :
168 : : /* Turns the vector under construction into a conflict */
169 : 102959 : ConstraintCP FarkasConflictBuilder::commitConflict(NodeManager* nm)
170 : : {
171 [ - + ][ - + ]: 102959 : Assert(underConstruction());
[ - - ]
172 [ - + ][ - + ]: 102959 : Assert(!d_constraints.empty());
[ - - ]
173 [ + + ][ - + ]: 102959 : Assert(
[ - - ][ - + ]
[ - - ][ - + ]
[ + + ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
174 : : !d_produceProofs
175 : : || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
176 : : || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
177 [ + + ][ + - ]: 102959 : Assert(d_produceProofs || d_farkas.empty());
[ - + ][ - + ]
[ - - ]
178 [ - + ][ - + ]: 102959 : Assert(d_consequentSet);
[ - - ]
179 : :
180 : 102959 : ConstraintP not_c = d_consequent->getNegation();
181 [ + + ]: 102959 : RationalVectorCP coeffs = d_produceProofs ? &d_farkas : nullptr;
182 : 102959 : not_c->impliedByFarkas(nm, d_constraints, coeffs, true);
183 : :
184 : 102959 : reset();
185 [ - + ][ - + ]: 102959 : Assert(!underConstruction());
[ - - ]
186 [ - + ][ - + ]: 102959 : Assert(not_c->inConflict());
[ - - ]
187 [ - + ][ - + ]: 102959 : Assert(!d_consequentSet);
[ - - ]
188 : 102959 : return not_c;
189 : : }
190 : :
191 : 28697 : RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
192 : 28697 : : d_ta(ta)
193 : : {
194 : 28697 : }
195 : :
196 : : /* If you are not an equality engine, don't use this! */
197 : 3962 : void RaiseEqualityEngineConflict::raiseEEConflict(
198 : : Node n, std::shared_ptr<ProofNode> pf) const
199 : : {
200 : 3962 : d_ta.raiseBlackBoxConflict(n, pf);
201 : 3962 : }
202 : :
203 : 28697 : BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta) : d_ta(ta) {}
204 : :
205 : 22613 : const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const
206 : : {
207 : 22613 : return d_ta.boundsInfo(basic);
208 : : }
209 : :
210 : 22613 : BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const
211 : : {
212 : 22613 : return boundsInfo(basic).atBounds();
213 : : }
214 : 0 : BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const
215 : : {
216 : 0 : return boundsInfo(basic).hasBounds();
217 : : }
218 : :
219 : : } // namespace arith::linear
220 : : } // namespace theory
221 : : } // namespace cvc5::internal
|
