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

10 files changed, 945 insertions, 0 deletions

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" );
   }