From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Jun 2013 17:12:30 +0000 (-0500)
Subject: Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds... 
X-Git-Tag: cvc5-1.0.0~7287^2~112
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=25a01d31bffcdcc339dce332ac893460b5f4cdcf;p=cvc5.git

Add partial support for MBQI with arrays when using --fmf-fmc.  Fix constant bounds for bounded integers.
---

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e33cd2131..e402a8969 100755
--- a/src/theory/quantifiers/bounded_integers.cpp
+++ b/src/theory/quantifiers/bounded_integers.cpp
@@ -184,7 +184,7 @@ void BoundedIntegers::processLiteral( Node f, Node lit, bool pol ) {
       }
     }
   }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {
-    std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
+    Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;
     exit(0);
   }
 }
@@ -283,11 +283,13 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           d_range[f][v] = new_range;
           r = new_range;
         }
-        if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
-          Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;
-          d_ranges.push_back( r );
-          d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
-          d_rms[r]->initialize();
+        if( r.getKind()!=CONST_RATIONAL ){
+          if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){
+            Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;
+            d_ranges.push_back( r );
+            d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );
+            d_rms[r]->initialize();
+          }
         }
       }
     }
diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index cf4381c02..4b101de49 100644
--- a/src/theory/quantifiers/first_order_model.cpp
+++ b/src/theory/quantifiers/first_order_model.cpp
@@ -25,6 +25,7 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 using namespace CVC4::theory::quantifiers;
+using namespace CVC4::theory::quantifiers::fmcheck;
 
 FirstOrderModel::FirstOrderModel( context::Context* c, std::string name ) : TheoryModel( c, name, true ),
 d_axiom_asserted( c, false ), d_forall_asserts( c ), d_isModelSet( c, false ){
@@ -507,4 +508,128 @@ Node FirstOrderModelIG::getCurrentUfModelValue( Node n, std::vector< Node > & ar
   }else{
     return d_eval_uf_model[ nv ].getValue( this, nv, argDepIndex );
   }
-}
\ No newline at end of file
+}
+
+
+
+
+
+
+FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
+FirstOrderModel(c, name), d_qe(qe){
+
+}
+
+Node FirstOrderModelFmc::getUsedRepresentative(Node n, bool strict) {
+  //Assert( fm->hasTerm(n) );
+  TypeNode tn = n.getType();
+  if( tn.isBoolean() ){
+    return areEqual(n, d_true) ? d_true : d_false;
+  }else{
+    if( !hasTerm(n) ){
+      if( strict ){
+        return Node::null();
+      }else{
+        Trace("fmc-warn") << "WARNING : no representative for " << n << std::endl;
+      }
+    }
+    Node r = getRepresentative(n);
+    if( d_model_basis_rep.find(tn)!=d_model_basis_rep.end() ){
+      if (r==d_model_basis_rep[tn]) {
+        r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+      }
+    }
+    return r;
+  }
+}
+
+Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
+  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
+  for(unsigned i=0; i<args.size(); i++) {
+    args[i] = getUsedRepresentative(args[i]);
+  }
+  Assert( n.getKind()==APPLY_UF );
+  return d_models[n.getOperator()]->evaluate(this, args);
+}
+
+void FirstOrderModelFmc::processInitialize() {
+  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
+    it->second->reset();
+  }
+  d_model_basis_rep.clear();
+}
+
+void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
+  if( n.getKind()==APPLY_UF ){
+    if( d_models.find(n.getOperator())==d_models.end()) {
+      d_models[n.getOperator()] = new Def;
+    }
+  }
+}
+
+Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){
+  //check if there is even any domain elements at all
+  if (!d_rep_set.hasType(tn)) {
+    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
+    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+    d_rep_set.d_type_reps[tn].push_back(mbt);
+  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
+    Message() << "empty reps" << std::endl;
+    exit(0);
+  }
+  return d_rep_set.d_type_reps[tn][0];
+}
+
+
+bool FirstOrderModelFmc::isStar(Node n) {
+  return n==getStar(n.getType());
+}
+
+Node FirstOrderModelFmc::getStar(TypeNode tn) {
+  if( d_type_star.find(tn)==d_type_star.end() ){
+    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
+    d_type_star[tn] = st;
+  }
+  return d_type_star[tn];
+}
+
+bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
+  return n==getModelBasisTerm(n.getType());
+}
+
+Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {
+  return d_qe->getTermDatabase()->getModelBasisTerm(tn);
+}
+
+Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
+  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);
+    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
+  }
+  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
+  Node curr;
+  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
+    Node v = getUsedRepresentative( d_models[op]->d_value[i] );
+    if( curr.isNull() ){
+      curr = v;
+    }else{
+      //make the condition
+      Node cond = d_models[op]->d_cond[i];
+      std::vector< Node > children;
+      for( unsigned j=0; j<cond.getNumChildren(); j++) {
+        if (!isStar(cond[j])){
+          Node c = getUsedRepresentative( cond[j] );
+          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
+        }
+      }
+      Assert( !children.empty() );
+      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
+      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
+    }
+  }
+  curr = Rewriter::rewrite( curr );
+  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
+}
diff --git a/src/theory/quantifiers/first_order_model.h b/src/theory/quantifiers/first_order_model.h
index 491e97097..c2d82cc0a 100644
--- a/src/theory/quantifiers/first_order_model.h
+++ b/src/theory/quantifiers/first_order_model.h
@@ -120,6 +120,42 @@ private:
 };
 
 
+namespace fmcheck {
+
+class Def;
+
+class FirstOrderModelFmc : public FirstOrderModel
+{
+  friend class FullModelChecker;
+private:
+  /** quant engine */
+  QuantifiersEngine * d_qe;
+  /** models for UF */
+  std::map<Node, Def * > d_models;
+  std::map<TypeNode, Node > d_model_basis_rep;
+  std::map<TypeNode, Node > d_type_star;
+  Node getUsedRepresentative(Node n, bool strict = false);
+  /** get current model value */
+  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
+  void processInitializeModelForTerm(Node n);
+public:
+  FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
+  FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
+  // initialize the model
+  void processInitialize();
+
+  Node getFunctionValue(Node op, const char* argPrefix );
+
+  bool isStar(Node n);
+  Node getStar(TypeNode tn);
+  bool isModelBasisTerm(Node n);
+  Node getModelBasisTerm(TypeNode tn);
+  Node getSomeDomainElement(TypeNode tn);
+};
+
+}
+
+
 }/* CVC4::theory::quantifiers namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 2513cb08e..b16115749 100755
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -190,119 +190,6 @@ void Def::debugPrint(const char * tr, Node op, FullModelChecker * m) {
 }
 
 
-
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :
-FirstOrderModel(c, name), d_qe(qe){
-
-}
-
-Node FirstOrderModelFmc::getUsedRepresentative(Node n) {
-  //Assert( fm->hasTerm(n) );
-  TypeNode tn = n.getType();
-  if( tn.isBoolean() ){
-    return areEqual(n, d_true) ? d_true : d_false;
-  }else{
-    Node r = getRepresentative(n);
-    if (r==d_model_basis_rep[tn]) {
-      r = d_qe->getTermDatabase()->getModelBasisTerm(tn);
-    }
-    return r;
-  }
-}
-
-Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {
-  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;
-  for(unsigned i=0; i<args.size(); i++) {
-    args[i] = getUsedRepresentative(args[i]);
-  }
-  Assert( n.getKind()==APPLY_UF );
-  return d_models[n.getOperator()]->evaluate(this, args);
-}
-
-void FirstOrderModelFmc::processInitialize() {
-  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){
-    it->second->reset();
-  }
-  d_model_basis_rep.clear();
-}
-
-void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {
-  if( n.getKind()==APPLY_UF ){
-    if( d_models.find(n.getOperator())==d_models.end()) {
-      d_models[n.getOperator()] = new Def;
-    }
-  }
-}
-
-Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){
-  //check if there is even any domain elements at all
-  if (!d_rep_set.hasType(tn)) {
-    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;
-    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);
-    d_rep_set.d_type_reps[tn].push_back(mbt);
-  }else if( d_rep_set.d_type_reps[tn].size()==0 ){
-    Message() << "empty reps" << std::endl;
-    exit(0);
-  }
-  return d_rep_set.d_type_reps[tn][0];
-}
-
-
-bool FirstOrderModelFmc::isStar(Node n) {
-  return n==getStar(n.getType());
-}
-
-Node FirstOrderModelFmc::getStar(TypeNode tn) {
-  if( d_type_star.find(tn)==d_type_star.end() ){
-    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );
-    d_type_star[tn] = st;
-  }
-  return d_type_star[tn];
-}
-
-bool FirstOrderModelFmc::isModelBasisTerm(Node n) {
-  return n==getModelBasisTerm(n.getType());
-}
-
-Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {
-  return d_qe->getTermDatabase()->getModelBasisTerm(tn);
-}
-
-Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {
-  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);
-    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );
-  }
-  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);
-  Node curr;
-  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {
-    Node v = getUsedRepresentative( d_models[op]->d_value[i] );
-    if( curr.isNull() ){
-      curr = v;
-    }else{
-      //make the condition
-      Node cond = d_models[op]->d_cond[i];
-      std::vector< Node > children;
-      for( unsigned j=0; j<cond.getNumChildren(); j++) {
-        if (!isStar(cond[j])){
-          Node c = getUsedRepresentative( cond[j] );
-          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );
-        }
-      }
-      Assert( !children.empty() );
-      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );
-      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );
-    }
-  }
-  curr = Rewriter::rewrite( curr );
-  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);
-}
-
-
-
 FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :
 QModelBuilder( c, qe ){
   d_true = NodeManager::currentNM()->mkConst(true);
@@ -369,6 +256,18 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         }
       }
     }
+    //also process non-rep set sorts
+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
+      Node op = it->first;
+      TypeNode tno = op.getType();
+      for( unsigned i=0; i<tno.getNumChildren(); i++) {
+        TypeNode tn = tno[i];
+        if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){
+          Node mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);
+          fm->d_model_basis_rep[tn] = fm->getUsedRepresentative( mbn );
+        }
+      }
+    }
     //now, make models
     for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {
       Node op = it->first;
@@ -397,7 +296,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         Trace("fmc-model-debug") << "Add default " << nmb << std::endl;
         addEntry(fm, op, nmb, nmb, conds, values, entry_conds);
       }else{
-        Node vmb = fm->getSomeDomainElement(nmb.getType());
+        Node vmb = getSomeDomainElement(fm, nmb.getType());
         Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";
         Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;
         addEntry(fm, op, nmb, vmb, conds, values, entry_conds);
@@ -570,30 +469,24 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Nod
   if( riter.setQuantifier( f ) ){
     std::vector< RepDomain > dom;
     for (unsigned i=0; i<c.getNumChildren(); i++) {
-      TypeNode tn = c[i].getType();
-      if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
-        //RepDomain rd;
-        if( fm->isStar(c[i]) ){
-          //add the full range
-          //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();
-          //     it != d_rep_ids[tn].end(); ++it ){
-          //  rd.push_back(it->second);
-          //}
-        }else{
-          if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
-            //rd.push_back(d_rep_ids[tn][c[i]]);
-            riter.d_domain[i].clear();
-            riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+      if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {
+        TypeNode tn = c[i].getType();
+        if( d_rep_ids.find(tn)!=d_rep_ids.end() ){
+          if( fm->isStar(c[i]) ){
+            //add the full range
           }else{
-            return -1;
+            if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {
+              riter.d_domain[i].clear();
+              riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);
+            }else{
+              return -1;
+            }
           }
+        }else{
+          return -1;
         }
-        //dom.push_back(rd);
-      }else{
-        return -1;
       }
     }
-    //riter.setDomain(dom);
     //now do full iteration
     while( !riter.isFinished() ){
       Trace("fmc-exh-debug") << "Inst : ";
@@ -633,14 +526,6 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     d.addEntry(fm, mkCondDefault(fm, f), n);
     Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;
   }
-  else if( n.getNumChildren()==0 ){
-    Node r = n;
-    if( !fm->hasTerm(n) ){
-      r = fm->getSomeDomainElement(n.getType() );
-    }
-    r = fm->getUsedRepresentative( r);
-    d.addEntry(fm, mkCondDefault(fm, f), r);
-  }
   else if( n.getKind() == kind::NOT ){
     //just do directly
     doCheck( fm, f, d, n[0] );
@@ -649,6 +534,42 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
   else if( n.getKind() == kind::FORALL ){
     d.addEntry(fm, mkCondDefault(fm, f), Node::null());
   }
+  else if( n.getType().isArray() ){
+    //make the definition
+    Node r = fm->getRepresentative(n);
+    Trace("fmc-debug") << "Representative for array is " << r << std::endl;
+    while( r.getKind() == kind::STORE ){
+      Node i = fm->getUsedRepresentative( r[1] );
+      Node e = fm->getUsedRepresentative( r[2] );
+      d.addEntry(fm, mkArrayCond(i), e );
+      r = r[0];
+    }
+    Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));
+    bool success = false;
+    if( r.getKind() == kind::STORE_ALL ){
+      ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();
+      Node defaultValue = Node::fromExpr(storeAll.getExpr());
+      defaultValue = fm->getUsedRepresentative( defaultValue, true );
+      if( !defaultValue.isNull() ){
+        d.addEntry(fm, defC, defaultValue);
+        success = true;
+      }
+    }
+    if( !success ){
+      Trace("fmc-debug") << "Can't process base array " << r << std::endl;
+      //can't process this array
+      d.reset();
+      d.addEntry(fm, defC, Node::null());
+    }
+  }
+  else if( n.getNumChildren()==0 ){
+    Node r = n;
+    if( !fm->hasTerm(n) ){
+      r = getSomeDomainElement(fm, n.getType() );
+    }
+    r = fm->getUsedRepresentative( r);
+    d.addEntry(fm, mkCondDefault(fm, f), r);
+  }
   else{
     std::vector< int > var_ch;
     std::vector< Def > children;
@@ -665,6 +586,14 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;
       //uninterpreted compose
       doUninterpretedCompose( fm, f, d, n.getOperator(), children );
+    } else if( n.getKind()==SELECT ){
+      Trace("fmc-debug") << "Do select compose " << n << std::endl;
+      std::vector< Def > children2;
+      children2.push_back( children[1] );
+      std::vector< Node > cond;
+      mkCondDefaultVec(fm, f, cond);
+      std::vector< Node > val;
+      doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );
     } else {
       if( !var_ch.empty() ){
         if( n.getKind()==EQUAL ){
@@ -676,8 +605,8 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
             doVariableRelation( fm, f, d, var_ch[0]==0 ? children[1] : children[0], var_ch[0]==0 ? n[0] : n[1] );
           }
         }else{
-          std::cout << "Don't know how to check " << n << std::endl;
-          exit(0);
+          Trace("fmc-warn") << "Don't know how to check " << n << std::endl;
+          d.addEntry(fm, mkCondDefault(fm, f), Node::null());
         }
       }else{
         Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;
@@ -713,7 +642,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
     int k = getVariableId(f, eq[1]);
     TypeNode tn = eq[0].getType();
     if( !fm->d_rep_set.hasType( tn ) ){
-      fm->getSomeDomainElement( tn );  //to verify the type is initialized
+      getSomeDomainElement( fm, tn );  //to verify the type is initialized
     }
     for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {
       Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );
@@ -729,19 +658,23 @@ void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def
   int j = getVariableId(f, v);
   for (unsigned i=0; i<dc.d_cond.size(); i++) {
     Node val = dc.d_value[i];
-    if( dc.d_cond[i][j]!=val ){
-      if (fm->isStar(dc.d_cond[i][j])) {
-        std::vector<Node> cond;
-        mkCondVec(dc.d_cond[i],cond);
-        cond[j+1] = val;
-        d.addEntry(fm, mkCond(cond), d_true);
-        cond[j+1] = fm->getStar(val.getType());
-        d.addEntry(fm, mkCond(cond), d_false);
+    if( val.isNull() ){
+      d.addEntry( fm, dc.d_cond[i], val);
+    }else{
+      if( dc.d_cond[i][j]!=val ){
+        if (fm->isStar(dc.d_cond[i][j])) {
+          std::vector<Node> cond;
+          mkCondVec(dc.d_cond[i],cond);
+          cond[j+1] = val;
+          d.addEntry(fm, mkCond(cond), d_true);
+          cond[j+1] = fm->getStar(val.getType());
+          d.addEntry(fm, mkCond(cond), d_false);
+        }else{
+          d.addEntry( fm, dc.d_cond[i], d_false);
+        }
       }else{
-        d.addEntry( fm, dc.d_cond[i], d_false);
+        d.addEntry( fm, dc.d_cond[i], d_true);
       }
-    }else{
-      d.addEntry( fm, dc.d_cond[i], d_true);
     }
   }
 }
@@ -754,11 +687,11 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f,
   std::vector< Node > cond;
   mkCondDefaultVec(fm, f, cond);
   std::vector< Node > val;
-  doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);
+  doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);
 }
 
-void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,
-                                               std::vector< Def > & dc, int index,
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
+                                               Def & df, std::vector< Def > & dc, int index,
                                                std::vector< Node > & cond, std::vector<Node> & val ) {
   Trace("fmc-uf-process") << "process at " << index << std::endl;
   for( unsigned i=1; i<cond.size(); i++) {
@@ -769,11 +702,15 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f,
   if (index==(int)dc.size()) {
     //we have an entry, now do actual compose
     std::map< int, Node > entries;
-    doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et);
-    //add them to the definition
-    for( unsigned e=0; e<fm->d_models[op]->d_cond.size(); e++ ){
-      if ( entries.find(e)!=entries.end() ){
-        d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] );
+    doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et);
+    if( entries.empty() ){
+      d.addEntry(fm, mkCond(cond), Node::null());
+    }else{
+      //add them to the definition
+      for( unsigned e=0; e<df.d_cond.size(); e++ ){
+        if ( entries.find(e)!=entries.end() ){
+          d.addEntry(fm, entries[e], df.d_value[e] );
+        }
       }
     }
   }else{
@@ -784,7 +721,7 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f,
         if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){
           Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;
           val.push_back(dc[index].d_value[i]);
-          doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);
+          doUninterpretedCompose(fm, f, d, df, dc, index+1, new_cond, val);
           val.pop_back();
         }else{
           Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;
@@ -811,7 +748,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
   }else{
     Node v = val[index];
     bool bind_var = false;
-    if( v.getKind()==kind::BOUND_VARIABLE ){
+    if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){
       int j = getVariableId(f, v);
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;
       if (!fm->isStar(cond[j+1])) {
@@ -829,14 +766,16 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
       }
       cond[j+1] = fm->getStar(v.getType());
     }else{
-      if (curr.d_child.find(v)!=curr.d_child.end()) {
-        Trace("fmc-uf-process") << "follow value..." << std::endl;
-        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
-      }
-      Node st = fm->getStar(v.getType());
-      if (curr.d_child.find(st)!=curr.d_child.end()) {
-        Trace("fmc-uf-process") << "follow star..." << std::endl;
-        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
+      if( !v.isNull() ){
+        if (curr.d_child.find(v)!=curr.d_child.end()) {
+          Trace("fmc-uf-process") << "follow value..." << std::endl;
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);
+        }
+        Node st = fm->getStar(v.getType());
+        if (curr.d_child.find(st)!=curr.d_child.end()) {
+          Trace("fmc-uf-process") << "follow star..." << std::endl;
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);
+        }
       }
     }
   }
@@ -928,9 +867,28 @@ void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
   }
 }
 
+Node FullModelChecker::mkArrayCond( Node a ) {
+  if( d_array_term_cond.find(a)==d_array_term_cond.end() ){
+    if( d_array_cond.find(a.getType())==d_array_cond.end() ){
+      TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );
+      Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );
+      d_array_cond[a.getType()] = op;
+    }
+    std::vector< Node > cond;
+    cond.push_back(d_array_cond[a.getType()]);
+    cond.push_back(a);
+    d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond );
+  }
+  return d_array_term_cond[a];
+}
+
 Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {
   if( n.getKind()==EQUAL ){
-    return vals[0]==vals[1] ? d_true : d_false;
+    if (!vals[0].isNull() && !vals[1].isNull()) {
+      return vals[0]==vals[1] ? d_true : d_false;
+    }else{
+      return Node::null();
+    }
   }else if( n.getKind()==ITE ){
     if( vals[0]==d_true ){
       return vals[1];
@@ -969,6 +927,15 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals )
   }
 }
 
+Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {
+  bool addRepId = !fm->d_rep_set.hasType( tn );
+  Node de = fm->getSomeDomainElement(tn);
+  if( addRepId ){
+    d_rep_ids[tn][de] = 0;
+  }
+  return de;
+}
+
 Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {
   return fm->getFunctionValue(op, argPrefix);
 }
@@ -1003,6 +970,9 @@ void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node
     values.push_back(nv);
     entry_conds.push_back(en);
   }
+  else {
+    Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;
+  }
 }
 
 bool FullModelChecker::useSimpleModels() {
diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index ddf298006..c390c9437 100755
--- a/src/theory/quantifiers/full_model_check.h
+++ b/src/theory/quantifiers/full_model_check.h
@@ -71,35 +71,6 @@ public:
   void debugPrint(const char * tr, Node op, FullModelChecker * m);
 };
 
-class FirstOrderModelFmc : public FirstOrderModel
-{
-  friend class FullModelChecker;
-private:
-  /** quant engine */
-  QuantifiersEngine * d_qe;
-  /** models for UF */
-  std::map<Node, Def * > d_models;
-  std::map<TypeNode, Node > d_model_basis_rep;
-  std::map<TypeNode, Node > d_type_star;
-  Node getUsedRepresentative(Node n);
-  /** get current model value */
-  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );
-  void processInitializeModelForTerm(Node n);
-public:
-  FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);
-  FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }
-  // initialize the model
-  void processInitialize();
-
-  Node getFunctionValue(Node op, const char* argPrefix );
-
-  bool isStar(Node n);
-  Node getStar(TypeNode tn);
-  bool isModelBasisTerm(Node n);
-  Node getModelBasisTerm(TypeNode tn);
-  Node getSomeDomainElement(TypeNode tn);
-};
-
 
 class FullModelChecker : public QModelBuilder
 {
@@ -109,6 +80,8 @@ protected:
   std::map<TypeNode, std::map< Node, int > > d_rep_ids;
   std::map<Node, Def > d_quant_models;
   std::map<Node, Node > d_quant_cond;
+  std::map< TypeNode, Node > d_array_cond;
+  std::map< Node, Node > d_array_term_cond;
   std::map<Node, std::map< Node, int > > d_quant_var_id;
   std::map<Node, std::vector< int > > d_star_insts;
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);
@@ -126,8 +99,8 @@ private:
   void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);
   void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );
 
-  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,
-                               std::vector< Def > & dc, int index,
+  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,
+                               Def & df, std::vector< Def > & dc, int index,
                                std::vector< Node > & cond, std::vector<Node> & val );
   void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
                                 std::map< int, Node > & entries, int index,
@@ -143,7 +116,9 @@ private:
   Node mkCondDefault( FirstOrderModelFmc * fm, Node f );
   void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );
   void mkCondVec( Node n, std::vector< Node > & cond );
+  Node mkArrayCond( Node a );
   Node evaluateInterpreted( Node n, std::vector< Node > & vals );
+  Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );
 public:
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );
   ~FullModelChecker(){}
diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index fc8db420d..e703ee467 100644
--- a/src/theory/rep_set.h
+++ b/src/theory/rep_set.h
@@ -54,16 +54,15 @@ typedef std::vector< int > RepDomain;
 
 /** this class iterates over a RepSet */
 class RepSetIterator {
-private:
+public:
   enum {
     ENUM_DOMAIN_ELEMENTS,
     ENUM_RANGE,
   };
+private:
   QuantifiersEngine * d_qe;
   //initialize function
   bool initialize();
-  //enumeration type?
-  std::vector< int > d_enum_type;
   //for enum ranges
   std::map< int, Node > d_lower_bounds;
   //domain size
@@ -82,6 +81,8 @@ public:
 public:
   //pointer to model
   RepSet* d_rep_set;
+  //enumeration type?
+  std::vector< int > d_enum_type;
   //index we are considering
   std::vector< int > d_index;
   //types we are considering