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.

1 files changed, 10 insertions, 0 deletions

diff --git a/src/theory/arith/delta_rational.cpp b/src/theory/arith/delta_rational.cpp
new file mode 100644
index 000000000..90529529a
--- /dev/null
+++ b/src/theory/arith/delta_rational.cpp
@@ -0,0 +1,10 @@
+
+#include "theory/arith/delta_rational.h"
+
+using namespace std;
+using namespace CVC4;
+
+std::ostream& CVC4::operator<<(std::ostream& os, const DeltaRational& dq){
+  return os << "(" << dq.getNoninfintestimalPart()
+            << "," << dq.getInfintestimalPart() << ")";
+}