Merging a squash of the branch timothy-king/CVC4/glpknecfix c95bf7d4f1 into master. See the CAV14 submission for an explanation of the changes to the integer solver's behavior. If compiled against the our custom extension of glpk, https://github.com/timothy-king/glpk-cut-log, this should have substantial differences in behavior. This should have moderate performance differences for linear real and integer arithmetic even if these features are disabled.

1 files changed, 48 insertions, 3 deletions

diff --git a/src/theory/arith/callbacks.cpp b/src/theory/arith/callbacks.cpp
index d4a445b70..c4b64682f 100644
--- a/src/theory/arith/callbacks.cpp
+++ b/src/theory/arith/callbacks.cpp
@@ -22,6 +22,9 @@ namespace CVC4 {
 namespace theory {
 namespace arith {
 
+SetupLiteralCallBack::SetupLiteralCallBack(TheoryArithPrivate& ta)
+  : d_arith(ta)
+{}
 void SetupLiteralCallBack::operator()(TNode lit){
   TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
   if(!d_arith.isSetup(atom)){
@@ -29,30 +32,72 @@ void SetupLiteralCallBack::operator()(TNode lit){
   }
 }
 
+DeltaComputeCallback::DeltaComputeCallback(const TheoryArithPrivate& ta)
+  : d_ta(ta)
+{}
 Rational DeltaComputeCallback::operator()() const{
   return d_ta.deltaValueForTotalOrder();
 }
 
+TempVarMalloc::TempVarMalloc(TheoryArithPrivate& ta)
+: d_ta(ta)
+{}
 ArithVar TempVarMalloc::request(){
   Node skolem = mkRealSkolem("tmpVar");
-  return d_ta.requestArithVar(skolem, false);
+  return d_ta.requestArithVar(skolem, false, true);
 }
 void TempVarMalloc::release(ArithVar v){
   d_ta.releaseArithVar(v);
 }
 
+BasicVarModelUpdateCallBack::BasicVarModelUpdateCallBack(TheoryArithPrivate& ta)
+  : d_ta(ta)
+{}
 void BasicVarModelUpdateCallBack::operator()(ArithVar x){
   d_ta.signal(x);
 }
 
-void RaiseConflict::operator()(Node n){
-  d_ta.raiseConflict(n);
+RaiseConflict::RaiseConflict(TheoryArithPrivate& ta, ConstraintCPVec& buf )
+  : d_ta(ta)
+  , d_construction(buf)
+{}
+
+/* Adds a constraint to the constraint under construction. */
+void RaiseConflict::addConstraint(ConstraintCP c){
+  d_construction.push_back(c);
+}
+/* Turns the vector under construction into a conflict */
+void RaiseConflict::commitConflict(){
+  Assert(!d_construction.empty());
+  sendConflict(d_construction);
+  d_construction.clear();
+}
+
+void RaiseConflict::sendConflict(const ConstraintCPVec& vec){
+  d_ta.raiseConflict(vec);
+}
+
+/* If you are not an equality engine, don't use this! */
+void RaiseConflict::blackBoxConflict(Node n){
+  d_ta.blackBoxConflict(n);
 }
 
+
+BoundCountingLookup::BoundCountingLookup(TheoryArithPrivate& ta)
+: d_ta(ta)
+{}
+
 const BoundsInfo& BoundCountingLookup::boundsInfo(ArithVar basic) const{
   return d_ta.boundsInfo(basic);
 }
 
+BoundCounts BoundCountingLookup::atBounds(ArithVar basic) const{
+  return boundsInfo(basic).atBounds();
+}
+BoundCounts BoundCountingLookup::hasBounds(ArithVar basic) const {
+  return boundsInfo(basic).hasBounds();
+}
+
 }/* CVC4::theory::arith namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */