first working version of new inst-gen-style quantifier instantiation technique for...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index fa619c653ed53a01bc1791bcf37f188cd5f2b541..3813f964d08d925004f6caee9114213053ce3cd9 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1154,8 +1154,6 @@ Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vect
         }else{
           TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, n[0][i].getType() );
           Node op = NodeManager::currentNM()->mkSkolem( "skop_$$", typ, "op created during pre-skolemization" );
-          NoMatchAttribute nma;
-          op.setAttribute(nma,true);
           std::vector< Node > funcArgs;
           funcArgs.push_back( op );
           funcArgs.insert( funcArgs.end(), fvs.begin(), fvs.end() );

diff --git a/src/theory/quantifiers/inst_gen.cpp b/src/theory/quantifiers/inst_gen.cpp
index ea58840f5ad0ff476c688aa219498b3fce69494a..099e3aa294f8913cfd1a1e62886f905e626eb6bd 100755 (executable)
--- a/src/theory/quantifiers/inst_gen.cpp
+++ b/src/theory/quantifiers/inst_gen.cpp
@@ -45,10 +45,11 @@ InstGenProcess::InstGenProcess( Node n ) : d_node( n ){
 \r
 void InstGenProcess::addMatchValue( QuantifiersEngine* qe, Node f, Node val, InstMatch& m ){\r
   if( !qe->existsInstantiation( f, m, true ) ){\r
-    //if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){\r
+    //make sure no duplicates are produced\r
+    if( d_inst_trie[val].addInstMatch( qe, f, m, true ) ){\r
       d_match_values.push_back( val );\r
       d_matches.push_back( InstMatch( &m ) );\r
-    //}\r
+    }\r
   }\r
 }\r
 \r
@@ -110,6 +111,8 @@ void InstGenProcess::calculateMatches( QuantifiersEngine* qe, Node f ){
     calculateMatchesInterpreted( qe, f, curr, terms, 0 );\r
   }\r
   Trace("cm") << "done calculate matches" << std::endl;\r
+  //can clear information used for finding duplicates\r
+  d_inst_trie.clear();\r
 }\r
 \r
 bool InstGenProcess::getMatch( EqualityQuery* q, int i, InstMatch& m ){\r

diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp
index 3d1ca8f0daeceea744491505906c7250f1f1c115..e0ab047ab3d8c521097c1e14cc7b1a8bfe90845c 100644 (file)
--- a/src/theory/quantifiers/model_builder.cpp
+++ b/src/theory/quantifiers/model_builder.cpp
@@ -538,7 +538,12 @@ void ModelEngineBuilderInstGen::analyzeQuantifier( FirstOrderModel* fm, Node f )
   //determine selection formula, set terms in selection formula as being selected
   Node s = getSelectionFormula( d_qe->getTermDatabase()->getInstConstantBody( f ),
                                 d_qe->getTermDatabase()->getModelBasisBody( f ), true, 0 );
-  Trace("sel-form") << "Selection formula for " << f << " is " << s << std::endl;
+  //if( !s.isNull() ){
+  //  s = Rewriter::rewrite( s );
+  //}
+  d_qe->getTermDatabase()->setInstantiationConstantAttr( s, f );
+  Trace("sel-form") << "Selection formula " << f << std::endl;
+  Trace("sel-form") << "                  " << s << std::endl;
   if( !s.isNull() ){
     d_quant_selection_formula[f] = s;
     Node gs = d_qe->getTermDatabase()->getModelBasis( f, s );
@@ -566,7 +571,7 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
       //get all possible values of selection formula
       InstGenProcess igp( d_quant_selection_formula[f] );
       igp.calculateMatches( d_qe, f );
-      Trace("inst-gen-debug") << "Add inst-gen instantiations..." << std::endl;
+      Trace("inst-gen-debug") << "Add inst-gen instantiations (" << igp.getNumMatches() << ")..." << std::endl;
       for( int i=0; i<igp.getNumMatches(); i++ ){
         //if the match is not already true in the model
         if( igp.getMatchValue( i )!=fm->d_true ){
@@ -576,13 +581,13 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
           //  matches that are empty should trigger other instances that are non-empty
           if( !m.empty() ){
             bool addInst = false;
+            Trace("inst-gen-debug") << "Get in terms of parent..." << std::endl;
             //translate to be in terms match in terms of fp
             InstMatch mp;
             getParentQuantifierMatch( mp, fp, m, f );
 
             //if this is a partial instantion
             if( !m.isComplete( f ) ){
-              Trace("inst-gen-debug") << "- partial inst" << std::endl;
               //if the instantiation does not yet exist
               if( d_sub_quant_inst_trie[fp].addInstMatch( d_qe, fp, mp, true ) ){
                 //get the partial instantiation pf
@@ -599,7 +604,6 @@ int ModelEngineBuilderInstGen::doInstGen( FirstOrderModel* fm, Node f ){
               addInst = true;
             }
             if( addInst ){
-              Trace("inst-gen-debug") << "- complete inst" << std::endl;
               //otherwise, get instantiation and add ground instantiation in terms of root parent
               if( d_qe->addInstantiation( fp, mp ) ){
                 addedLemmas++;
@@ -631,43 +635,48 @@ bool ModelEngineBuilderInstGen::shouldSetDefaultValue( Node n ){
   return d_term_selected.find( n )!=d_term_selected.end();
 }
 
-//if possible, returns a formula n' such that ( n' <=> polarity ) => ( n <=> polarity ), and ( n' <=> polarity ) is true in the current context,
+//if possible, returns a formula n' such that n' => ( n <=> polarity ), and n' is true in the current context,
 //   and NULL otherwise
 Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polarity, int useOption ){
+  Trace("sel-form-debug") << "Looking for selection formula " << n << " " << polarity << std::endl;
+  Node ret;
   if( n.getKind()==NOT ){
-    Node nn = getSelectionFormula( fn[0], n[0], !polarity, useOption );
-    if( !nn.isNull() ){
-      return nn.negate();
-    }
+    ret = getSelectionFormula( fn[0], n[0], !polarity, useOption );
   }else if( n.getKind()==OR || n.getKind()==IMPLIES || n.getKind()==AND ){
     //whether we only need to find one or all
     bool posPol = (( n.getKind()==OR || n.getKind()==IMPLIES ) && polarity ) || ( n.getKind()==AND && !polarity );
     std::vector< Node > children;
+    bool retSet = false;
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
       Node fnc = ( i==0 && fn.getKind()==IMPLIES ) ? fn[i].negate() : fn[i];
       Node nc = ( i==0 && n.getKind()==IMPLIES ) ? n[i].negate() : n[i];
       Node nn = getSelectionFormula( fnc, nc, polarity, useOption );
       if( nn.isNull()!=posPol ){   //TODO: may want to weaken selection formula
-        return nn;
+        ret = nn;
+        retSet = true;
+        break;
+      }
+      if( std::find( children.begin(), children.end(), nn )==children.end() ){
+        children.push_back( nn );
       }
-      children.push_back( nn );
     }
-    if( !posPol ){
-      return NodeManager::currentNM()->mkNode( n.getKind()==AND ? AND : OR, children );
+    if( !retSet && !posPol ){
+      ret = NodeManager::currentNM()->mkNode( AND, children );
     }
   }else if( n.getKind()==ITE ){
     Node nn;
     Node nc[2];
     //get selection formula for the
     for( int i=0; i<2; i++ ){
-      nn = getSelectionFormula( i==0 ? fn[0] : fn[0].negate(), i==0 ? n[0] : n[0].negate(), true, useOption );
+      nn = getSelectionFormula( fn[0], n[0], i==0, useOption );
       nc[i] = getSelectionFormula( fn[i+1], n[i+1], polarity, useOption );
       if( !nn.isNull() && !nc[i].isNull() ){
-        return NodeManager::currentNM()->mkNode( AND, nn, nc[i] );
+        ret = NodeManager::currentNM()->mkNode( AND, nn, nc[i] );
+        break;
       }
     }
-    if( !nc[0].isNull() && !nc[1].isNull() ){
-      return NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] );
+    if( ret.isNull() && !nc[0].isNull() && !nc[1].isNull() ){
+      ret = NodeManager::currentNM()->mkNode( AND, nc[0], nc[1] );
     }
   }else if( n.getKind()==IFF || n.getKind()==XOR ){
     bool opPol = polarity ? n.getKind()==XOR : n.getKind()==IFF;
@@ -675,13 +684,13 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar
       Node nn[2];
       for( int i=0; i<2; i++ ){
         bool pol = i==0 ? p==0 : ( opPol ? p!=0 : p==0 );
-        nn[i] = getSelectionFormula( pol ? fn[i] : fn[i].negate(), pol ? n[i] : n[i].negate(), true, useOption );
+        nn[i] = getSelectionFormula( fn[i], n[i], pol, useOption );
         if( nn[i].isNull() ){
           break;
         }
       }
       if( !nn[0].isNull() && !nn[1].isNull() ){
-        return NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] );
+        ret = NodeManager::currentNM()->mkNode( AND, nn[0], nn[1] );
       }
     }
   }else{
@@ -691,12 +700,16 @@ Node ModelEngineBuilderInstGen::getSelectionFormula( Node fn, Node n, bool polar
       bool value;
       if( d_qe->getValuation().hasSatValue( n, value ) ){
         if( value==polarity ){
-          return fn;
+          ret = fn;
+          if( !polarity ){
+            ret = ret.negate();
+          }
         }
       }
     }
   }
-  return Node::null();
+  Trace("sel-form-debug") << "   return " << ret << std::endl;
+  return ret;
 }
 
 void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
@@ -707,7 +720,7 @@ void ModelEngineBuilderInstGen::setSelectedTerms( Node s ){
     if( !s.hasAttribute(ModelBasisArgAttribute()) ) std::cout << "no mba!! " << s << std::endl;
     if( s.getAttribute(ModelBasisArgAttribute())==1 ){
       d_term_selected[ s ] = true;
-      Trace("sel-form") << "  " << s << " is a selected term." << std::endl;
+      Trace("sel-form-term") << "  " << s << " is a selected term." << std::endl;
     }
   }
   for( int i=0; i<(int)s.getNumChildren(); i++ ){
@@ -744,18 +757,26 @@ Node ModelEngineBuilderInstGen::getParentQuantifier( Node f ){
 }
 
 void ModelEngineBuilderInstGen::getParentQuantifierMatch( InstMatch& mp, Node fp, InstMatch& m, Node f ){
-  int counter = 0;
-  for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
-    Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i );
-    if( fp[0][i]==f[0][counter] ){
-      Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter );
-      Node n = m.getValue( ic );
-      if( !n.isNull() ){
-        mp.setMatch( d_qe->getEqualityQuery(), icp, n );
+  if( f!=fp ){
+    //std::cout << "gpqm " << fp << " " << f << " " << m << std::endl;
+    //std::cout << "     " << fp[0].getNumChildren() << " " << f[0].getNumChildren() << std::endl;
+    int counter = 0;
+    for( size_t i=0; i<fp[0].getNumChildren(); i++ ){
+      Node icp = d_qe->getTermDatabase()->getInstantiationConstant( fp, i );
+      if( counter<f[0].getNumChildren() ){
+        if( fp[0][i]==f[0][counter] ){
+          Node ic = d_qe->getTermDatabase()->getInstantiationConstant( f, counter );
+          Node n = m.getValue( ic );
+          if( !n.isNull() ){
+            mp.setMatch( d_qe->getEqualityQuery(), icp, n );
+          }
+          counter++;
+        }
       }
-      counter++;
     }
+    mp.add( d_sub_quant_inst[f] );
+  }else{
+    mp.add( m );
   }
-  mp.add( d_sub_quant_inst[f] );
 }
 

diff --git a/src/theory/quantifiers/options_handlers.h b/src/theory/quantifiers/options_handlers.h
index ba5c5c88421e759ebe3cb404a4f25845562c446c..312261d3cb63b63a6613224c478329229b69598b 100644 (file)
--- a/src/theory/quantifiers/options_handlers.h
+++ b/src/theory/quantifiers/options_handlers.h
@@ -57,7 +57,7 @@ predicate\n\
 ";
 
 static const std::string axiomInstModeHelp = "\
-Literal match modes currently supported by the --axiom-inst option:\n\
+Axiom instantiation modes currently supported by the --axiom-inst option:\n\
 \n\
 default \n\
 + Treat axioms the same as usual quantifiers, i.e. use all available methods for\n\

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index c8c88497427c71647ad1fbd91e8d240e1bdec630..3b27780618ba945a43d9ab37d62cd24795fabda5 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -216,7 +216,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){
 Node TermDb::getModelBasisTerm( TypeNode tn, int i ){
   if( d_model_basis_term.find( tn )==d_model_basis_term.end() ){
     Node mbt;
-    if( d_type_map[ tn ].empty() || options::fmfNewInstGen() ){
+    if( d_type_map[ tn ].empty() ){
       std::stringstream ss;
       ss << Expr::setlanguage(options::outputLanguage());
       ss << "e_" << tn;

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index d63eebf7e9d52262c2069a8776898bdb9a7d7933..bcd6b833d18719989d568acddcafc77f8af1b038 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -144,8 +144,6 @@ private:
   std::map< Node, Node > d_inst_constants_map;
   /** make instantiation constants for */
   void makeInstantiationConstantsFor( Node f );
-  /** set instantiation constant attr */
-  void setInstantiationConstantAttr( Node n, Node f );
 public:
   /** get the i^th instantiation constant of f */
   Node getInstantiationConstant( Node f, int i ) { return d_inst_constants[f][i]; }
@@ -174,6 +172,8 @@ public:
   Node getInstConstantIffTerm( Node n, bool pol );
   /** make node, validating the inst constant attribute */
   Node mkNodeInstConstant( Kind k, std::vector< Node >& children, Node f );
+  /** set instantiation constant attr */
+  void setInstantiationConstantAttr( Node n, Node f );
 
 //for skolem
 private:

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 9d7c8e315caf6ade1fbbd4d20b26605c1f368245..4ba5c39e60cadfab29c2651b674fc244e5451561 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -97,17 +97,17 @@ void QuantifiersEngine::check( Theory::Effort e ){
 
   d_hasAddedLemma = false;
   if( e==Theory::EFFORT_LAST_CALL ){
+    //if effort is last call, try to minimize model first
+    if( options::finiteModelFind() ){
+      //first, check if we can minimize the model further
+      if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
+        return;
+      }
+    }
     ++(d_statistics.d_instantiation_rounds_lc);
   }else if( e==Theory::EFFORT_FULL ){
     ++(d_statistics.d_instantiation_rounds);
   }
-  //if effort is last call, try to minimize model first
-  if( e==Theory::EFFORT_LAST_CALL && options::finiteModelFind() ){
-    //first, check if we can minimize the model further
-    if( !((uf::TheoryUF*)getTheoryEngine()->theoryOf( THEORY_UF ))->getStrongSolver()->minimize() ){
-      return;
-    }
-  }
   for( int i=0; i<(int)d_modules.size(); i++ ){
     d_modules[i]->check( e );
   }