GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/callbacks.cpp Lines: 100 112 89.3 %
Date: 2021-03-22 Branches: 112 460 24.3 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file callbacks.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Haniel Barbosa, Mathias Preiner
6
 ** This file is part of the CVC4 project.
7
 ** Copyright (c) 2009-2021 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.\endverbatim
11
 **
12
 ** \brief [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
18
#include "theory/arith/callbacks.h"
19
20
#include "expr/proof_node.h"
21
#include "theory/arith/proof_macros.h"
22
#include "theory/arith/theory_arith_private.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace arith {
27
28
8995
SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
29
8995
  : d_arith(ta)
30
8995
{}
31
17109
void SetupLiteralCallBack::operator()(TNode lit){
32
34218
  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
33
17109
  if(!d_arith.isSetup(atom)){
34
17109
    d_arith.setupAtom(atom);
35
  }
36
17109
}
37
38
8995
DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
39
8995
  : d_ta(ta)
40
8995
{}
41
15629
Rational DeltaComputeCallback::operator()() const{
42
15629
  return d_ta.deltaValueForTotalOrder();
43
}
44
45
35980
TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
46
35980
: d_ta(ta)
47
35980
{}
48
ArithVar TempVarMalloc::request(){
49
  Node skolem = mkRealSkolem("tmpVar");
50
  return d_ta.requestArithVar(skolem, false, true);
51
}
52
void TempVarMalloc::release(ArithVar v){
53
  d_ta.releaseArithVar(v);
54
}
55
56
8995
BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
57
8995
  : d_ta(ta)
58
8995
{}
59
5608372
void BasicVarModelUpdateCallBack::operator()(ArithVar x){
60
5608372
  d_ta.signal(x);
61
5608372
}
62
63
44975
RaiseConflict::RaiseConflict(TheoryArithPrivate& ta)
64
44975
  : d_ta(ta)
65
44975
{}
66
67
66664
void RaiseConflict::raiseConflict(ConstraintCP c, InferenceId id) const{
68
66664
  Assert(c->inConflict());
69
66664
  d_ta.raiseConflict(c, id);
70
66664
}
71
72
35980
FarkasConflictBuilder::FarkasConflictBuilder()
73
  : d_farkas()
74
  , d_constraints()
75
  , d_consequent(NullConstraint)
76
35980
  , d_consequentSet(false)
77
{
78
35980
  reset();
79
35980
}
80
81
483815
bool FarkasConflictBuilder::underConstruction() const{
82
483815
  return d_consequent != NullConstraint;
83
}
84
85
66664
bool FarkasConflictBuilder::consequentIsSet() const{
86
66664
  return d_consequentSet;
87
}
88
89
102644
void FarkasConflictBuilder::reset(){
90
102644
  d_consequent = NullConstraint;
91
102644
  d_constraints.clear();
92
102644
  d_consequentSet = false;
93
102644
  ARITH_PROOF(d_farkas.clear());
94
102644
  Assert(!underConstruction());
95
102644
}
96
97
/* Adds a constraint to the constraint under construction. */
98
908686
void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc){
99
908686
  Assert(
100
      !ARITH_PROOF_ON()
101
      || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
102
      || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
103
908686
  Assert(ARITH_PROOF_ON() || d_farkas.empty());
104
908686
  Assert(c->isTrue());
105
106
908686
  if(d_consequent == NullConstraint){
107
66664
    d_consequent = c;
108
  } else {
109
842022
    d_constraints.push_back(c);
110
  }
111
908686
  ARITH_PROOF(d_farkas.push_back(fc));
112
908686
  Assert(!ARITH_PROOF_ON() || d_constraints.size() + 1 == d_farkas.size());
113
908686
  Assert(ARITH_PROOF_ON() || d_farkas.empty());
114
908686
}
115
116
908686
void FarkasConflictBuilder::addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult){
117
908686
  Assert(!mult.isZero());
118
908686
  if (ARITH_PROOF_ON() && !mult.isOne())
119
  {
120
51134
    Rational prod = fc * mult;
121
25567
    addConstraint(c, prod);
122
  }
123
  else
124
  {
125
883119
    addConstraint(c, fc);
126
  }
127
908686
}
128
129
66664
void FarkasConflictBuilder::makeLastConsequent(){
130
66664
  Assert(!d_consequentSet);
131
66664
  Assert(underConstruction());
132
133
66664
  if(d_constraints.empty()){
134
    // no-op
135
2803
    d_consequentSet = true;
136
  } else {
137
63861
    Assert(d_consequent != NullConstraint);
138
63861
    ConstraintCP last = d_constraints.back();
139
63861
    d_constraints.back() = d_consequent;
140
63861
    d_consequent = last;
141
63861
    ARITH_PROOF(std::swap(d_farkas.front(), d_farkas.back()));
142
63861
    d_consequentSet = true;
143
  }
144
145
66664
  Assert(!d_consequent->negationHasProof());
146
66664
  Assert(d_consequentSet);
147
66664
}
148
149
/* Turns the vector under construction into a conflict */
150
66664
ConstraintCP FarkasConflictBuilder::commitConflict(){
151
66664
  Assert(underConstruction());
152
66664
  Assert(!d_constraints.empty());
153
66664
  Assert(
154
      !ARITH_PROOF_ON()
155
      || (!underConstruction() && d_constraints.empty() && d_farkas.empty())
156
      || (underConstruction() && d_constraints.size() + 1 == d_farkas.size()));
157
66664
  Assert(ARITH_PROOF_ON() || d_farkas.empty());
158
66664
  Assert(d_consequentSet);
159
160
66664
  ConstraintP not_c = d_consequent->getNegation();
161
66664
  RationalVectorCP coeffs = ARITH_NULLPROOF(&d_farkas);
162
66664
  not_c->impliedByFarkas(d_constraints, coeffs, true );
163
164
66664
  reset();
165
66664
  Assert(!underConstruction());
166
66664
  Assert(not_c->inConflict());
167
66664
  Assert(!d_consequentSet);
168
66664
  return not_c;
169
}
170
171
8995
RaiseEqualityEngineConflict::RaiseEqualityEngineConflict(TheoryArithPrivate& ta)
172
8995
  : d_ta(ta)
173
8995
{}
174
175
/* If you are not an equality engine, don't use this! */
176
2388
void RaiseEqualityEngineConflict::raiseEEConflict(
177
    Node n, std::shared_ptr<ProofNode> pf) const
178
{
179
2388
  d_ta.raiseBlackBoxConflict(n, pf);
180
2388
}
181
182
8995
BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
183
8995
: d_ta(ta)
184
8995
{}
185
186
const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
187
  return d_ta.boundsInfo(basic);
188
}
189
190
BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
191
  return boundsInfo(basic).atBounds();
192
}
193
BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
194
  return boundsInfo(basic).hasBounds();
195
}
196
197
}/* CVC4::theory::arith namespace */
198
}/* CVC4::theory namespace */
199
26676
}/* CVC4 namespace */