1 files changed, 0 insertions, 105 deletions
diff --git a/src/theory/quantifiers/fmf/ambqi_builder.h b/src/theory/quantifiers/fmf/ambqi_builder.h
deleted file mode 100644
index b052e0985..000000000
--- a/src/theory/quantifiers/fmf/ambqi_builder.h
+++ /dev/null
@@ -1,105 +0,0 @@
-/*********************                                                        */
-/*! \file ambqi_builder.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Andrew Reynolds, Tim King
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 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