Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Tim King, Gereon Kremer, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2025 by the authors listed in the file AUTHORS
8 : : * in the top-level source directory and their institutional affiliations.
9 : : * All rights reserved. See the file COPYING in the top-level source
10 : : * directory for licensing information.
11 : : * ****************************************************************************
12 : : *
13 : : * [[ Add one-line brief description here ]]
14 : : *
15 : : * [[ Add lengthier description here ]]
16 : : * \todo document this file
17 : : */
18 : :
19 : : #include "theory/arith/linear/callbacks.h"
20 : :
21 : : #include "expr/skolem_manager.h"
22 : : #include "proof/proof_node.h"
23 : : #include "theory/arith/linear/theory_arith_private.h"
24 : :
25 : : namespace cvc5::internal {
26 : : namespace theory {
27 : : namespace arith::linear {
28 : :
29 : 49907 : SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
30 : 49907 : : d_arith(ta)
31 : 49907 : {}
32 : 41371 : void SetupLiteralCallBack::operator()(TNode lit){
33 [ + + ]: 41371 : TNode atom = (lit.getKind() == Kind::NOT) ? lit[0] : lit;
34 [ + - ]: 41371 : if(!d_arith.isSetup(atom)){
35 : 41371 : d_arith.setupAtom(atom);
36 : : }
37 : 41371 : }
38 : :
39 : 49907 : DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
40 : 49907 : : d_ta(ta)
41 : 49907 : {}
42 : 110531 : Rational DeltaComputeCallback::operator()() const{
43 : 110531 : return d_ta.deltaValueForTotalOrder();
44 : : }
45 : :
46 : 199628 : TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
47 : 199628 : : d_ta(ta)
48 : 199628 : {}
49 : 3943 : ArithVar TempVarMalloc::request(){
50 : 3943 : NodeManager* nm = d_ta.getNodeManager();
51 : 7886 : Node skolem = NodeManager::mkDummySkolem("tmpVar", nm->realType());
52 : 7886 : return d_ta.requestArithVar(skolem, false, true);
53 : 3943 : }
54 : 3943 : void TempVarMalloc::release(ArithVar v){
55 : 3943 : d_ta.releaseArithVar(v);
56 : 3943 : }
57 : :
58 : 49907 : BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
59 : 49907 : : d_ta(ta)
60 : 49907 : {}
61 : 10179519 : void BasicVarModelUpdateCallBack::operator()(ArithVar x){
62 : 10179519 : d_ta.signal(x);
63 : 10179519 : }
64 : :
65 : 249535 : RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
66 : 249535 : : d_ta(ta)
67 : 249535 : {}
68 : :
69 : 101174 : void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
70 [ - + ][ - + ]: 101174 : Assert(c->inConflict());
[ - - ]
71 : 101174 : d_ta.raiseConflict(c, id);
72 : 101174 : }
73 : :
74 : 199628 : FarkasConflictBuilder::FarkasConflictBuilder(bool produceProofs)
75 : 199628 : : d_farkas(),
76 : 199628 : d_constraints(),
77 : 199628 : d_consequent(NullConstraint),
78 : 199628 : d_consequentSet(false),
79 : 199628 : d_produceProofs(produceProofs)
80 : : {
81 : 199628 : reset();
82 : 199628 : }
83 : :
84 : 1767913 : bool FarkasConflictBuilder::underConstruction() const{
85 : 1767913 : return d_consequent != NullConstraint;
86 : : }
87 : :
88 : 101172 : bool FarkasConflictBuilder::consequentIsSet() const{
89 : 101172 : return d_consequentSet;
90 : : }
91 : :
92 : 300800 : void FarkasConflictBuilder::reset(){
93 : 300800 : d_consequent = NullConstraint;
94 : 300800 : d_constraints.clear();
95 : 300800 : d_consequentSet = false;
96 [ + + ]: 300800 : if (d_produceProofs)
97 : : {
98 : 139281 : d_farkas.clear();
99 : : }
100 [ - + ][ - + ]: 300800 : Assert(!underConstruction());
[ - - ]
101 : 300800 : }
102 : :
103 : : /* Adds a constraint to the constraint under construction. */
104 : 1264334 : void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
105 [ + + ][ + + ]: 1264334 : Assert(
[ + - ][ + + ]
[ + - ][ + + ]
[ + + ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
106 : : !d_produceProofs
107 : : || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
108 : : || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
109 [ + + ][ + - ]: 1264334 : Assert(d_produceProofs || d_farkas.empty());
[ - + ][ - + ]
[ - - ]
110 [ - + ][ - + ]: 1264334 : Assert(c->isTrue());
[ - - ]
111 : :
112 [ + + ]: 1264334 : if(d_consequent == NullConstraint){
113 : 101172 : d_consequent = c;
114 : : } else {
115 : 1163162 : d_constraints.push_back(c);
116 : : }
117 [ + + ]: 1264334 : if (d_produceProofs)
118 : : {
119 : 499250 : d_farkas.push_back(fc);
120 : : }
121 [ + + ][ + - ]: 1264334 : Assert(!d_produceProofs || d_constraints.size() + 1 == d_farkas.size());
[ - + ][ - + ]
[ - - ]
122 [ + + ][ + - ]: 1264334 : Assert(d_produceProofs || d_farkas.empty());
[ - + ][ - + ]
[ - - ]
123 : 1264334 : }
124 : :
125 : 1263708 : void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
126 [ - + ][ - + ]: 1263708 : Assert(!mult.isZero());
[ - - ]
127 [ + + ][ + + ]: 1263708 : if (d_produceProofs && !mult.isOne())
[ + + ]
128 : : {
129 : 211507 : Rational prod = fc * mult;
130 : 211507 : addConstraint(c, prod);
131 : 211507 : }
132 : : else
133 : : {
134 : 1052201 : addConstraint(c, fc);
135 : : }
136 : 1263708 : }
137 : :
138 : 101172 : void FarkasConflictBuilder::makeLastConsequent(){
139 [ - + ][ - + ]: 101172 : Assert(!d_consequentSet);
[ - - ]
140 [ - + ][ - + ]: 101172 : Assert(underConstruction());
[ - - ]
141 : :
142 [ + + ]: 101172 : if(d_constraints.empty()){
143 : : // no-op
144 : 4906 : d_consequentSet = true;
145 : : } else {
146 [ - + ][ - + ]: 96266 : Assert(d_consequent != NullConstraint);
[ - - ]
147 : 96266 : ConstraintCP last = d_constraints.back();
148 : 96266 : d_constraints.back() = d_consequent;
149 : 96266 : d_consequent = last;
150 [ + + ]: 96266 : if (d_produceProofs)
151 : : {
152 : 60878 : std::swap(d_farkas.front(), d_farkas.back());
153 : : }
154 : 96266 : d_consequentSet = true;
155 : : }
156 : :
157 [ - + ][ - + ]: 101172 : Assert(!d_consequent->negationHasProof());
[ - - ]
158 [ - + ][ - + ]: 101172 : Assert(d_consequentSet);
[ - - ]
159 : 101172 : }
160 : :
161 : : /* Turns the vector under construction into a conflict */
162 : 101172 : ConstraintCP FarkasConflictBuilder::commitConflict(NodeManager* nm)
163 : : {
164 [ - + ][ - + ]: 101172 : Assert(underConstruction());
[ - - ]
165 [ - + ][ - + ]: 101172 : Assert(!d_constraints.empty());
[ - - ]
166 [ + + ][ - + ]: 101172 : Assert(
[ - - ][ - + ]
[ - - ][ - + ]
[ + + ][ + - ]
[ + - ][ + - ]
[ - + ][ - + ]
[ - - ]
167 : : !d_produceProofs
168 : : || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
169 : : || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
170 [ + + ][ + - ]: 101172 : Assert(d_produceProofs || d_farkas.empty());
[ - + ][ - + ]
[ - - ]
171 [ - + ][ - + ]: 101172 : Assert(d_consequentSet);
[ - - ]
172 : :
173 : 101172 : ConstraintP not_c = d_consequent->getNegation();
174 [ + + ]: 101172 : RationalVectorCP coeffs = d_produceProofs ? &d_farkas : nullptr;
175 : 101172 : not_c->impliedByFarkas(nm, d_constraints, coeffs, true);
176 : :
177 : 101172 : reset();
178 [ - + ][ - + ]: 101172 : Assert(!underConstruction());
[ - - ]
179 [ - + ][ - + ]: 101172 : Assert(not_c->inConflict());
[ - - ]
180 [ - + ][ - + ]: 101172 : Assert(!d_consequentSet);
[ - - ]
181 : 101172 : return not_c;
182 : : }
183 : :
184 : 49907 : RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
185 : 49907 : : d_ta(ta)
186 : 49907 : {}
187 : :
188 : : /* If you are not an equality engine, don't use this! */
189 : 4183 : void RaiseEqualityEngineConflict::raiseEEConflict(
190 : : Node n, std::shared_ptr<ProofNode> pf) const
191 : : {
192 : 4183 : d_ta.raiseBlackBoxConflict(n, pf);
193 : 4183 : }
194 : :
195 : 49907 : BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
196 : 49907 : : d_ta(ta)
197 : 49907 : {}
198 : :
199 : 20788 : const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
200 : 20788 : return d_ta.boundsInfo(basic);
201 : : }
202 : :
203 : 20788 : BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
204 : 20788 : return boundsInfo(basic).atBounds();
205 : : }
206 : 0 : BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
207 : 0 : return boundsInfo(basic).hasBounds();
208 : : }
209 : :
210 : : } // namespace arith
211 : : } // namespace theory
212 : : } // namespace cvc5::internal
|
