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

diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp
index e33cd2131b29235d75b1823593fd583cbdb36a71..e402a8969847c33d7d74223538e3c71da7944d24 100755 (executable)
--- 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 ) {
       }\r
     }\r
   }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) {\r
-    std::cout << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;\r
+    Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl;\r
     exit(0);\r
   }\r
 }\r
@@ -283,11 +283,13 @@ void BoundedIntegers::registerQuantifier( Node f ) {
           d_range[f][v] = new_range;\r
           r = new_range;\r
         }\r
-        if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){\r
-          Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl;\r
-          d_ranges.push_back( r );\r
-          d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );\r
-          d_rms[r]->initialize();\r
+        if( r.getKind()!=CONST_RATIONAL ){\r
+          if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){\r
+            Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl;\r
+            d_ranges.push_back( r );\r
+            d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext() );\r
+            d_rms[r]->initialize();\r
+          }\r
         }\r
       }\r
     }\r

diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp
index cf4381c02b6bb49802f398348cdf3c079a5879c5..4b101de491ecf9464a2ed5923b5ad9e3291a44c1 100644 (file)
--- 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 491e97097a52e03b4c51c0defd271dc952c50545..c2d82cc0a891bfaafd9c5138627c18488800a1bd 100644 (file)
--- 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 2513cb08e9e9b0e294f38a283ba7004228c0607f..b1611574921a28677528bf6b328a90f5efd06660 100755 (executable)
--- 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) {
 }\r
 \r
 \r
-\r
-FirstOrderModelFmc::FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name) :\r
-FirstOrderModel(c, name), d_qe(qe){\r
-\r
-}\r
-\r
-Node FirstOrderModelFmc::getUsedRepresentative(Node n) {\r
-  //Assert( fm->hasTerm(n) );\r
-  TypeNode tn = n.getType();\r
-  if( tn.isBoolean() ){\r
-    return areEqual(n, d_true) ? d_true : d_false;\r
-  }else{\r
-    Node r = getRepresentative(n);\r
-    if (r==d_model_basis_rep[tn]) {\r
-      r = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
-    }\r
-    return r;\r
-  }\r
-}\r
-\r
-Node FirstOrderModelFmc::getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial ) {\r
-  Trace("fmc-uf-model") << "Get model value for " << n << " " << n.getKind() << std::endl;\r
-  for(unsigned i=0; i<args.size(); i++) {\r
-    args[i] = getUsedRepresentative(args[i]);\r
-  }\r
-  Assert( n.getKind()==APPLY_UF );\r
-  return d_models[n.getOperator()]->evaluate(this, args);\r
-}\r
-\r
-void FirstOrderModelFmc::processInitialize() {\r
-  for( std::map<Node, Def * >::iterator it = d_models.begin(); it != d_models.end(); ++it ){\r
-    it->second->reset();\r
-  }\r
-  d_model_basis_rep.clear();\r
-}\r
-\r
-void FirstOrderModelFmc::processInitializeModelForTerm(Node n) {\r
-  if( n.getKind()==APPLY_UF ){\r
-    if( d_models.find(n.getOperator())==d_models.end()) {\r
-      d_models[n.getOperator()] = new Def;\r
-    }\r
-  }\r
-}\r
-\r
-Node FirstOrderModelFmc::getSomeDomainElement(TypeNode tn){\r
-  //check if there is even any domain elements at all\r
-  if (!d_rep_set.hasType(tn)) {\r
-    Trace("fmc-model-debug") << "Must create domain element for " << tn << "..." << std::endl;\r
-    Node mbt = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
-    d_rep_set.d_type_reps[tn].push_back(mbt);\r
-  }else if( d_rep_set.d_type_reps[tn].size()==0 ){\r
-    Message() << "empty reps" << std::endl;\r
-    exit(0);\r
-  }\r
-  return d_rep_set.d_type_reps[tn][0];\r
-}\r
-\r
-\r
-bool FirstOrderModelFmc::isStar(Node n) {\r
-  return n==getStar(n.getType());\r
-}\r
-\r
-Node FirstOrderModelFmc::getStar(TypeNode tn) {\r
-  if( d_type_star.find(tn)==d_type_star.end() ){\r
-    Node st = NodeManager::currentNM()->mkSkolem( "star_$$", tn, "skolem created for full-model checking" );\r
-    d_type_star[tn] = st;\r
-  }\r
-  return d_type_star[tn];\r
-}\r
-\r
-bool FirstOrderModelFmc::isModelBasisTerm(Node n) {\r
-  return n==getModelBasisTerm(n.getType());\r
-}\r
-\r
-Node FirstOrderModelFmc::getModelBasisTerm(TypeNode tn) {\r
-  return d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
-}\r
-\r
-Node FirstOrderModelFmc::getFunctionValue(Node op, const char* argPrefix ) {\r
-  TypeNode type = op.getType();\r
-  std::vector< Node > vars;\r
-  for( size_t i=0; i<type.getNumChildren()-1; i++ ){\r
-    std::stringstream ss;\r
-    ss << argPrefix << (i+1);\r
-    vars.push_back( NodeManager::currentNM()->mkBoundVar( ss.str(), type[i] ) );\r
-  }\r
-  Node boundVarList = NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars);\r
-  Node curr;\r
-  for( int i=(d_models[op]->d_cond.size()-1); i>=0; i--) {\r
-    Node v = getUsedRepresentative( d_models[op]->d_value[i] );\r
-    if( curr.isNull() ){\r
-      curr = v;\r
-    }else{\r
-      //make the condition\r
-      Node cond = d_models[op]->d_cond[i];\r
-      std::vector< Node > children;\r
-      for( unsigned j=0; j<cond.getNumChildren(); j++) {\r
-        if (!isStar(cond[j])){\r
-          Node c = getUsedRepresentative( cond[j] );\r
-          children.push_back( NodeManager::currentNM()->mkNode( EQUAL, vars[j], c ) );\r
-        }\r
-      }\r
-      Assert( !children.empty() );\r
-      Node cc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( AND, children );\r
-      curr = NodeManager::currentNM()->mkNode( ITE, cc, v, curr );\r
-    }\r
-  }\r
-  curr = Rewriter::rewrite( curr );\r
-  return NodeManager::currentNM()->mkNode(kind::LAMBDA, boundVarList, curr);\r
-}\r
-\r
-\r
-\r
 FullModelChecker::FullModelChecker(context::Context* c, QuantifiersEngine* qe) :\r
 QModelBuilder( c, qe ){\r
   d_true = NodeManager::currentNM()->mkConst(true);\r
@@ -369,6 +256,18 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         }\r
       }\r
     }\r
+    //also process non-rep set sorts\r
+    for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
+      Node op = it->first;\r
+      TypeNode tno = op.getType();\r
+      for( unsigned i=0; i<tno.getNumChildren(); i++) {\r
+        TypeNode tn = tno[i];\r
+        if( fm->d_model_basis_rep.find( tn )==fm->d_model_basis_rep.end() ){\r
+          Node mbn = d_qe->getTermDatabase()->getModelBasisTerm(tn);\r
+          fm->d_model_basis_rep[tn] = fm->getUsedRepresentative( mbn );\r
+        }\r
+      }\r
+    }\r
     //now, make models\r
     for( std::map<Node, Def * >::iterator it = fm->d_models.begin(); it != fm->d_models.end(); ++it ) {\r
       Node op = it->first;\r
@@ -397,7 +296,7 @@ void FullModelChecker::processBuildModel(TheoryModel* m, bool fullModel){
         Trace("fmc-model-debug") << "Add default " << nmb << std::endl;\r
         addEntry(fm, op, nmb, nmb, conds, values, entry_conds);\r
       }else{\r
-        Node vmb = fm->getSomeDomainElement(nmb.getType());\r
+        Node vmb = getSomeDomainElement(fm, nmb.getType());\r
         Trace("fmc-model-debug") << "Add default to default representative " << nmb << " ";\r
         Trace("fmc-model-debug") << fm->d_rep_set.d_type_reps[nmb.getType()].size() << std::endl;\r
         addEntry(fm, op, nmb, vmb, conds, values, entry_conds);\r
@@ -570,30 +469,24 @@ int FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Nod
   if( riter.setQuantifier( f ) ){\r
     std::vector< RepDomain > dom;\r
     for (unsigned i=0; i<c.getNumChildren(); i++) {\r
-      TypeNode tn = c[i].getType();\r
-      if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
-        //RepDomain rd;\r
-        if( fm->isStar(c[i]) ){\r
-          //add the full range\r
-          //for( std::map< Node, int >::iterator it = d_rep_ids[tn].begin();\r
-          //     it != d_rep_ids[tn].end(); ++it ){\r
-          //  rd.push_back(it->second);\r
-          //}\r
-        }else{\r
-          if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {\r
-            //rd.push_back(d_rep_ids[tn][c[i]]);\r
-            riter.d_domain[i].clear();\r
-            riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);\r
+      if (riter.d_enum_type[i]==RepSetIterator::ENUM_DOMAIN_ELEMENTS) {\r
+        TypeNode tn = c[i].getType();\r
+        if( d_rep_ids.find(tn)!=d_rep_ids.end() ){\r
+          if( fm->isStar(c[i]) ){\r
+            //add the full range\r
           }else{\r
-            return -1;\r
+            if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) {\r
+              riter.d_domain[i].clear();\r
+              riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]);\r
+            }else{\r
+              return -1;\r
+            }\r
           }\r
+        }else{\r
+          return -1;\r
         }\r
-        //dom.push_back(rd);\r
-      }else{\r
-        return -1;\r
       }\r
     }\r
-    //riter.setDomain(dom);\r
     //now do full iteration\r
     while( !riter.isFinished() ){\r
       Trace("fmc-exh-debug") << "Inst : ";\r
@@ -633,14 +526,6 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
     d.addEntry(fm, mkCondDefault(fm, f), n);\r
     Trace("fmc-debug") << "Done with " << n << " " << n.getKind() << std::endl;\r
   }\r
-  else if( n.getNumChildren()==0 ){\r
-    Node r = n;\r
-    if( !fm->hasTerm(n) ){\r
-      r = fm->getSomeDomainElement(n.getType() );\r
-    }\r
-    r = fm->getUsedRepresentative( r);\r
-    d.addEntry(fm, mkCondDefault(fm, f), r);\r
-  }\r
   else if( n.getKind() == kind::NOT ){\r
     //just do directly\r
     doCheck( fm, f, d, n[0] );\r
@@ -649,6 +534,42 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
   else if( n.getKind() == kind::FORALL ){\r
     d.addEntry(fm, mkCondDefault(fm, f), Node::null());\r
   }\r
+  else if( n.getType().isArray() ){\r
+    //make the definition\r
+    Node r = fm->getRepresentative(n);\r
+    Trace("fmc-debug") << "Representative for array is " << r << std::endl;\r
+    while( r.getKind() == kind::STORE ){\r
+      Node i = fm->getUsedRepresentative( r[1] );\r
+      Node e = fm->getUsedRepresentative( r[2] );\r
+      d.addEntry(fm, mkArrayCond(i), e );\r
+      r = r[0];\r
+    }\r
+    Node defC = mkArrayCond(fm->getStar(n.getType().getArrayIndexType()));\r
+    bool success = false;\r
+    if( r.getKind() == kind::STORE_ALL ){\r
+      ArrayStoreAll storeAll = r.getConst<ArrayStoreAll>();\r
+      Node defaultValue = Node::fromExpr(storeAll.getExpr());\r
+      defaultValue = fm->getUsedRepresentative( defaultValue, true );\r
+      if( !defaultValue.isNull() ){\r
+        d.addEntry(fm, defC, defaultValue);\r
+        success = true;\r
+      }\r
+    }\r
+    if( !success ){\r
+      Trace("fmc-debug") << "Can't process base array " << r << std::endl;\r
+      //can't process this array\r
+      d.reset();\r
+      d.addEntry(fm, defC, Node::null());\r
+    }\r
+  }\r
+  else if( n.getNumChildren()==0 ){\r
+    Node r = n;\r
+    if( !fm->hasTerm(n) ){\r
+      r = getSomeDomainElement(fm, n.getType() );\r
+    }\r
+    r = fm->getUsedRepresentative( r);\r
+    d.addEntry(fm, mkCondDefault(fm, f), r);\r
+  }\r
   else{\r
     std::vector< int > var_ch;\r
     std::vector< Def > children;\r
@@ -665,6 +586,14 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Trace("fmc-debug") << "Do uninterpreted compose " << n << std::endl;\r
       //uninterpreted compose\r
       doUninterpretedCompose( fm, f, d, n.getOperator(), children );\r
+    } else if( n.getKind()==SELECT ){\r
+      Trace("fmc-debug") << "Do select compose " << n << std::endl;\r
+      std::vector< Def > children2;\r
+      children2.push_back( children[1] );\r
+      std::vector< Node > cond;\r
+      mkCondDefaultVec(fm, f, cond);\r
+      std::vector< Node > val;\r
+      doUninterpretedCompose(fm, f, d, children[0], children2, 0, cond, val );\r
     } else {\r
       if( !var_ch.empty() ){\r
         if( n.getKind()==EQUAL ){\r
@@ -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] );\r
           }\r
         }else{\r
-          std::cout << "Don't know how to check " << n << std::endl;\r
-          exit(0);\r
+          Trace("fmc-warn") << "Don't know how to check " << n << std::endl;\r
+          d.addEntry(fm, mkCondDefault(fm, f), Node::null());\r
         }\r
       }else{\r
         Trace("fmc-debug") << "Do interpreted compose " << n << std::endl;\r
@@ -713,7 +642,7 @@ void FullModelChecker::doVariableEquality( FirstOrderModelFmc * fm, Node f, Def
     int k = getVariableId(f, eq[1]);\r
     TypeNode tn = eq[0].getType();\r
     if( !fm->d_rep_set.hasType( tn ) ){\r
-      fm->getSomeDomainElement( tn );  //to verify the type is initialized\r
+      getSomeDomainElement( fm, tn );  //to verify the type is initialized\r
     }\r
     for (unsigned i=0; i<fm->d_rep_set.d_type_reps[tn].size(); i++) {\r
       Node r = fm->getUsedRepresentative( fm->d_rep_set.d_type_reps[tn][i] );\r
@@ -729,19 +658,23 @@ void FullModelChecker::doVariableRelation( FirstOrderModelFmc * fm, Node f, Def
   int j = getVariableId(f, v);\r
   for (unsigned i=0; i<dc.d_cond.size(); i++) {\r
     Node val = dc.d_value[i];\r
-    if( dc.d_cond[i][j]!=val ){\r
-      if (fm->isStar(dc.d_cond[i][j])) {\r
-        std::vector<Node> cond;\r
-        mkCondVec(dc.d_cond[i],cond);\r
-        cond[j+1] = val;\r
-        d.addEntry(fm, mkCond(cond), d_true);\r
-        cond[j+1] = fm->getStar(val.getType());\r
-        d.addEntry(fm, mkCond(cond), d_false);\r
+    if( val.isNull() ){\r
+      d.addEntry( fm, dc.d_cond[i], val);\r
+    }else{\r
+      if( dc.d_cond[i][j]!=val ){\r
+        if (fm->isStar(dc.d_cond[i][j])) {\r
+          std::vector<Node> cond;\r
+          mkCondVec(dc.d_cond[i],cond);\r
+          cond[j+1] = val;\r
+          d.addEntry(fm, mkCond(cond), d_true);\r
+          cond[j+1] = fm->getStar(val.getType());\r
+          d.addEntry(fm, mkCond(cond), d_false);\r
+        }else{\r
+          d.addEntry( fm, dc.d_cond[i], d_false);\r
+        }\r
       }else{\r
-        d.addEntry( fm, dc.d_cond[i], d_false);\r
+        d.addEntry( fm, dc.d_cond[i], d_true);\r
       }\r
-    }else{\r
-      d.addEntry( fm, dc.d_cond[i], d_true);\r
     }\r
   }\r
 }\r
@@ -754,11 +687,11 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f,
   std::vector< Node > cond;\r
   mkCondDefaultVec(fm, f, cond);\r
   std::vector< Node > val;\r
-  doUninterpretedCompose( fm, f, op, d, dc, 0, cond, val);\r
+  doUninterpretedCompose( fm, f, d, *fm->d_models[op], dc, 0, cond, val);\r
 }\r
 \r
-void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,\r
-                                               std::vector< Def > & dc, int index,\r
+void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,\r
+                                               Def & df, std::vector< Def > & dc, int index,\r
                                                std::vector< Node > & cond, std::vector<Node> & val ) {\r
   Trace("fmc-uf-process") << "process at " << index << std::endl;\r
   for( unsigned i=1; i<cond.size(); i++) {\r
@@ -769,11 +702,15 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f,
   if (index==(int)dc.size()) {\r
     //we have an entry, now do actual compose\r
     std::map< int, Node > entries;\r
-    doUninterpretedCompose2( fm, f, entries, 0, cond, val, fm->d_models[op]->d_et);\r
-    //add them to the definition\r
-    for( unsigned e=0; e<fm->d_models[op]->d_cond.size(); e++ ){\r
-      if ( entries.find(e)!=entries.end() ){\r
-        d.addEntry(fm, entries[e], fm->d_models[op]->d_value[e] );\r
+    doUninterpretedCompose2( fm, f, entries, 0, cond, val, df.d_et);\r
+    if( entries.empty() ){\r
+      d.addEntry(fm, mkCond(cond), Node::null());\r
+    }else{\r
+      //add them to the definition\r
+      for( unsigned e=0; e<df.d_cond.size(); e++ ){\r
+        if ( entries.find(e)!=entries.end() ){\r
+          d.addEntry(fm, entries[e], df.d_value[e] );\r
+        }\r
       }\r
     }\r
   }else{\r
@@ -784,7 +721,7 @@ void FullModelChecker::doUninterpretedCompose( FirstOrderModelFmc * fm, Node f,
         if( doMeet(fm, new_cond, dc[index].d_cond[i]) ){\r
           Trace("fmc-uf-process") << "index " << i << " succeeded meet." << std::endl;\r
           val.push_back(dc[index].d_value[i]);\r
-          doUninterpretedCompose(fm, f, op, d, dc, index+1, new_cond, val);\r
+          doUninterpretedCompose(fm, f, d, df, dc, index+1, new_cond, val);\r
           val.pop_back();\r
         }else{\r
           Trace("fmc-uf-process") << "index " << i << " failed meet." << std::endl;\r
@@ -811,7 +748,7 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
   }else{\r
     Node v = val[index];\r
     bool bind_var = false;\r
-    if( v.getKind()==kind::BOUND_VARIABLE ){\r
+    if( !v.isNull() && v.getKind()==kind::BOUND_VARIABLE ){\r
       int j = getVariableId(f, v);\r
       Trace("fmc-uf-process") << v << " is variable #" << j << std::endl;\r
       if (!fm->isStar(cond[j+1])) {\r
@@ -829,14 +766,16 @@ void FullModelChecker::doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,
       }\r
       cond[j+1] = fm->getStar(v.getType());\r
     }else{\r
-      if (curr.d_child.find(v)!=curr.d_child.end()) {\r
-        Trace("fmc-uf-process") << "follow value..." << std::endl;\r
-        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
-      }\r
-      Node st = fm->getStar(v.getType());\r
-      if (curr.d_child.find(st)!=curr.d_child.end()) {\r
-        Trace("fmc-uf-process") << "follow star..." << std::endl;\r
-        doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
+      if( !v.isNull() ){\r
+        if (curr.d_child.find(v)!=curr.d_child.end()) {\r
+          Trace("fmc-uf-process") << "follow value..." << std::endl;\r
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[v]);\r
+        }\r
+        Node st = fm->getStar(v.getType());\r
+        if (curr.d_child.find(st)!=curr.d_child.end()) {\r
+          Trace("fmc-uf-process") << "follow star..." << std::endl;\r
+          doUninterpretedCompose2(fm, f, entries, index+1, cond, val, curr.d_child[st]);\r
+        }\r
       }\r
     }\r
   }\r
@@ -928,9 +867,28 @@ void FullModelChecker::mkCondVec( Node n, std::vector< Node > & cond ) {
   }\r
 }\r
 \r
+Node FullModelChecker::mkArrayCond( Node a ) {\r
+  if( d_array_term_cond.find(a)==d_array_term_cond.end() ){\r
+    if( d_array_cond.find(a.getType())==d_array_cond.end() ){\r
+      TypeNode typ = NodeManager::currentNM()->mkFunctionType( a.getType(), NodeManager::currentNM()->booleanType() );\r
+      Node op = NodeManager::currentNM()->mkSkolem( "fmc_$$", typ, "op created for full-model checking" );\r
+      d_array_cond[a.getType()] = op;\r
+    }\r
+    std::vector< Node > cond;\r
+    cond.push_back(d_array_cond[a.getType()]);\r
+    cond.push_back(a);\r
+    d_array_term_cond[a] = NodeManager::currentNM()->mkNode(APPLY_UF, cond );\r
+  }\r
+  return d_array_term_cond[a];\r
+}\r
+\r
 Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals ) {\r
   if( n.getKind()==EQUAL ){\r
-    return vals[0]==vals[1] ? d_true : d_false;\r
+    if (!vals[0].isNull() && !vals[1].isNull()) {\r
+      return vals[0]==vals[1] ? d_true : d_false;\r
+    }else{\r
+      return Node::null();\r
+    }\r
   }else if( n.getKind()==ITE ){\r
     if( vals[0]==d_true ){\r
       return vals[1];\r
@@ -969,6 +927,15 @@ Node FullModelChecker::evaluateInterpreted( Node n, std::vector< Node > & vals )
   }\r
 }\r
 \r
+Node FullModelChecker::getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn ) {\r
+  bool addRepId = !fm->d_rep_set.hasType( tn );\r
+  Node de = fm->getSomeDomainElement(tn);\r
+  if( addRepId ){\r
+    d_rep_ids[tn][de] = 0;\r
+  }\r
+  return de;\r
+}\r
+\r
 Node FullModelChecker::getFunctionValue(FirstOrderModelFmc * fm, Node op, const char* argPrefix ) {\r
   return fm->getFunctionValue(op, argPrefix);\r
 }\r
@@ -1003,6 +970,9 @@ void FullModelChecker::addEntry( FirstOrderModelFmc * fm, Node op, Node c, Node
     values.push_back(nv);\r
     entry_conds.push_back(en);\r
   }\r
+  else {\r
+    Trace("fmc-model-debug") << "Already have entry for : " << n << " -> " << nv << " (entry is " << en << ")" << std::endl;\r
+  }\r
 }\r
 \r
 bool FullModelChecker::useSimpleModels() {\r

diff --git a/src/theory/quantifiers/full_model_check.h b/src/theory/quantifiers/full_model_check.h
index ddf29800627e0424a1d0fa623df85040a1e6b9fc..c390c943776ee7e0ccdc545a441ffcc5e6901d3c 100755 (executable)
--- 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);\r
 };\r
 \r
-class FirstOrderModelFmc : public FirstOrderModel\r
-{\r
-  friend class FullModelChecker;\r
-private:\r
-  /** quant engine */\r
-  QuantifiersEngine * d_qe;\r
-  /** models for UF */\r
-  std::map<Node, Def * > d_models;\r
-  std::map<TypeNode, Node > d_model_basis_rep;\r
-  std::map<TypeNode, Node > d_type_star;\r
-  Node getUsedRepresentative(Node n);\r
-  /** get current model value */\r
-  Node getCurrentUfModelValue( Node n, std::vector< Node > & args, bool partial );\r
-  void processInitializeModelForTerm(Node n);\r
-public:\r
-  FirstOrderModelFmc(QuantifiersEngine * qe, context::Context* c, std::string name);\r
-  FirstOrderModelFmc * asFirstOrderModelFmc() { return this; }\r
-  // initialize the model\r
-  void processInitialize();\r
-\r
-  Node getFunctionValue(Node op, const char* argPrefix );\r
-\r
-  bool isStar(Node n);\r
-  Node getStar(TypeNode tn);\r
-  bool isModelBasisTerm(Node n);\r
-  Node getModelBasisTerm(TypeNode tn);\r
-  Node getSomeDomainElement(TypeNode tn);\r
-};\r
-\r
 \r
 class FullModelChecker : public QModelBuilder\r
 {\r
@@ -109,6 +80,8 @@ protected:
   std::map<TypeNode, std::map< Node, int > > d_rep_ids;\r
   std::map<Node, Def > d_quant_models;\r
   std::map<Node, Node > d_quant_cond;\r
+  std::map< TypeNode, Node > d_array_cond;\r
+  std::map< Node, Node > d_array_term_cond;\r
   std::map<Node, std::map< Node, int > > d_quant_var_id;\r
   std::map<Node, std::vector< int > > d_star_insts;\r
   Node normalizeArgReps(FirstOrderModelFmc * fm, Node op, Node n);\r
@@ -126,8 +99,8 @@ private:
   void doVariableRelation( FirstOrderModelFmc * fm, Node f, Def & d, Def & dc, Node v);\r
   void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d, Node n, std::vector< Def > & dc );\r
 \r
-  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Node op, Def & d,\r
-                               std::vector< Def > & dc, int index,\r
+  void doUninterpretedCompose( FirstOrderModelFmc * fm, Node f, Def & d,\r
+                               Def & df, std::vector< Def > & dc, int index,\r
                                std::vector< Node > & cond, std::vector<Node> & val );\r
   void doUninterpretedCompose2( FirstOrderModelFmc * fm, Node f,\r
                                 std::map< int, Node > & entries, int index,\r
@@ -143,7 +116,9 @@ private:
   Node mkCondDefault( FirstOrderModelFmc * fm, Node f );\r
   void mkCondDefaultVec( FirstOrderModelFmc * fm, Node f, std::vector< Node > & cond );\r
   void mkCondVec( Node n, std::vector< Node > & cond );\r
+  Node mkArrayCond( Node a );\r
   Node evaluateInterpreted( Node n, std::vector< Node > & vals );\r
+  Node getSomeDomainElement( FirstOrderModelFmc * fm, TypeNode tn );\r
 public:\r
   FullModelChecker( context::Context* c, QuantifiersEngine* qe );\r
   ~FullModelChecker(){}\r

diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h
index fc8db420dea2638d4ce85e870722c168f080616d..e703ee46776713c6cc4278f055e531032bf9df24 100644 (file)
--- 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