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, 7 insertions, 0 deletions

diff --git a/src/expr/node.h b/src/expr/node.h
index d3e8792ed..b90683050 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -570,6 +570,13 @@ struct NodeHashFunction {
   }
 };
 
+// for hash_maps, hash_sets..
+struct TNodeHashFunction {
+  size_t operator()(CVC4::TNode node) const {
+    return (size_t) node.getId();
+  }
+};
+
 template <bool ref_count>
 inline size_t NodeTemplate<ref_count>::getNumChildren() const {
   return d_nv->getNumChildren();