Add skeleton of the FP theory solver (#1130)

This commit adds the skeleton of the theory solver using a dummy version of the converter (fp_converter.{h,cpp}). The converter is a class that is used to produce bit-vector expressions equivalent to floating-point ones. The commit sets up the equality engine and the infrastructure for interacting with the main theory components. The majority of this code is still agnostic to how the conversion is actually implemented / what kind of theory solver this is. This is pretty much the template code you need to write any kind of theory solver. This includes equality reasoning and so should be able to solve some basic problems.

1 files changed, 91 insertions, 15 deletions

diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 0355ed811..5205f5e23 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -20,34 +20,110 @@
 #ifndef __CVC4__THEORY__FP__THEORY_FP_H
 #define __CVC4__THEORY__FP__THEORY_FP_H
 
+#include <string>
+#include <utility>
+
+#include "context/cdo.h"
+#include "theory/fp/fp_converter.h"
 #include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 namespace fp {
 
 class TheoryFp : public Theory {
-public:
-
+ public:
   /** Constructs a new instance of TheoryFp w.r.t. the provided contexts. */
-  TheoryFp(context::Context* c,
-           context::UserContext* u,
-           OutputChannel& out,
-           Valuation valuation,
-           const LogicInfo& logicInfo);
+  TheoryFp(context::Context* c, context::UserContext* u, OutputChannel& out,
+           Valuation valuation, const LogicInfo& logicInfo);
+
+  Node expandDefinition(LogicRequest& lr, Node node);
 
-  Node expandDefinition(LogicRequest &, Node node);
+  void preRegisterTerm(TNode node);
+  void addSharedTerm(TNode node);
 
   void check(Effort);
 
-  std::string identify() const {
-    return "THEORY_FP";
-  }
+  Node getModelValue(TNode var);
+  void collectModelInfo(TheoryModel* m);
+
+  std::string identify() const { return "THEORY_FP"; }
+
+  void setMasterEqualityEngine(eq::EqualityEngine* eq);
+
+  Node explain(TNode n);
+
+ protected:
+  /** Equality engine */
+  class NotifyClass : public eq::EqualityEngineNotify {
+   protected:
+    TheoryFp& d_theorySolver;
+
+   public:
+    NotifyClass(TheoryFp& solver) : d_theorySolver(solver) {}
+    bool eqNotifyTriggerEquality(TNode equality, bool value);
+    bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+    bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2,
+                                     bool value);
+    void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+    void eqNotifyNewClass(TNode t) {}
+    void eqNotifyPreMerge(TNode t1, TNode t2) {}
+    void eqNotifyPostMerge(TNode t1, TNode t2) {}
+    void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {}
+  };
+  friend NotifyClass;
+
+  NotifyClass d_notification;
+  eq::EqualityEngine d_equalityEngine;
+
+  /** General utility **/
+  void registerTerm(TNode node);
+  bool isRegistered(TNode node);
+
+  context::CDHashSet<Node, NodeHashFunction> d_registeredTerms;
+
+  /** Bit-blasting conversion */
+  FpConverter d_conv;
+  bool d_expansionRequested;
+
+  void convertAndEquateTerm(TNode node);
+
+  /** Interaction with the rest of the solver **/
+  void handleLemma(Node node);
+  bool handlePropagation(TNode node);
+  void handleConflict(TNode node);
+
+  context::CDO<bool> d_conflict;
+  context::CDO<Node> d_conflictNode;
+
+  /** Uninterpretted functions for partially defined functions. **/
+  typedef context::CDHashMap<TypeNode, Node, TypeNodeHashFunction>
+      ComparisonUFMap;
+
+  ComparisonUFMap d_minMap;
+  ComparisonUFMap d_maxMap;
+
+  Node minUF(Node);
+  Node maxUF(Node);
+
+  typedef context::CDHashMap<std::pair<TypeNode, TypeNode>, Node,
+                             PairTypeNodeHashFunction>
+      ConversionUFMap;
+
+  ConversionUFMap d_toUBVMap;
+  ConversionUFMap d_toSBVMap;
+
+  Node toUBVUF(Node);
+  Node toSBVUF(Node);
+
+  ComparisonUFMap d_toRealMap;
 
-};/* class TheoryFp */
+  Node toRealUF(Node);
+}; /* class TheoryFp */
 
-}/* CVC4::theory::fp namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace fp
+}  // namespace theory
+}  // namespace CVC4
 
 #endif /* __CVC4__THEORY__FP__THEORY_FP_H */