From f0a7f0d1b929424776b103cde45b2b60d98f5f48 Mon Sep 17 00:00:00 2001
From: Cristian Cadar <cristic@cs.stanford.edu>
Date: Fri, 10 Jul 2009 07:35:41 +0000
Subject: Simple propagation rules for boolean not in the fast cex solver.

git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@75242 91177308-0d34-0410-b5e6-96231b3b80d8
---
 lib/Solver/FastCexSolver.cpp | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

(limited to 'lib')

diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp
index 74c068b0..fbf2ecf2 100644
--- a/lib/Solver/FastCexSolver.cpp
+++ b/lib/Solver/FastCexSolver.cpp
@@ -697,6 +697,13 @@ public:
       break;
     }
 
+    case Expr::Not: {
+      if (e->getWidth() == Expr::Bool && range.isFixed()) {
+	propogatePossibleValue(e->getKid(0), !range.min());
+      }
+      break;
+    }
+
     case Expr::Ult: {
       BinaryExpr *be = cast<BinaryExpr>(e);
       
@@ -887,6 +894,14 @@ public:
       break;
     }
 
+    // If a boolean not, and the result is known, propagate it
+    case Expr::Not: {
+      if (e->getWidth() == Expr::Bool && range.isFixed()) {
+	propogateExactValue(e->getKid(0), !range.min());
+      }
+      break;
+    }
+
     case Expr::Ult: {
       break;
     }
-- 
cgit 1.4.1