1 /********************* */
2 /*! \file infer_bounds.h
4 ** Top contributors (to current version):
5 ** Tim King, Andrew Reynolds
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "cvc4_private.h"
24 #include "expr/node.h"
25 #include "theory/arith/delta_rational.h"
26 #include "theory/theory.h"
27 #include "util/integer.h"
28 #include "util/maybe.h"
29 #include "util/rational.h"
36 namespace inferbounds
{
37 enum Algorithms
{None
= 0, Lookup
, RowSum
, Simplex
};
38 enum SimplexParamKind
{ Unbounded
, NumVars
, Direct
};
40 class InferBoundAlgorithm
{
43 Maybe
<int> d_simplexRounds
;
44 InferBoundAlgorithm(Algorithms a
);
45 InferBoundAlgorithm(const Maybe
<int>& simplexRounds
);
48 InferBoundAlgorithm();
50 Algorithms
getAlgorithm() const;
51 const Maybe
<int>& getSimplexRounds() const;
53 static InferBoundAlgorithm
mkLookup();
54 static InferBoundAlgorithm
mkRowSum();
55 static InferBoundAlgorithm
mkSimplex(const Maybe
<int>& rounds
);
58 std::ostream
& operator<<(std::ostream
& os
, const Algorithms a
);
59 } /* namespace inferbounds */
61 class ArithEntailmentCheckParameters
64 typedef std::vector
<inferbounds::InferBoundAlgorithm
> VecInferBoundAlg
;
65 VecInferBoundAlg d_algorithms
;
68 typedef VecInferBoundAlg::const_iterator const_iterator
;
70 ArithEntailmentCheckParameters();
71 ~ArithEntailmentCheckParameters();
73 void addLookupRowSumAlgorithms();
74 void addAlgorithm(const inferbounds::InferBoundAlgorithm
& alg
);
76 const_iterator
begin() const;
77 const_iterator
end() const;
82 class InferBoundsResult
{
85 InferBoundsResult(Node term
, bool ub
);
87 void setBound(const DeltaRational
& dr
, Node exp
);
88 bool foundBound() const;
91 bool boundIsOptimal() const;
93 void setInconsistent();
94 bool inconsistentState() const;
96 const DeltaRational
& getValue() const;
97 bool boundIsRational() const;
98 const Rational
& valueAsRational() const;
99 bool boundIsInteger() const;
100 Integer
valueAsInteger() const;
102 Node
getTerm() const;
103 Node
getLiteral() const;
104 void setTerm(Node t
){ d_term
= t
; }
106 /* If there is a bound, this is a node that explains the bound. */
107 Node
getExplanation() const;
109 bool budgetIsExhausted() const;
110 void setBudgetExhausted();
112 bool thresholdWasReached() const;
113 void setReachedThreshold();
115 bool findUpperBound() const { return d_upperBound
; }
117 void setFindLowerBound() { d_upperBound
= false; }
118 void setFindUpperBound() { d_upperBound
= true; }
120 /* was a bound found */
123 /* was the budget exhausted */
124 bool d_budgetExhausted
;
126 /* does the bound have to be optimal*/
127 bool d_boundIsProvenOpt
;
129 /* was this started on an inconsistent state. */
130 bool d_inconsistentState
;
132 /* reached the threshold. */
133 bool d_reachedThreshold
;
135 /* the value of the bound */
136 DeltaRational d_value
;
138 /* The input term. */
141 /* Was the bound found an upper or lower bound.*/
144 /* Explanation of the bound. */
148 std::ostream
& operator<<(std::ostream
& os
, const InferBoundsResult
& ibr
);
150 class ArithEntailmentCheckSideEffects
153 ArithEntailmentCheckSideEffects();
154 ~ArithEntailmentCheckSideEffects();
156 InferBoundsResult
& getSimplexSideEffects();
159 InferBoundsResult
* d_simplexSideEffects
;
163 } /* namespace arith */
164 } /* namespace theory */
165 } /* namespace CVC4 */