Significant revision to theory/arith. The new draft has a lot of small bug fixes and organizational changes. The theory is now enabled to perform checking in the TheoryEngine. This draft can now solve 2 new regression tests test/regress/regress0/ineq_slack.smt and test/regress/regress0/ineq_basic.smt. There is also a small bug fix inside src/expr/attribute.h.

4 files changed, 46 insertions, 0 deletions

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 58f9c6a4e..521536630 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -24,6 +24,8 @@ TESTS =	\
 	logops.04.cvc \
 	logops.05.cvc \
 	simple.cvc \
+	ineq_basic.smt \
+	ineq_slack.smt \
 	smallcnf.cvc \
 	test11.cvc \
 	test9.cvc \
diff --git a/test/regress/regress0/ineq_basic.smt b/test/regress/regress0/ineq_basic.smt
new file mode 100644
index 000000000..ba4cb8b7f
--- /dev/null
+++ b/test/regress/regress0/ineq_basic.smt
@@ -0,0 +1,9 @@
+(benchmark ineq_basic
+:status unsat
+:logic QF_LRA
+:extrafuns ((x Real))
+:formula
+ (and (<= 0 x)
+      (< x 0)
+ )
+)
diff --git a/test/regress/regress0/ineq_slack.smt b/test/regress/regress0/ineq_slack.smt
new file mode 100644
index 000000000..b3d79c5f2
--- /dev/null
+++ b/test/regress/regress0/ineq_slack.smt
@@ -0,0 +1,11 @@
+(benchmark ineq_basic
+:status unsat
+:logic QF_LRA
+:extrafuns ((x Real))
+:extrafuns ((y Real))
+:formula
+ (and (<= (+ x y) 0)
+      (< 1 x)
+      (<= 0 y)
+ )
+)
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 7e034036a..52a324d53 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -561,4 +561,28 @@ public:
     sstr << Node::setdepth(3) << o;
     TS_ASSERT(sstr.str() == "(XOR (AND w (OR x y) z) (AND w (OR x y) z))");
   }
+
+//  This Test is designed to fail in a way that will cause a segfault,
+//  so it is commented out.
+//  This is for demonstrating what a certain type of user error looks like.
+//   Node level0(){
+//     NodeBuilder<> nb(kind::AND);
+//     Node x = d_nodeManager->mkVar(*d_booleanType);
+//     nb << x;
+//     nb << x;
+//     return Node(nb.constructNode());
+//   }
+
+//   TNode level1(){
+//     return level0();
+//   }
+
+//   void testChaining() {
+//     Node res = level1();
+
+//     TS_ASSERT(res.getKind() == kind::NULL_EXPR);
+//     TS_ASSERT(res != Node::null());
+
+//     cerr << "I finished both tests now watch as I crash" << endl;
+//   }
 };