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