2 #include "theory/arith/arith_prop_manager.h"
4 #include "theory/arith/arith_utilities.h"
5 #include "context/context.h"
6 #include "context/cdlist.h"
7 #include "context/cdmap.h"
8 #include "context/cdo.h"
11 using namespace CVC4::theory
;
12 using namespace CVC4::theory::arith
;
13 using namespace CVC4::kind
;
17 bool ArithPropManager::isAsserted(TNode n
) const{
18 Node satValue
= d_valuation
.getSatValue(n
);
19 if(satValue
.isNull()){
22 //Assert(satValue.getConst<bool>());
27 // Node ArithPropManager::strictlyWeakerAssertedUpperBound(TNode n) const{
30 // weaker = d_propagator.getWeakerImpliedUpperBound(weaker);
31 // }while(!weaker.isNull() && !isAsserted(weaker));
32 // Assert(weaker != n);
36 // Node ArithPropManager::strictlyWeakerAssertedLowerBound(TNode n) const{
39 // weaker = d_propagator.getWeakerImpliedLowerBound(weaker);
40 // }while(!weaker.isNull() && !isAsserted(weaker));
41 // Assert(weaker != n);
45 Node
ArithPropManager::strictlyWeakerAssertedUpperBound(ArithVar v
, const DeltaRational
& b
) const{
46 Node bound
= boundAsNode(true, v
, b
);
48 Assert(b
.getInfinitesimalPart() <= 0);
49 bool largeEpsilon
= (b
.getInfinitesimalPart() < -1);
54 weaker
= d_propagator
.getBestImpliedUpperBound(weaker
);
57 weaker
= d_propagator
.getWeakerImpliedUpperBound(weaker
);
59 }while(!weaker
.isNull() && !isAsserted(weaker
));
63 Node
ArithPropManager::strictlyWeakerAssertedLowerBound(ArithVar v
, const DeltaRational
& b
) const{
64 Debug("ArithPropManager") << "strictlyWeakerAssertedLowerBound" << endl
;
65 Node bound
= boundAsNode(false, v
, b
);
67 Assert(b
.getInfinitesimalPart() >= 0);
68 bool largeEpsilon
= (b
.getInfinitesimalPart() > 1);
71 Debug("ArithPropManager") << bound
<< b
<< endl
;
74 weaker
= d_propagator
.getBestImpliedLowerBound(weaker
);
77 weaker
= d_propagator
.getWeakerImpliedLowerBound(weaker
);
79 }while(!weaker
.isNull() && !isAsserted(weaker
));
80 Debug("ArithPropManager") << "res: " << weaker
<< endl
;
84 Node
ArithPropManager::getBestImpliedLowerBound(ArithVar v
, const DeltaRational
& b
) const{
85 Node bound
= boundAsNode(false, v
, b
);
86 return d_propagator
.getBestImpliedLowerBound(bound
);
88 Node
ArithPropManager::getBestImpliedUpperBound(ArithVar v
, const DeltaRational
& b
) const{
89 Node bound
= boundAsNode(true, v
, b
);
90 return d_propagator
.getBestImpliedUpperBound(bound
);
93 bool ArithPropManager::hasStrongerLowerBound(TNode n
) const{
94 bool haveAcompilerWarning
;
97 bool ArithPropManager::hasStrongerUpperBound(TNode n
) const{
101 Node
ArithPropManager::boundAsNode(bool upperbound
, ArithVar var
, const DeltaRational
& b
) const {
102 Assert((!upperbound
) || (b
.getInfinitesimalPart() <= 0) );
103 Assert(upperbound
|| (b
.getInfinitesimalPart() >= 0) );
105 Node varAsNode
= d_arithvarNodeMap
.asNode(var
);
109 negate
= b
.getInfinitesimalPart() < 0;
110 kind
= negate
? GEQ
: LEQ
;
112 negate
= b
.getInfinitesimalPart() > 0;
113 kind
= negate
? LEQ
: GEQ
;
116 Node righthand
= mkRationalNode(b
.getNoninfinitesimalPart());
117 Node bAsNode
= NodeBuilder
<2>(kind
) << varAsNode
<< righthand
;
120 bAsNode
= NodeBuilder
<1>(NOT
) << bAsNode
;
126 bool ArithPropManager::propagateArithVar(bool upperbound
, ArithVar var
, const DeltaRational
& b
, TNode reason
){
127 bool success
= false;
129 ++d_statistics
.d_propagateArithVarCalls
;
131 Node bAsNode
= boundAsNode(upperbound
, var
,b
);
133 Node bestImplied
= upperbound
?
134 d_propagator
.getBestImpliedUpperBound(bAsNode
):
135 d_propagator
.getBestImpliedLowerBound(bAsNode
);
137 Debug("ArithPropManager") << upperbound
<<","<< var
<<","<< b
<<","<< reason
<< endl
138 << bestImplied
<< endl
;
140 if(!bestImplied
.isNull()){
141 bool asserted
= isAsserted(bestImplied
);
143 if( !asserted
&& !isPropagated(bestImplied
)){
144 propagate(bestImplied
, reason
);
145 ++d_statistics
.d_addedPropagation
;
148 ++d_statistics
.d_alreadyPropagatedNode
;
149 }else if(!isPropagated(bestImplied
)){
150 ++d_statistics
.d_alreadySetSatLiteral
;
156 ArithPropManager::Statistics::Statistics():
157 d_propagateArithVarCalls("arith::prop-manager::propagateArithVarCalls",0),
158 d_addedPropagation("arith::prop-manager::addedPropagation",0),
159 d_alreadySetSatLiteral("arith::prop-manager::alreadySetSatLiteral",0),
160 d_alreadyPropagatedNode("arith::prop-manager::alreadyPropagatedNode",0)
162 StatisticsRegistry::registerStat(&d_propagateArithVarCalls
);
163 StatisticsRegistry::registerStat(&d_alreadySetSatLiteral
);
164 StatisticsRegistry::registerStat(&d_alreadyPropagatedNode
);
165 StatisticsRegistry::registerStat(&d_addedPropagation
);
168 ArithPropManager::Statistics::~Statistics()
170 StatisticsRegistry::unregisterStat(&d_propagateArithVarCalls
);
171 StatisticsRegistry::unregisterStat(&d_alreadySetSatLiteral
);
172 StatisticsRegistry::unregisterStat(&d_alreadyPropagatedNode
);
173 StatisticsRegistry::unregisterStat(&d_addedPropagation
);