1 files changed, 105 insertions, 0 deletions
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h
new file mode 100644
index 000000000..914da14b4
--- /dev/null
+++ b/src/theory/quantifiers/fmf/ambqi_builder.h
@@ -0,0 +1,105 @@
+/*********************                                                        */
+/*! \file ambqi_builder.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Morgan Deters, Tim King, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Abstract MBQI model builder class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef ABSTRACT_MBQI_BUILDER
+#define ABSTRACT_MBQI_BUILDER
+
+#include "theory/quantifiers/fmf/model_builder.h"
+#include "theory/quantifiers/first_order_model.h"
+
+namespace CVC4 {
+namespace theory {
+namespace quantifiers {
+
+class FirstOrderModelAbs;
+
+//representiation of function and term interpretations
+class AbsDef
+{
+private:
+  bool addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, TNode q, std::vector< Node >& terms, int& inst, unsigned depth );
+  void construct_compose( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
+                          std::map< unsigned, AbsDef * >& children,
+                          std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
+                          std::vector< unsigned >& entry, std::vector< bool >& entry_def );
+  void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
+  void construct_def_entry( FirstOrderModelAbs * m, TNode q, TNode n, int v, unsigned depth = 0 );
+  void apply_ucompose( FirstOrderModelAbs * m, TNode q,
+                       std::vector< unsigned >& entry, std::vector< bool >& entry_def, std::vector< int >& terms,
+                       std::map< unsigned, int >& vchildren, AbsDef * a, unsigned depth = 0 );
+  void construct_var_eq( FirstOrderModelAbs * m, TNode q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 );
+  void construct_var( FirstOrderModelAbs * m, TNode q, unsigned v, int currv, unsigned depth = 0 );
+  void get_defs( unsigned u, std::vector< AbsDef * >& defs );
+  void construct_normalize( FirstOrderModelAbs * m, TNode q, std::vector< AbsDef * >& defs, unsigned depth = 0 );
+public:
+  enum {
+    val_none = -1,
+    val_unk = -2,
+  };
+  AbsDef() : d_default( 0 ), d_value( -1 ){}
+  std::map< unsigned, AbsDef > d_def;
+  unsigned d_default;
+  int d_value;
+
+  void clear() { d_def.clear(); d_default = 0; d_value = -1; }
+  AbsDef * getDefault() { return &d_def[d_default]; }
+  void construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth = 0 );
+  void debugPrintUInt( const char * c, unsigned dSize, unsigned u ) const;
+  void debugPrint( const char * c, FirstOrderModelAbs * m, TNode f, unsigned depth = 0 ) const;
+  void simplify( FirstOrderModelAbs * m, TNode q, TNode n, unsigned depth = 0 );
+  int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, int& inst ){
+    std::vector< Node > terms;
+    terms.resize( q[0].getNumChildren() );
+    return addInstantiations( m, qe, q, terms, inst, 0 );
+  }
+  bool construct( FirstOrderModelAbs * m, TNode q, TNode n, AbsDef * f,
+                  std::map< unsigned, AbsDef * >& children,
+                  std::map< unsigned, int >& bchildren,
+                  std::map< unsigned, int >& vchildren,
+                  int varChCount );
+  void negate();
+  Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
+  static bool isSimple( unsigned n );
+  static unsigned getId( unsigned n, unsigned start=0, unsigned end=32 );
+  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
+  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
+  //for debugging
+  bool is_normalized();
+};
+
+class AbsMbqiBuilder : public QModelBuilder
+{
+  friend class AbsDef;
+private:
+  Node d_true;
+  Node d_false;
+  bool doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n );
+public:
+  AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe );
+
+  //process build model
+  bool processBuildModel(TheoryModel* m) override;
+  //do exhaustive instantiation
+  int doExhaustiveInstantiation(FirstOrderModel* fm,
+                                Node q,
+                                int effort) override;
+};
+
+}
+}
+}
+
+#endif