From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 6 May 2014 13:19:04 +0000 (-0500)
Subject: First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).
X-Git-Tag: cvc5-1.0.0~6928
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c9404d8ecdfbc6da4fd125cefede7a21a5499e4d;p=cvc5.git

First draft of ambqi_builder (new implementation of MBQI based on disjoint sets).
---

diff --git a/src/Makefile.am b/src/Makefile.am
index e7cc9628e..573181ccf 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -306,6 +306,8 @@ libcvc4_la_SOURCES = \
 	theory/quantifiers/symmetry_breaking.cpp \
 	theory/quantifiers/qinterval_builder.h \
 	theory/quantifiers/qinterval_builder.cpp \
+	theory/quantifiers/ambqi_builder.h \
+	theory/quantifiers/ambqi_builder.cpp \
 	theory/quantifiers/quant_conflict_find.h \
 	theory/quantifiers/quant_conflict_find.cpp \
 	theory/quantifiers/options_handlers.h \
diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
new file mode 100755
index 000000000..7a296c934
--- /dev/null
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -0,0 +1,715 @@
+/*********************                                                        */
+/*! \file ambqi_builder.cpp
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of abstract MBQI builder
+ **/
+
+
+#include "theory/quantifiers/ambqi_builder.h"
+#include "theory/quantifiers/term_database.h"
+
+
+using namespace std;
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::quantifiers;
+
+void AbsDef::construct_func( FirstOrderModelAbs * m, std::vector< TNode >& fapps, unsigned depth ) {
+  d_def.clear();
+  Assert( !fapps.empty() );
+  if( depth==fapps[0].getNumChildren() ){
+    //get representative in model for this term
+    Assert( fapps.size()==1 );
+    d_value = m->getRepresentativeId( fapps[0] );
+    Assert( d_value!=-1 );
+  }else{
+    TypeNode tn = fapps[0][depth].getType();
+    std::map< unsigned, std::vector< TNode > > fapp_child;
+
+    //partition based on evaluations of fapps[1][depth]....fapps[n][depth]
+    for( unsigned i=0; i<fapps.size(); i++ ){
+      unsigned r = m->getRepresentativeId( fapps[i][depth] );
+      Assert( r < 32 );
+      fapp_child[r].push_back( fapps[i] );
+    }
+
+    //do completion
+    std::map< unsigned, unsigned > fapp_child_index;
+    unsigned def = m->d_domain[ tn ];
+    unsigned minSize = fapp_child.begin()->second.size();
+    unsigned minSizeIndex = fapp_child.begin()->first;
+    for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
+      fapp_child_index[it->first] = ( 1 << it->first );
+      def = def & ~( 1 << it->first );
+      if( it->second.size()<minSize ){
+        minSize = it->second.size();
+        minSizeIndex = it->first;
+      }
+    }
+    fapp_child_index[minSizeIndex] |= def;
+    d_default = fapp_child_index[minSizeIndex];
+
+    //construct children
+    for( std::map< unsigned, std::vector< TNode > >::iterator it = fapp_child.begin(); it != fapp_child.end(); ++it ){
+      Trace("abs-model-debug") << "Construct " << it->first << " : " << fapp_child_index[it->first] << " : ";
+      debugPrintUInt( "abs-model-debug", m->d_rep_set.d_type_reps[tn].size(), fapp_child_index[it->first] );
+      Trace("abs-model-debug") << " : " << it->second.size() << " terms." << std::endl;
+      d_def[fapp_child_index[it->first]].construct_func( m, it->second, depth+1 );
+    }
+  }
+}
+
+void AbsDef::simplify( FirstOrderModelAbs * m, Node q, unsigned depth ) {
+  if( d_value==-1 ){
+    //process the default
+    std::map< unsigned, AbsDef >::iterator defd = d_def.find( d_default );
+    unsigned newDef = d_default;
+    std::vector< unsigned > to_erase;
+    defd->second.simplify( m, q, depth+1 );
+    bool isConstant = ( defd->second.d_value!=-1 );
+    //process each child
+    for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
+      if( it->first!=d_default ){
+        it->second.simplify( m, q, depth+1 );
+        if( it->second.d_value==defd->second.d_value && it->second.d_value!=-1 ){
+          newDef = d_default | it->first;
+          to_erase.push_back( it->first );
+        }else{
+          isConstant = false;
+        }
+      }
+    }
+    if( !to_erase.empty() ){
+      //erase old default
+      int defVal = defd->second.d_value;
+      d_def.erase( d_default );
+      //set new default
+      d_default = newDef;
+      d_def[d_default].construct_def_entry( m, q, defVal, depth+1 );
+      //erase redundant entries
+      for( unsigned i=0; i<to_erase.size(); i++ ){
+        d_def.erase( to_erase[i] );
+      }
+    }
+    //if constant, propagate the value upwards
+    if( isConstant ){
+      d_value = defd->second.d_value;
+    }
+  }
+}
+
+void AbsDef::debugPrintUInt( const char * c, unsigned dSize, unsigned u ) {
+  for( unsigned i=0; i<dSize; i++ ){
+    Trace(c) << ( ( u & ( 1 << i ) )!=0 ? "1" : "0");
+  }
+}
+
+void AbsDef::debugPrint( const char * c, FirstOrderModelAbs * m, Node f, unsigned depth ) {
+  if( Trace.isOn(c) ){
+    if( depth==f.getNumChildren() ){
+      for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
+      Trace(c) << "V[" << d_value << "]" << std::endl;
+    }else{
+      TypeNode tn = f[depth].getType();
+      unsigned dSize = m->d_rep_set.d_type_reps[tn].size();
+      Assert( dSize<32 );
+      for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
+        for( unsigned i=0; i<depth; i++ ){ Trace(c) << "  ";}
+        debugPrintUInt( c, dSize, it->first );
+        if( it->first==d_default ){
+          Trace(c) << "*";
+        }
+        if( it->second.d_value!=-1 ){
+          Trace(c) << " -> V[" << it->second.d_value << "]";
+        }
+        Trace(c) << std::endl;
+        it->second.debugPrint( c, m, f, depth+1 );
+      }
+    }
+  }
+}
+
+int AbsDef::addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, std::vector< Node >& terms, unsigned depth ) {
+  if( depth==q[0].getNumChildren() ){
+    if( d_value!=1 ){
+      if( qe->addInstantiation( q, terms ) ){
+        return 1;
+      }
+    }
+    return 0;
+  }else{
+    int sum = 0;
+    TypeNode tn = q[0][depth].getType();
+    for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
+      //get witness term
+      int index = getId( it->first );
+      terms.push_back( m->d_rep_set.d_type_reps[tn][index] );
+      sum += it->second.addInstantiations( m, qe, q, terms, depth+1 );
+      terms.pop_back();
+    }
+    return sum;
+  }
+}
+
+void AbsDef::construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth ) {
+  if( depth==entry.size() ){
+    d_value = v;
+  }else{
+    d_def[entry[depth]].construct_entry( entry, entry_def, v, depth+1 );
+    if( entry_def[depth] ){
+      d_default = entry[depth];
+    }
+  }
+}
+
+void AbsDef::construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth ) {
+  if( depth==q[0].getNumChildren() ){
+    d_value = v;
+  }else{
+    unsigned dom = m->d_domain[q[0][depth].getType()];
+    d_def[dom].construct_def_entry( m, q, v, depth+1 );
+    d_default = dom;
+  }
+}
+
+void AbsDef::apply_ucompose( std::vector< unsigned >& entry, std::vector< bool >& entry_def,
+                             std::vector< int >& terms, std::map< unsigned, int >& vchildren,
+                             AbsDef * a, unsigned depth ) {
+  if( depth==terms.size() ){
+    a->construct_entry( entry, entry_def, d_value );
+  }else{
+    unsigned id;
+    if( terms[depth]==-1 ){
+      //a variable
+      std::map< unsigned, int >::iterator itv = vchildren.find( depth );
+      Assert( itv!=vchildren.end() );
+      unsigned prev_v = entry[itv->second];
+      bool prev_vd = entry_def[itv->second];
+      for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
+        entry[itv->second] = it->first & prev_v;
+        entry_def[itv->second] = ( it->first==d_default ) && prev_vd;
+        if( entry[itv->second]!=0 ){
+          it->second.apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 );
+        }
+      }
+      entry[itv->second] = prev_v;
+      entry_def[itv->second] = prev_vd;
+    }else{
+      id = (unsigned)terms[depth];
+      Assert( id<32 );
+      unsigned fid = 1 << id;
+      std::map< unsigned, AbsDef >::iterator it = d_def.find( fid );
+      if( it!=d_def.end() ){
+        it->second.apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 );
+      }else{
+        d_def[d_default].apply_ucompose( entry, entry_def, terms, vchildren, a, depth+1 );
+      }
+    }
+  }
+}
+
+void AbsDef::construct_var_eq( FirstOrderModelAbs * m, Node q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth ) {
+  if( depth==q[0].getNumChildren() ){
+    Assert( currv!=-1 );
+    d_value = currv;
+  }else{
+    TypeNode tn = q[0][depth].getType();
+    unsigned dom = m->d_domain[tn];
+    int vindex = depth==v1 ? 0 : ( depth==v2 ? 1 : -1 );
+    if( vindex==-1 ){
+      d_def[dom].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
+      d_default = dom;
+    }else{
+      Assert( currv==-1 );
+      if( curr==-1 ){
+        unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
+        Assert( numReps < 32 );
+        for( unsigned i=0; i<numReps; i++ ){
+          curr = 1 << i;
+          d_def[curr].construct_var_eq( m, q, v1, v2, curr, currv, depth+1 );
+        }
+        d_default = curr;
+      }else{
+        d_def[curr].construct_var_eq( m, q, v1, v2, curr, 1, depth+1 );
+        dom = dom & ~curr;
+        d_def[dom].construct_var_eq( m, q, v1, v2, curr, 0, depth+1 );
+        d_default = dom;
+      }
+    }
+  }
+}
+
+void AbsDef::construct_var( FirstOrderModelAbs * m, Node q, unsigned v, int currv, unsigned depth ) {
+  if( depth==q[0].getNumChildren() ){
+    Assert( currv!=-1 );
+    d_value = currv;
+  }else{
+    TypeNode tn = q[0][depth].getType();
+    if( v==depth ){
+      unsigned numReps = m->d_rep_set.d_type_reps[tn].size();
+      Assert( numReps>0 && numReps < 32 );
+      for( unsigned i=0; i<numReps; i++ ){
+        d_def[ 1 << i ].construct_var( m, q, v, i, depth+1 );
+      }
+      d_default = 1 << (numReps-1);
+    }else{
+      unsigned dom = m->d_domain[tn];
+      d_def[dom].construct_var( m, q, v, currv, depth+1 );
+      d_default = dom;
+    }
+  }
+}
+
+void AbsDef::construct_compose( FirstOrderModelAbs * m, Node q, Node 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,
+                                bool incomplete ) {
+  if( Trace.isOn("ambqi-check-debug2") ){
+    for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
+  }
+  if( n.getKind()==OR || n.getKind()==AND ){
+    // short circuiting
+    for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
+      if( ( it->second->d_value==0 && n.getKind()==AND ) ||
+          ( it->second->d_value==1 && n.getKind()==OR ) ){
+        construct_entry( entry, entry_def, it->second->d_value );
+        return;
+      }
+    }
+  }
+  if( entry.size()==q[0].getNumChildren() ){
+    if( incomplete ){
+      //if a child is unknown, we must return unknown
+      construct_entry( entry, entry_def, -1 );
+    }else{
+      if( f ){
+        Trace("ambqi-check-debug2") << "Evaluate uninterpreted function entry..." << std::endl;
+        //we are composing with an uninterpreted function
+        std::vector< int > values;
+        values.resize( n.getNumChildren(), -1 );
+        for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
+          values[it->first] = it->second->d_value;
+        }
+        for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
+          values[it->first] = it->second;
+        }
+        //look up value(s)
+        f->apply_ucompose( entry, entry_def, values, vchildren, this );
+      }else{
+        //we are composing with an interpreted function
+        std::vector< TNode > values;
+        values.resize( n.getNumChildren(), TNode::null() );
+        for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
+          Assert( it->second->d_value>=0 && it->second->d_value<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
+          values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second->d_value];
+          Trace("ambqi-check-debug2") << it->first << " : " << it->second->d_value << " ->> " << values[it->first] << std::endl;
+        }
+        for( std::map< unsigned, int >::iterator it = bchildren.begin(); it != bchildren.end(); ++it ){
+          Assert( it->second>=0 && it->second<(int)m->d_rep_set.d_type_reps[n[it->first].getType()].size() );
+          values[it->first] = m->d_rep_set.d_type_reps[n[it->first].getType()][it->second];
+          Trace("ambqi-check-debug2") << it->first << " : " << it->second << " ->> " << values[it->first] << std::endl;
+        }
+        Assert( vchildren.empty() );
+        if( Trace.isOn("ambqi-check-debug2") ){
+          Trace("ambqi-check-debug2") << "Evaluate interpreted function entry ( ";
+          for( unsigned i=0; i<values.size(); i++ ){
+            Trace("ambqi-check-debug2") << values[i] << " ";
+          }
+          Trace("ambqi-check-debug2") << ")..." << std::endl;
+        }
+        //evaluate
+        Node vv = NodeManager::currentNM()->mkNode( n.getKind(), values );
+        vv = Rewriter::rewrite( vv );
+        int v = m->getRepresentativeId( vv );
+        construct_entry( entry, entry_def, v );
+      }
+    }
+  }else{
+    //take product of arguments
+    TypeNode tn = q[0][entry.size()].getType();
+    unsigned def = m->d_domain[tn];
+    Trace("ambqi-check-debug2") << "Take product of arguments" << std::endl;
+    for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
+      //process each child
+      for( std::map< unsigned, AbsDef >::iterator itd = it->second->d_def.begin(); itd != it->second->d_def.end(); ++itd ){
+        if( itd->first!=it->second->d_default && ( def & itd->first )!=0 ){
+          def &= ~( itd->first );
+          //process this value
+          std::map< unsigned, AbsDef * > cchildren;
+          for( std::map< unsigned, AbsDef * >::iterator it2 = children.begin(); it2 != children.end(); ++it2 ){
+            std::map< unsigned, AbsDef >::iterator itdf = it->second->d_def.find( itd->first );
+            if( itdf!=it->second->d_def.end() ){
+              cchildren[it->first] = &itdf->second;
+            }else{
+              cchildren[it->first] = it2->second->getDefault();
+            }
+          }
+          if( Trace.isOn("ambqi-check-debug2") ){
+            for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
+            Trace("ambqi-check-debug2") << "...process : ";
+            debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), itd->first );
+            Trace("ambqi-check-debug2") << std::endl;
+          }
+          entry.push_back( itd->first );
+          entry_def.push_back( def==0 );
+          construct_compose( m, q, n, f, cchildren, bchildren, vchildren, entry, entry_def, incomplete );
+          entry_def.pop_back();
+          entry.pop_back();
+          if( def==0 ){
+            break;
+          }
+        }
+      }
+      if( def==0 ){
+        break;
+      }
+    }
+    if( def!=0 ){
+      std::map< unsigned, AbsDef * > cdchildren;
+      for( std::map< unsigned, AbsDef * >::iterator it = children.begin(); it != children.end(); ++it ){
+        cdchildren[it->first] = it->second->getDefault();
+      }
+      if( Trace.isOn("ambqi-check-debug2") ){
+        for( unsigned i=0; i<entry.size(); i++ ){ Trace("ambqi-check-debug2") << "  "; }
+        Trace("ambqi-check-debug2") << "...process default : ";
+        debugPrintUInt("ambqi-check-debug2", m->d_rep_set.d_type_reps[tn].size(), def );
+        Trace("ambqi-check-debug2") << std::endl;
+      }
+      entry.push_back( def );
+      entry_def.push_back( true );
+      construct_compose( m, q, n, f, cdchildren, bchildren, vchildren, entry, entry_def, incomplete );
+      entry_def.pop_back();
+      entry.pop_back();
+    }
+  }
+}
+
+bool AbsDef::construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f,
+                        std::map< unsigned, AbsDef * >& children,
+                        std::map< unsigned, int >& bchildren, std::map< unsigned, int >& vchildren,
+                        int varChCount, bool incomplete ) {
+  if( varChCount==0 || f ){
+    //short-circuit
+    if( n.getKind()==AND || n.getKind()==OR ){
+      for( std::map< unsigned, int >::iterator it = bchildren.begin(); it !=bchildren.end(); ++it ){
+        if( ( it->second==0 && n.getKind()==AND ) ||
+            ( it->second==1 && n.getKind()==OR ) ){
+          construct_def_entry( m, q, it->second );
+          return true;
+        }
+      }
+    }
+    Trace("ambqi-check-debug2") << "Construct compose..." << std::endl;
+    std::vector< unsigned > entry;
+    std::vector< bool > entry_def;
+    construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def, incomplete );
+    return true;
+  }else if( varChCount==1 && n.getKind()==EQUAL ){
+    Trace("ambqi-check-debug2") << "Expand variable child..." << std::endl;
+    //expand the variable based on its finite domain
+    AbsDef a;
+    a.construct_var( m, q, vchildren.begin()->second, -1 );
+    children[vchildren.begin()->first] = &a;
+    vchildren.clear();
+    std::vector< unsigned > entry;
+    std::vector< bool > entry_def;
+    Trace("ambqi-check-debug2") << "Construct compose with variable..." << std::endl;
+    construct_compose( m, q, n, f, children, bchildren, vchildren, entry, entry_def, incomplete );
+    return true;
+  }else if( varChCount==2 && n.getKind()==EQUAL ){
+    Trace("ambqi-check-debug2") << "Construct variable equality..." << std::endl;
+    //efficient expansion of the equality
+    construct_var_eq( m, q, vchildren[0], vchildren[1], -1, -1 );
+    return true;
+  }else{
+    return false;
+  }
+}
+
+Node AbsDef::getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth ) {
+  if( depth==vars.size() ){
+    TypeNode tn = op.getType();
+    if( tn.getNumChildren()>0 ){
+      tn = tn[tn.getNumChildren()-1];
+    }
+    if( d_value>=0 ){
+      Assert( d_value<(int)m->d_rep_set.d_type_reps[tn].size() );
+      if( tn.isBoolean() ){
+        return NodeManager::currentNM()->mkConst( d_value==1 );
+      }else{
+        return m->d_rep_set.d_type_reps[tn][d_value];
+      }
+    }else{
+      return Node::null();
+    }
+  }else{
+    TypeNode tn = vars[depth].getType();
+    Node curr;
+    curr = d_def[d_default].getFunctionValue( m, op, vars, depth+1 );
+    for( std::map< unsigned, AbsDef >::iterator it = d_def.begin(); it != d_def.end(); ++it ){
+      if( it->first!=d_default ){
+        unsigned id = getId( it->first );
+        Assert( id<m->d_rep_set.d_type_reps[tn].size() );
+        TNode n = m->d_rep_set.d_type_reps[tn][id];
+        Node fv = it->second.getFunctionValue( m, op, vars, depth+1 );
+        if( !curr.isNull() && !fv.isNull() ){
+          curr = NodeManager::currentNM()->mkNode( ITE, vars[depth].eqNode( n ), fv, curr );
+        }else{
+          curr = Node::null();
+        }
+      }
+    }
+    return curr;
+  }
+}
+
+unsigned AbsDef::getId( unsigned n ) {
+  Assert( n!=0 );
+  unsigned index = 0;
+  while( (n & ( 1 << index )) == 0 ){
+    index++;
+  }
+  return index;
+}
+
+Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< Node >& args ) {
+  std::vector< unsigned > iargs;
+  for( unsigned i=0; i<args.size(); i++ ){
+    unsigned v = 1 << m->getRepresentativeId( args[i] );
+    iargs.push_back( v );
+  }
+  return evaluate( m, retTyp, iargs, 0 );
+}
+
+Node AbsDef::evaluate( FirstOrderModelAbs * m, TypeNode retTyp, std::vector< unsigned >& iargs, unsigned depth ) {
+  if( d_value!=-1 ){
+    Assert( d_value>=0 && d_value<(int)m->d_rep_set.d_type_reps[retTyp].size() );
+    return m->d_rep_set.d_type_reps[retTyp][d_value];
+  }else{
+    std::map< unsigned, AbsDef >::iterator it = d_def.find( iargs[depth] );
+    if( it==d_def.end() ){
+      return d_def[d_default].evaluate( m, retTyp, iargs, depth+1 );
+    }else{
+      return it->second.evaluate( m, retTyp, iargs, depth+1 );
+    }
+  }
+}
+
+AbsMbqiBuilder::AbsMbqiBuilder( context::Context* c, QuantifiersEngine* qe ) :
+QModelBuilder( c, qe ){
+  d_true = NodeManager::currentNM()->mkConst( true );
+  d_false = NodeManager::currentNM()->mkConst( false );
+}
+
+
+//------------------------model construction----------------------------
+
+void AbsMbqiBuilder::processBuildModel(TheoryModel* m, bool fullModel) {
+  Trace("ambqi-debug") << "process build model " << fullModel << std::endl;
+  FirstOrderModel* f = (FirstOrderModel*)m;
+  FirstOrderModelAbs* fm = f->asFirstOrderModelAbs();
+  if( fullModel ){
+    Trace("ambqi-model") << "Construct model representation..." << std::endl;
+    //make function values
+    for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      if( it->first.getType().getNumChildren()>1 ){
+        Trace("ambqi-model") << "Construct for " << it->first << "..." << std::endl;
+        m->d_uf_models[ it->first ] = fm->getFunctionValue( it->first, "$x" );
+      }
+    }
+    TheoryEngineModelBuilder::processBuildModel( m, fullModel );
+    //mark that the model has been set
+    fm->markModelSet();
+    //debug the model
+    debugModel( fm );
+  }else{
+    fm->initialize( d_considerAxioms );
+    //process representatives
+    fm->d_rep_id.clear();
+    fm->d_domain.clear();
+
+    //initialize boolean sort
+    TypeNode b = d_true.getType();
+    fm->d_rep_set.d_type_reps[b].clear();
+    fm->d_rep_set.d_type_reps[b].push_back( d_false );
+    fm->d_rep_set.d_type_reps[b].push_back( d_true );
+    fm->d_rep_id[d_false] = 0;
+    fm->d_rep_id[d_true] = 1;
+
+    //initialize unintpreted sorts
+    Trace("ambqi-model") << std::endl << "Making representatives..." << std::endl;
+    for( std::map< TypeNode, std::vector< Node > >::iterator it = fm->d_rep_set.d_type_reps.begin();
+         it != fm->d_rep_set.d_type_reps.end(); ++it ){
+      if( it->first.isSort() ){
+        Assert( !it->second.empty() );
+        //set the domain
+        fm->d_domain[it->first] = 0;
+        Trace("ambqi-model") << "Representatives for " << it->first << " : " << std::endl;
+        for( unsigned i=0; i<it->second.size(); i++ ){
+          if( i<32 ){
+            fm->d_domain[it->first] |= ( 1 << i );
+          }
+          Trace("ambqi-model") << i << " : " << it->second[i] << std::endl;
+          fm->d_rep_id[it->second[i]] = i;
+        }
+        if( it->second.size()>=32 ){
+          fm->d_domain.erase( it->first );
+        }
+      }
+    }
+
+    Trace("ambqi-model") << std::endl << "Making function definitions..." << std::endl;
+    //construct the models for functions
+    for( std::map<Node, AbsDef * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      Node f = it->first;
+      Trace("ambqi-model-debug") << "Building Model for " << f << std::endl;
+      //reset the model
+      //get all (non-redundant) f-applications
+      std::vector< TNode > fapps;
+      Trace("ambqi-model-debug") << "Initial terms: " << std::endl;
+      for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+        Node n = fm->d_uf_terms[f][i];
+        if( !n.getAttribute(NoMatchAttribute()) ){
+          Trace("ambqi-model-debug") << "  " << n << " -> " << fm->getRepresentativeId( n ) << std::endl;
+          fapps.push_back( n );
+        }
+      }
+      if( fapps.empty() ){
+        //choose arbitrary value
+        Node mbt = d_qe->getTermDatabase()->getModelBasisOpTerm(f);
+        Trace("ambqi-model-debug") << "Initial terms empty, add " << mbt << std::endl;
+        fapps.push_back( mbt );
+      }
+      bool fValid = true;
+      for( unsigned i=0; i<fapps[0].getNumChildren(); i++ ){
+        if( fm->d_domain.find( fapps[0][i].getType() )==fm->d_domain.end() ){
+          Trace("ambqi-model") << "Interpretation of " << f << " is not valid.";
+          Trace("ambqi-model") << " (domain for " << fapps[0][i].getType() << " is too large)." << std::endl;
+          fValid = false;
+          break;
+        }
+      }
+      fm->d_models_valid[f] = fValid;
+      if( fValid ){
+        //construct the ambqi model
+        it->second->construct_func( fm, fapps );
+        Trace("ambqi-model-debug") << "Interpretation of " << f << " : " << std::endl;
+        it->second->debugPrint("ambqi-model-debug", fm, fapps[0] );
+
+        it->second->simplify( fm, Node::null() );
+        Trace("ambqi-model") << "(Simplified) interpretation of " << f << " : " << std::endl;
+        it->second->debugPrint("ambqi-model", fm, fapps[0] );
+
+/*
+        if( Debug.isOn("ambqi-model-debug") ){
+          for( size_t i=0; i<fm->d_uf_terms[f].size(); i++ ){
+            Node e = it->second->evaluate_n( fm, fm->d_uf_terms[f][i] );
+            Debug("ambqi-model-debug") << fm->d_uf_terms[f][i] << " evaluates to " << e << std::endl;
+            Assert( fm->areEqual( e, fm->d_uf_terms[f][i] ) );
+          }
+        }
+*/
+      }
+    }
+  }
+}
+
+
+//--------------------model checking---------------------------------------
+
+//do exhaustive instantiation
+bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, int effort ) {
+  Trace("ambqi-check") << "exhaustive instantiation " << q << " " << effort << std::endl;
+  if (effort==0) {
+    FirstOrderModelAbs * fma = fm->asFirstOrderModelAbs();
+    bool quantValid = true;
+    for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
+      if( !fma->isValidType( q[0][i].getType() ) ){
+        quantValid = false;
+        Trace("ambqi-inst") << "Interpretation of " << q << " is not valid because of type " << q[0][i].getType() << std::endl;
+        break;
+      }
+    }
+    if( quantValid ){
+      AbsDef ad;
+      doCheck( fma, q, ad, q[1] );
+      //now process entries
+      Trace("ambqi-inst") << "Interpretation of " << q << " is : " << std::endl;
+      ad.debugPrint( "ambqi-inst", fma, q );
+      Trace("ambqi-inst") << std::endl;
+      int lem = ad.addInstantiations( fma, d_qe, q );
+      Trace("ambqi-inst") << "...Added " << lem << " lemmas." << std::endl;
+      d_addedLemmas += lem;
+    }
+    return quantValid;
+  }
+  return true;
+}
+
+bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {
+  Assert( n.getKind()!=FORALL );
+  std::map< unsigned, AbsDef > children;
+  std::map< unsigned, int > bchildren;
+  std::map< unsigned, int > vchildren;
+  bool incomplete = false;
+  int varChCount = 0;
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    if( n[i].getKind()==FORALL ){
+      bchildren[i] = -1;
+      incomplete = true;
+    }else if( n[i].getKind() == BOUND_VARIABLE ){
+      varChCount++;
+      vchildren[i] = m->getVariableId( q, n[i] );
+    }else if( m->hasTerm( n[i] ) ){
+      bchildren[i] = m->getRepresentativeId( n[i] );
+    }else{
+      if( !doCheck( m, q, children[i], n[i] ) ){
+        bchildren[i] = -1;
+        incomplete = true;
+      }
+    }
+  }
+  //convert to pointers
+  std::map< unsigned, AbsDef * > pchildren;
+  for( std::map< unsigned, AbsDef >::iterator it = children.begin(); it != children.end(); ++it ){
+    pchildren[it->first] = &it->second;
+  }
+  //construct the interpretation
+  Trace("ambqi-check-debug") << "Compute Interpretation of " << n << " " << n.getKind() << std::endl;
+  if( n.getKind() == APPLY_UF || n.getKind() == VARIABLE || n.getKind() == SKOLEM ){
+    Node op;
+    if( n.getKind() == APPLY_UF ){
+      op = n.getOperator();
+    }else{
+      op = n;
+    }
+    //uninterpreted compose
+    if( m->d_models_valid[op] ){
+      ad.construct( m, q, n, m->d_models[op], pchildren, bchildren, vchildren, varChCount, incomplete );
+    }else{
+      Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (no function model)" << std::endl;
+      return false;
+    }
+  }else if( !ad.construct( m, q, n, NULL, pchildren, bchildren, vchildren, varChCount, incomplete ) ){
+    Trace("ambqi-check-debug") << "** Cannot produce interpretation for " << n << " (variables are children of interpreted symbol)" << std::endl;
+    return false;
+  }
+  Trace("ambqi-check-debug2") << "Interpretation for " << n << " is : " << std::endl;
+  ad.debugPrint("ambqi-check-debug2", m, q[0] );
+  ad.simplify( m, q );
+  Trace("ambqi-check-debug") << "(Simplified) Interpretation for " << n << " is : " << std::endl;
+  ad.debugPrint("ambqi-check-debug", m, q[0] );
+  Trace("ambqi-check-debug") << std::endl;
+  return true;
+}
diff --git a/src/theory/quantifiers/ambqi_builder.h b/src/theory/quantifiers/ambqi_builder.h
new file mode 100755
index 000000000..d0818a784
--- /dev/null
+++ b/src/theory/quantifiers/ambqi_builder.h
@@ -0,0 +1,90 @@
+/*********************                                                        */
+/*! \file ambqi_builder.h
+ ** \verbatim
+ ** Original author: Andrew Reynolds
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013  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:
+  int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q, std::vector< Node >& terms, unsigned depth );
+  void construct_compose( FirstOrderModelAbs * m, Node q, Node 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,
+                          bool incomplete );
+  void construct_entry( std::vector< unsigned >& entry, std::vector< bool >& entry_def, int v, unsigned depth = 0 );
+  void construct_def_entry( FirstOrderModelAbs * m, Node q, int v, unsigned depth = 0 );
+  void apply_ucompose( 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, Node q, unsigned v1, unsigned v2, int curr, int currv, unsigned depth = 0 );
+  void construct_var( FirstOrderModelAbs * m, Node q, unsigned v, int currv, unsigned depth = 0 );
+public:
+  AbsDef() : d_value( -1 ){}
+  std::map< unsigned, AbsDef > d_def;
+  unsigned d_default;
+  int d_value;
+
+  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 );
+  void debugPrint( const char * c, FirstOrderModelAbs * m, Node f, unsigned depth = 0 );
+  void simplify( FirstOrderModelAbs * m, Node q, unsigned depth = 0 );
+  int addInstantiations( FirstOrderModelAbs * m, QuantifiersEngine * qe, Node q ){
+    std::vector< Node > terms;
+    return addInstantiations( m, qe, q, terms, 0 );
+  }
+  bool construct( FirstOrderModelAbs * m, Node q, Node n, AbsDef * f,
+                  std::map< unsigned, AbsDef * >& children,
+                  std::map< unsigned, int >& bchildren,
+                  std::map< unsigned, int >& vchildren,
+                  int varChCount, bool incomplete );
+  Node getFunctionValue( FirstOrderModelAbs * m, TNode op, std::vector< Node >& vars, unsigned depth = 0 );
+  static unsigned getId( unsigned n );
+  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< Node >& args );
+  Node evaluate( FirstOrderModelAbs * m, TypeNode retType, std::vector< unsigned >& iargs, unsigned depth = 0 );
+};
+
+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
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index 509c00bb6..0b2fae5d4 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -18,6 +18,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/qinterval_builder.h"
+#include "theory/quantifiers/ambqi_builder.h"
 #include "theory/quantifiers/options.h"
 
 #define USE_INDEX_ORDERING
@@ -882,3 +883,101 @@ bool FirstOrderModelQInt::doMeet( Node l1, Node u1, Node l2, Node u2, Node& lr,
   //return lr==ur || lr.isNull() || isLessThan( lr, ur );
   return lr.isNull() || isLessThan( lr, ur );
 }
+
+
+
+
+FirstOrderModelAbs::FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name) :
+FirstOrderModel(qe, c, name) {
+
+}
+
+void FirstOrderModelAbs::processInitialize( bool ispre ) {
+  if( !ispre ){
+    Trace("ambqi-debug") << "Process initialize" << std::endl;
+    for( std::map<Node, AbsDef * >::iterator it = d_models.begin(); it != d_models.end(); ++it ) {
+      Node op = it->first;
+      TypeNode tno = op.getType();
+      Trace("ambqi-debug") << "  Init " << op << " " << tno << std::endl;
+      for( unsigned i=0; i<tno.getNumChildren(); i++) {
+        //make sure a representative of the type exists
+        if( !d_rep_set.hasType( tno[i] ) ){
+          Node e = getSomeDomainElement( tno[i] );
+          Trace("ambqi-debug") << "  * Initialize type " << tno[i] << ", add ";
+          Trace("ambqi-debug") << e << " " << e.getType() << std::endl;
+          //d_rep_set.add( e );
+        }
+      }
+    }
+  }
+}
+
+unsigned FirstOrderModelAbs::getRepresentativeId( TNode n ) {
+  TNode r = getUsedRepresentative( n );
+  std::map< TNode, unsigned >::iterator it = d_rep_id.find( r );
+  if( it!=d_rep_id.end() ){
+    return it->second;
+  }else{
+    return 0;
+  }
+}
+
+TNode FirstOrderModelAbs::getUsedRepresentative( TNode n ) {
+  if( hasTerm( n ) ){
+    if( n.getType().isBoolean() ){
+      return areEqual(n, d_true) ? d_true : d_false;
+    }else{
+      return getRepresentative( n );
+    }
+  }else{
+    Trace("qint-debug") << "Get rep " << n << " " << n.getType() << std::endl;
+    Assert( d_rep_set.hasType( n.getType() ) && !d_rep_set.d_type_reps[n.getType()].empty() );
+    return d_rep_set.d_type_reps[n.getType()][0];
+  }
+}
+
+Node FirstOrderModelAbs::getFunctionValue(Node op, const char* argPrefix ) {
+  if( d_models_valid[op] ){
+    Trace("ambqi-debug") << "Get function value for " << op << std::endl;
+    TypeNode type = op.getType();
+    std::vector< Node > vars;
+    for( size_t i=0; i<type.getNumChildren()-1; i++ ){
+      std::stringstream ss;
+      ss << argPrefix << (i+1);
+      Node b = NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] );
+      vars.push_back( b );
+    }
+    Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
+    Node curr = d_models[op]->getFunctionValue( this, op, vars );
+    Node fv = NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
+    Trace("ambqi-debug") << "Return " << fv << std::endl;
+    return fv;
+  }else{
+
+  }
+  return Node::null();
+}
+
+Node FirstOrderModelAbs::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
+  Debug("qint-debug") << "get curr uf value " << n << std::endl;
+  if( d_models_valid[n] ){
+    TypeNode tn = n.getType();
+    if( tn.getNumChildren()>0 ){
+      tn = tn[tn.getNumChildren()-1];
+    }
+    return d_models[n]->evaluate( this, tn, args );
+  }else{
+    return Node::null();
+  }
+}
+
+void FirstOrderModelAbs::processInitializeModelForTerm( Node n ) {
+  if( n.getKind()==APPLY_UF || n.getKind()==VARIABLE || n.getKind()==SKOLEM ){
+    Node op = n.getKind()==APPLY_UF ? n.getOperator() : n;
+    if( d_models.find(op)==d_models.end()) {
+      Trace("abmqi-debug") << "init model for " << op << std::endl;
+      d_models[op] = new AbsDef;
+      d_models_valid[op] = false;
+    }
+  }
+}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 63d8ffcce..d799cfad3 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -37,6 +37,7 @@ namespace fmcheck {
 }/* CVC4::theory::quantifiers::fmcheck namespace */
 
 class FirstOrderModelQInt;
+class FirstOrderModelAbs;
 
 struct IsStarAttributeId {};
 typedef expr::Attribute<IsStarAttributeId, bool> IsStarAttribute;
@@ -75,6 +76,7 @@ public:
   virtual FirstOrderModelIG * asFirstOrderModelIG() { return NULL; }
   virtual fmcheck::FirstOrderModelFmc * asFirstOrderModelFmc() { return NULL; }
   virtual FirstOrderModelQInt * asFirstOrderModelQInt() { return NULL; }
+  virtual FirstOrderModelAbs * asFirstOrderModelAbs() { return NULL; }
   // initialize the model
   void initialize( bool considerAxioms = true );
   virtual void processInitialize( bool ispre ) = 0;
@@ -220,6 +222,27 @@ public:
   int getOrderedVarNumToVarNum( Node q, int i );
 };/* class FirstOrderModelQInt */
 
+class AbsDef;
+
+class FirstOrderModelAbs : public FirstOrderModel
+{
+public:
+  std::map< Node, AbsDef * > d_models;
+  std::map< Node, bool > d_models_valid;
+  std::map< TNode, unsigned > d_rep_id;
+  std::map< TypeNode, unsigned > d_domain;
+  /** get current model value */
+  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
+  void processInitializeModelForTerm(Node n);
+public:
+  FirstOrderModelAbs(QuantifiersEngine * qe, context::Context* c, std::string name);
+  FirstOrderModelAbs * asFirstOrderModelAbs() { return this; }
+  void processInitialize( bool ispre );
+  unsigned getRepresentativeId( TNode n );
+  TNode getUsedRepresentative( TNode n );
+  bool isValidType( TypeNode tn ) { return d_domain.find( tn )!=d_domain.end(); }
+  Node getFunctionValue(Node op, const char* argPrefix );
+};
 
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
diff --git a/src/theory/quantifiers/model_engine.cpp b/src/theory/quantifiers/model_engine.cpp
index 3a4879b42..dfbc01414 100644
--- a/src/theory/quantifiers/model_engine.cpp
+++ b/src/theory/quantifiers/model_engine.cpp
@@ -23,6 +23,7 @@
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/full_model_check.h"
 #include "theory/quantifiers/qinterval_builder.h"
+#include "theory/quantifiers/ambqi_builder.h"
 
 using namespace std;
 using namespace CVC4;
@@ -44,6 +45,9 @@ QuantifiersModule( qe ){
   }else if( options::mbqiMode()==MBQI_INTERVAL ){
     Trace("model-engine-debug") << "...make interval builder." << std::endl;
     d_builder = new QIntervalBuilder( c, qe );
+  }else if( options::mbqiMode()==MBQI_ABS ){
+    Trace("model-engine-debug") << "...make abs mbqi builder." << std::endl;
+    d_builder = new AbsMbqiBuilder( c, qe );
   }else if( options::mbqiMode()==MBQI_INST_GEN ){
     Trace("model-engine-debug") << "...make inst-gen builder." << std::endl;
     d_builder = new QModelBuilderInstGen( c, qe );
diff --git a/src/theory/quantifiers/modes.cpp b/src/theory/quantifiers/modes.cpp
index 8bd97a8a7..b24721170 100644
--- a/src/theory/quantifiers/modes.cpp
+++ b/src/theory/quantifiers/modes.cpp
@@ -94,6 +94,9 @@ std::ostream& operator<<(std::ostream& out, theory::quantifiers::MbqiMode mode)
   case theory::quantifiers::MBQI_INTERVAL:
     out << "MBQI_INTERVAL";
     break;
+  case theory::quantifiers::MBQI_ABS:
+    out << "MBQI_ABS";
+    break;
   case theory::quantifiers::MBQI_TRUST:
     out << "MBQI_TRUST";
     break;
diff --git a/src/theory/quantifiers/modes.h b/src/theory/quantifiers/modes.h
index 80534c8b0..230495f1f 100644
--- a/src/theory/quantifiers/modes.h
+++ b/src/theory/quantifiers/modes.h
@@ -70,6 +70,8 @@ typedef enum {
   MBQI_FMC_INTERVAL,
   /** mbqi with interval abstraction of uninterpreted sorts */
   MBQI_INTERVAL,
+  /** abstract mbqi algorithm */
+  MBQI_ABS,
   /** mbqi trust (produce no instantiations) */
   MBQI_TRUST,
 } MbqiMode;
diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index b7e624a66..c0b76bcec 100644
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -101,6 +101,9 @@ fmc-interval \n\
 interval \n\
 + Use algorithm that abstracts domain elements as intervals. \n\
 \n\
+abs \n\
++ Use abstract MBQI algorithm (uses disjoint sets). \n\
+\n\
 ";
 static const std::string qcfWhenModeHelp = "\
 Quantifier conflict find modes currently supported by the --quant-cf-when option:\n\
@@ -226,6 +229,8 @@ inline MbqiMode stringToMbqiMode(std::string option, std::string optarg, SmtEngi
     return MBQI_FMC_INTERVAL;
   } else if(optarg == "interval") {
     return MBQI_INTERVAL;
+  } else if(optarg == "abs") {
+    return MBQI_ABS;
   } else if(optarg == "trust") {
     return MBQI_TRUST;
   } else if(optarg == "help") {
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index b79c0da69..929a638d7 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -60,6 +60,8 @@ d_lemmas_produced_c(u){
     d_model = new quantifiers::fmcheck::FirstOrderModelFmc( this, c, "FirstOrderModelFmc" );
   }else if( options::mbqiMode()==quantifiers::MBQI_INTERVAL ){
     d_model = new quantifiers::FirstOrderModelQInt( this, c, "FirstOrderModelQInt" );
+  }else if( options::mbqiMode()==quantifiers::MBQI_ABS ){
+    d_model = new quantifiers::FirstOrderModelAbs( this, c, "FirstOrderModelAbs" );
   }else{
     d_model = new quantifiers::FirstOrderModelIG( this, c, "FirstOrderModelIG" );
   }