This commit merges the branch arithmetic/propagation-again into trunk.

	- This adds code for bounds refinement, and conflict weakening.
	- This adds util/boolean_simplification.h.
	- This adds a propagation manager to theory of arithmetic.
	- Propagation is disabled by default.
	- Propagation can be enabled by the command line flag "--enable-arithmetic-propagation"
	- Propagation interacts *heavily* with rewriting equalities, and will work best if the command line flag "--rewrite-arithmetic-equalities" is enabled.

4 files changed, 131 insertions, 2 deletions

diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index eb63885a2..aaf9ca03b 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -47,7 +47,9 @@ libutil_la_SOURCES = \
 	language.h \
 	triple.h \
 	trans_closure.h \
-	trans_closure.cpp
+	trans_closure.cpp \
+	boolean_simplification.h
+
 libutil_la_LIBADD = \
 	@builddir@/libutilcudd.la
 libutilcudd_la_SOURCES = \
diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h
new file mode 100644
index 000000000..062bf11b6
--- /dev/null
+++ b/src/util/boolean_simplification.h
@@ -0,0 +1,116 @@
+/*********************                                                        */
+/*! \file bitvector.h
+ ** \verbatim
+ ** Original author: dejan
+ ** Major contributors: cconway
+ ** Minor contributors (to current version): mdeters
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__BOOLEAN_SIMPLIFICATION_H
+#define __CVC4__BOOLEAN_SIMPLIFICATION_H
+
+#include "expr/node.h"
+#include "util/Assert.h"
+#include <vector>
+
+
+namespace CVC4 {
+
+class BooleanSimplification {
+public:
+
+  static const uint32_t DUPLICATE_REMOVAL_THRESHOLD = 10;
+
+  static void removeDuplicates(std::vector<Node>& buffer){
+    if(buffer.size() < DUPLICATE_REMOVAL_THRESHOLD){
+      std::sort(buffer.begin(), buffer.end());
+      std::vector<Node>::iterator new_end = std::unique(buffer.begin(), buffer.end());
+      buffer.erase(new_end, buffer.end());
+    }
+  }
+
+  static Node simplifyConflict(Node andNode){
+    Assert(andNode.getKind() == kind::AND);
+    std::vector<Node> buffer;
+    push_back_associative_commute(andNode, buffer, kind::AND, kind::OR, false);
+
+    removeDuplicates(buffer);
+
+    NodeBuilder<> nb(kind::AND);
+    nb.append(buffer);
+    return nb;
+  }
+
+  static Node simplifyClause(Node orNode){
+    Assert(orNode.getKind() == kind::OR);
+    std::vector<Node> buffer;
+    push_back_associative_commute(orNode, buffer, kind::OR, kind::AND, false);
+
+    removeDuplicates(buffer);
+
+    NodeBuilder<> nb(kind::OR);
+    nb.append(buffer);
+    return nb;
+  }
+
+  static Node simplifyHornClause(Node implication){
+    Assert(implication.getKind() == kind::IMPLIES);
+    TNode left = implication[0];
+    TNode right = implication[1];
+    Node notLeft = NodeBuilder<1>(kind::NOT)<<left;
+    Node clause = NodeBuilder<2>(kind::OR)<< notLeft << right;
+    return simplifyClause(clause);
+  }
+
+  static void push_back_associative_commute(Node n, std::vector<Node>& buffer, Kind k, Kind notK, bool negateNode){
+    Node::iterator i = n.begin(), end = n.end();
+    for(; i != end; ++i){
+      Node child = *i;
+      if(child.getKind() == k){
+        push_back_associative_commute(child, buffer, k, notK, negateNode);
+      }else if(child.getKind() == kind::NOT && child[0].getKind() == notK){
+        push_back_associative_commute(child, buffer, notK, k, !negateNode);
+      }else{
+        if(negateNode){
+          buffer.push_back(negate(child));
+        }else{
+          buffer.push_back(child);
+        }
+      }
+    }
+  }
+
+  static Node negate(TNode n){
+    bool polarity = true;
+    TNode base = n;
+    while(base.getKind() == kind::NOT){
+      base = base[0];
+      polarity = !polarity;
+    }
+    if(polarity){
+      return base.notNode();
+    }else{
+      return base;
+    }
+  }
+
+};/* class BitVector */
+
+
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__BITVECTOR_H */
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 03dedfe00..6018ce611 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -81,6 +81,7 @@ Options::Options() :
   replayStream(NULL),
   replayLog(NULL),
   rewriteArithEqualities(false),
+  arithPropagation(false),
   satRandomFreq(0.0),
   satRandomSeed(91648253), //Minisat's default value
   pivotRule(MINIMUM)
@@ -120,6 +121,7 @@ static const string optionsDescription = "\
    --random-freq=P        sets the frequency of random decisions in the sat solver(P=0.0 by default)\n\
    --random-seed=S        sets the random seed for the sat solver\n\
    --rewrite-arithmetic-equalities rewrite (= x y) to (and (<= x y) (>= x y)) in arithmetic\n\
+   --enable-arithmetic-propagation turns on arithmetic propagation\n \
    --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
@@ -179,7 +181,8 @@ enum OptionValue {
   PIVOT_RULE,
   RANDOM_FREQUENCY,
   RANDOM_SEED,
-  REWRITE_ARITHMETIC_EQUALITIES
+  REWRITE_ARITHMETIC_EQUALITIES,
+  ARITHMETIC_PROPAGATION
 };/* enum OptionValue */
 
 /**
@@ -247,6 +250,7 @@ static struct option cmdlineOptions[] = {
   { "random-freq" , required_argument, NULL, RANDOM_FREQUENCY  },
   { "random-seed" , required_argument, NULL, RANDOM_SEED  },
   { "rewrite-arithmetic-equalities", no_argument, NULL, REWRITE_ARITHMETIC_EQUALITIES },
+  { "enable-arithmetic-propagation", no_argument, NULL, ARITHMETIC_PROPAGATION },
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -477,6 +481,10 @@ throw(OptionException) {
       rewriteArithEqualities = true;
       break;
 
+    case ARITHMETIC_PROPAGATION:
+      arithPropagation = true;
+      break;
+
     case RANDOM_SEED:
       satRandomSeed = atof(optarg);
       break;
diff --git a/src/util/options.h b/src/util/options.h
index 8273db458..be432e5a7 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -143,6 +143,9 @@ struct CVC4_PUBLIC Options {
   /** Whether to rewrite equalities in arithmetic theory */
   bool rewriteArithEqualities;
 
+  /** Turn on and of arithmetic propagation. */
+  bool arithPropagation;
+
   /**
    * Frequency for the sat solver to make random decisions.
    * Should be between 0 and 1.