text: /*********************                                                        */
  /*! \file ambqi_builder.h
   ** \verbatim
   ** Original author: Andrew Reynolds
   ** Major contributors: Morgan Deters
   ** Minor contributors (to current version): none
   ** This file is part of the CVC4 project.
   ** Copyright (c) 2009-2014  New York University and The University of Iowa
   ** 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/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
    void processBuildModel(TheoryModel* m, bool fullModel);
    //do exhaustive instantiation
    bool doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort );
  };
  
  }
  }
  }
  
  #endif
  