1 /*********************                                                        */
2 /*! \file callbacks.h
3  ** \verbatim
4  ** Top contributors (to current version):
5  **   Tim King, Mathias Preiner, Clark Barrett
6  ** This file is part of the CVC4 project.
7  ** Copyright (c) 2009-2019 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 
19 #pragma once
20 
21 #include "expr/node.h"
22 #include "theory/arith/arithvar.h"
23 #include "theory/arith/bound_counts.h"
24 #include "theory/arith/constraint_forward.h"
25 #include "theory/arith/theory_arith_private_forward.h"
26 #include "util/rational.h"
27 
28 namespace CVC4 {
29 namespace theory {
30 namespace arith {
31 
32 /**
33  * ArithVarCallBack provides a mechanism for agreeing on callbacks while
34  * breaking mutual recursion inclusion order problems.
35  */
36 class ArithVarCallBack {
37 public:
~ArithVarCallBack()38   virtual ~ArithVarCallBack() {}
39   virtual void operator()(ArithVar x) = 0;
40 };
41 
42 /**
43  * Requests arithmetic variables for internal use,
44  * and releases arithmetic variables that are no longer being used.
45  */
46 class ArithVarMalloc {
47 public:
~ArithVarMalloc()48   virtual ~ArithVarMalloc() {}
49   virtual ArithVar request() = 0;
50   virtual void release(ArithVar v) = 0;
51 };
52 
53 class TNodeCallBack {
54 public:
~TNodeCallBack()55   virtual ~TNodeCallBack() {}
56   virtual void operator()(TNode n) = 0;
57 };
58 
59 class NodeCallBack {
60 public:
~NodeCallBack()61   virtual ~NodeCallBack() {}
62   virtual void operator()(Node n) = 0;
63 };
64 
65 class RationalCallBack {
66 public:
~RationalCallBack()67   virtual ~RationalCallBack() {}
68   virtual Rational operator()() const = 0;
69 };
70 
71 class SetupLiteralCallBack : public TNodeCallBack {
72 private:
73   TheoryArithPrivate& d_arith;
74 public:
75   SetupLiteralCallBack(TheoryArithPrivate& ta);
76   void operator()(TNode lit) override;
77 };
78 
79 class DeltaComputeCallback : public RationalCallBack {
80 private:
81   const TheoryArithPrivate& d_ta;
82 public:
83   DeltaComputeCallback(const TheoryArithPrivate& ta);
84   Rational operator()() const override;
85 };
86 
87 class BasicVarModelUpdateCallBack : public ArithVarCallBack{
88 private:
89   TheoryArithPrivate& d_ta;
90 public:
91   BasicVarModelUpdateCallBack(TheoryArithPrivate& ta);
92   void operator()(ArithVar x) override;
93 };
94 
95 class TempVarMalloc : public ArithVarMalloc {
96 private:
97   TheoryArithPrivate& d_ta;
98 public:
99   TempVarMalloc(TheoryArithPrivate& ta);
100   ArithVar request() override;
101   void release(ArithVar v) override;
102 };
103 
104 class RaiseConflict {
105 private:
106   TheoryArithPrivate& d_ta;
107 public:
108   RaiseConflict(TheoryArithPrivate& ta);
109 
110   /** Calls d_ta.raiseConflict(c) */
111   void raiseConflict(ConstraintCP c) const;
112 };
113 
114 class FarkasConflictBuilder {
115 private:
116   RationalVector d_farkas;
117   ConstraintCPVec d_constraints;
118   ConstraintCP d_consequent;
119   bool d_consequentSet;
120 public:
121 
122   /**
123    * Constructs a new FarkasConflictBuilder.
124    */
125   FarkasConflictBuilder();
126 
127   /**
128    * Adds an antecedent constraint to the conflict under construction
129    * with the farkas coefficient fc * mult.
130    *
131    * The value mult is either 1 or -1.
132    */
133   void addConstraint(ConstraintCP c, const Rational& fc, const Rational& mult);
134 
135   /**
136    * Adds an antecedent constraint to the conflict under construction
137    * with the farkas coefficient fc.
138    */
139   void addConstraint(ConstraintCP c, const Rational& fc);
140 
141   /**
142    * Makes the last constraint added the consequent.
143    * Can be done exactly once per reset().
144    */
145   void makeLastConsequent();
146 
147   /**
148    * Turns the antecendents into a proof of the negation of one of the
149    * antecedents.
150    *
151    * The buffer is no longer underConstruction afterwards.
152    *
153    * precondition:
154    * - At least two constraints have been asserted.
155    * - makeLastConsequent() has been called.
156    *
157    * postcondition: The returned constraint is in conflict.
158    */
159   ConstraintCP commitConflict();
160 
161   /** Returns true if a conflict has been pushed back since the last reset. */
162   bool underConstruction() const;
163 
164   /** Returns true if the consequent has been set since the last reset. */
165   bool consequentIsSet() const;
166 
167   /** Resets the state of the buffer. */
168   void reset();
169 };
170 
171 
172 class RaiseEqualityEngineConflict {
173 private:
174   TheoryArithPrivate& d_ta;
175 
176 public:
177   RaiseEqualityEngineConflict(TheoryArithPrivate& ta);
178 
179   /* If you are not an equality engine, don't use this! */
180   void raiseEEConflict(Node n) const;
181 };
182 
183 class BoundCountingLookup {
184 private:
185   TheoryArithPrivate& d_ta;
186 public:
187   BoundCountingLookup(TheoryArithPrivate& ta);
188   const BoundsInfo& boundsInfo(ArithVar basic) const;
189   BoundCounts atBounds(ArithVar basic) const;
190   BoundCounts hasBounds(ArithVar basic) const;
191 };
192 
193 }/* CVC4::theory::arith namespace */
194 }/* CVC4::theory namespace */
195 }/* CVC4 namespace */
196