about summary refs log tree commit diff homepage
path: root/lib/Solver
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver')
-rw-r--r--lib/Solver/CexCachingSolver.cpp8
-rw-r--r--lib/Solver/FastCexSolver.cpp10
-rw-r--r--lib/Solver/IndependentSolver.cpp2
-rw-r--r--lib/Solver/STPBuilder.cpp18
-rw-r--r--lib/Solver/Solver.cpp8
5 files changed, 23 insertions, 23 deletions
diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp
index db15632b..546d81fd 100644
--- a/lib/Solver/CexCachingSolver.cpp
+++ b/lib/Solver/CexCachingSolver.cpp
@@ -138,7 +138,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
                                         Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
-  if (neg.isConstant()) {
+  if (neg->isConstant()) {
     if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
@@ -153,7 +153,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query,
 bool CexCachingSolver::getAssignment(const Query& query, Assignment *&result) {
   KeyType key(query.constraints.begin(), query.constraints.end());
   ref<Expr> neg = Expr::createNot(query.expr);
-  if (neg.isConstant()) {
+  if (neg->isConstant()) {
     if (!neg->getConstantValue()) {
       result = (Assignment*) 0;
       return true;
@@ -217,7 +217,7 @@ bool CexCachingSolver::computeValidity(const Query& query,
     return false;
   assert(a && "computeValidity() must have assignment");
   ref<Expr> q = a->evaluate(query.expr);
-  assert(q.isConstant() && "assignment evaluation did not result in constant");
+  assert(q->isConstant() && "assignment evaluation did not result in constant");
 
   if (q->getConstantValue()) {
     if (!getAssignment(query, a))
@@ -268,7 +268,7 @@ bool CexCachingSolver::computeValue(const Query& query,
     return false;
   assert(a && "computeValue() must have assignment");
   result = a->evaluate(query.expr);  
-  assert(result.isConstant() && 
+  assert(result->isConstant() && 
          "assignment evaluation did not result in constant");
   return true;
 }
diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 88f34c99..ee46be4f 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -416,7 +416,7 @@ public:
 
       // XXX we need to respect the version here and object state chain
 
-      if (re->index.isConstant() && 
+      if (re->index->isConstant() && 
           re->index->getConstantValue() < array->size) {
         CexValueData &cvd = cod.values[re->index->getConstantValue()];
         CexValueData tmp = cvd.set_intersection(range);
@@ -613,7 +613,7 @@ public:
     case Expr::Eq: {
       BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
       if (range.isFixed()) {
-        if (be->left.isConstant()) {
+        if (be->left->isConstant()) {
           uint64_t value = be->left->getConstantValue();
           if (range.min()) {
             forceExprToValue(be->right, value);
@@ -729,7 +729,7 @@ public:
   bool exprMustBeValue(ref<Expr> e, uint64_t value) {
     CexConstifier cc(objectValues);
     ref<Expr> v = cc.visit(e);
-    if (!v.isConstant()) return false;
+    if (!v->isConstant()) return false;
     // XXX reenable once all reads and vars are fixed
     //    assert(v.isConstant() && "not all values have been fixed");
     return v->getConstantValue() == value;
@@ -886,7 +886,7 @@ bool FastCexSolver::computeValue(const Query& query, ref<Expr> &result) {
   CexConstifier cc(cd.objectValues);
   ref<Expr> value = cc.visit(query.expr);
 
-  if (value.isConstant()) {
+  if (value->isConstant()) {
     result = value;
     return true;
   } else {
@@ -939,7 +939,7 @@ FastCexSolver::computeInitialValues(const Query& query,
                                   ConstantExpr::create(i,
                                                        kMachinePointerType)));
       
-      if (value.isConstant()) {
+      if (value->isConstant()) {
         data.push_back(value->getConstantValue());
       } else {
         // FIXME: When does this happen?
diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp
index 18e5c84d..4e004fd8 100644
--- a/lib/Solver/IndependentSolver.cpp
+++ b/lib/Solver/IndependentSolver.cpp
@@ -97,7 +97,7 @@ public:
       if (re->updates.isRooted) {
         const Array *array = re->updates.root;
         if (!wholeObjects.count(array)) {
-          if (re->index.isConstant()) {
+          if (re->index->isConstant()) {
             DenseSet<unsigned> &dis = elements[array];
             dis.add((unsigned) re->index->getConstantValue());
           } else {
diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp
index 1d27c655..d1f7360c 100644
--- a/lib/Solver/STPBuilder.cpp
+++ b/lib/Solver/STPBuilder.cpp
@@ -419,7 +419,7 @@ ExprHandle STPBuilder::getInitialRead(const Array *root, unsigned index) {
 /** if *width_out!=1 then result is a bitvector,
     otherwise it is a bool */
 ExprHandle STPBuilder::construct(ref<Expr> e, int *width_out) {
-  if (!UseConstructHash || e.isConstant()) {
+  if (!UseConstructHash || e->isConstant()) {
     return constructActual(e, width_out);
   } else {
     ExprHashMap< std::pair<ExprHandle, unsigned> >::iterator it = 
@@ -555,7 +555,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle right = construct(me->right, width_out);
     assert(*width_out!=1 && "uncanonicalized mul");
 
-    if (me->left.isConstant()) {
+    if (me->left->isConstant()) {
       return constructMulByConstant(right, *width_out, 
                                     me->left->getConstantValue());
     } else {
@@ -569,7 +569,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized udiv");
     
-    if (de->right.isConstant()) {
+    if (de->right->isConstant()) {
       uint64_t divisor = de->right->getConstantValue();
       
       if (bits64::isPowerOfTwo(divisor)) {
@@ -591,7 +591,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized sdiv");
 
-    if (de->right.isConstant()) {
+    if (de->right->isConstant()) {
       uint64_t divisor = de->right->getConstantValue();
  
       if (optimizeDivides) {
@@ -611,7 +611,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(de->left, width_out);
     assert(*width_out!=1 && "uncanonicalized urem");
     
-    if (de->right.isConstant()) {
+    if (de->right->isConstant()) {
       uint64_t divisor = de->right->getConstantValue();
 
       if (bits64::isPowerOfTwo(divisor)) {
@@ -710,7 +710,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(se->left, width_out);
     assert(*width_out!=1 && "uncanonicalized shl");
 
-    if (se->right.isConstant()) {
+    if (se->right->isConstant()) {
       return bvLeftShift(left, se->right->getConstantValue(), getShiftBits(*width_out));
     } else {
       int shiftWidth;
@@ -725,7 +725,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     unsigned shiftBits = getShiftBits(*width_out);
     assert(*width_out!=1 && "uncanonicalized lshr");
 
-    if (lse->right.isConstant()) {
+    if (lse->right->isConstant()) {
       return bvRightShift(left, (unsigned) lse->right->getConstantValue(), shiftBits);
     } else {
       int shiftWidth;
@@ -739,7 +739,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ase->left, width_out);
     assert(*width_out!=1 && "uncanonicalized ashr");
     
-    if (ase->right.isConstant()) {
+    if (ase->right->isConstant()) {
       unsigned shift = (unsigned) ase->right->getConstantValue();
       ExprHandle signedBool = bvBoolExtract(left, *width_out-1);
       return constructAShrByConstant(left, shift, signedBool, getShiftBits(*width_out));
@@ -757,7 +757,7 @@ ExprHandle STPBuilder::constructActual(ref<Expr> e, int *width_out) {
     ExprHandle left = construct(ee->left, width_out);
     ExprHandle right = construct(ee->right, width_out);
     if (*width_out==1) {
-      if (ee->left.isConstant()) {
+      if (ee->left->isConstant()) {
         assert(!ee->left->getConstantValue() && "uncanonicalized eq");
         return vc_notExpr(vc, right);
       } else {
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 8990e3b9..46d6039e 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -56,7 +56,7 @@ bool Solver::evaluate(const Query& query, Validity &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr.isConstant()) {
+  if (query.expr->isConstant()) {
     result = query.expr->getConstantValue() ? True : False;
     return true;
   }
@@ -82,7 +82,7 @@ bool Solver::mustBeTrue(const Query& query, bool &result) {
   assert(query.expr->getWidth() == Expr::Bool && "Invalid expression type!");
 
   // Maintain invariants implementations expect.
-  if (query.expr.isConstant()) {
+  if (query.expr->isConstant()) {
     result = query.expr->getConstantValue() ? true : false;
     return true;
   }
@@ -112,7 +112,7 @@ bool Solver::mayBeFalse(const Query& query, bool &result) {
 
 bool Solver::getValue(const Query& query, ref<Expr> &result) {
   // Maintain invariants implementation expect.
-  if (query.expr.isConstant()) {
+  if (query.expr->isConstant()) {
     result = query.expr;
     return true;
   }
@@ -151,7 +151,7 @@ std::pair< ref<Expr>, ref<Expr> > Solver::getRange(const Query& query) {
     default:
       min = 0, max = 1; break;
     }
-  } else if (e.isConstant()) {
+  } else if (e->isConstant()) {
     min = max = e->getConstantValue();
   } else {
     // binary search for # of useful bits
generated by cgit-pink 1.4.1 (git 2.36.1) at 2025-01-08 15:19:35 +0000