Add get instantiations utilities to API.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f288c6c0acc4cacd639153f37877ae660f0ccc08..e3a0533afea80c43954dcfd86524f810abae492f 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -5125,6 +5125,43 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict)
   }
 }
 
+void SmtEngine::getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    std::vector< Node > qs_n;
+    d_theoryEngine->getInstantiatedQuantifiedFormulas( qs_n );
+    for( unsigned i=0; i<qs_n.size(); i++ ){
+      qs.push_back( qs_n[i].toExpr() );
+    }
+  }
+}
+
+void SmtEngine::getInstantiations( Expr q, std::vector< Expr >& insts ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    std::vector< Node > insts_n;
+    d_theoryEngine->getInstantiations( Node::fromExpr( q ), insts_n );
+    for( unsigned i=0; i<insts_n.size(); i++ ){
+      insts.push_back( insts_n[i].toExpr() );
+    }
+  }
+}
+
+void SmtEngine::getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs ) {
+  SmtScope smts(this);
+  if( d_theoryEngine ){
+    std::vector< std::vector< Node > > tvecs_n;
+    d_theoryEngine->getInstantiationTermVectors( Node::fromExpr( q ), tvecs_n );
+    for( unsigned i=0; i<tvecs_n.size(); i++ ){
+      std::vector< Expr > tvec;
+      for( unsigned j=0; j<tvecs_n[i].size(); j++ ){
+        tvec.push_back( tvecs_n[i][j].toExpr() );
+      }
+      tvecs.push_back( tvec );
+    }
+  }
+}
+
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {
   SmtScope smts(this);
   finalOptionsAreSet();

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 2741cea8527f1099c780058ed10d73b4b840ddac..760c7c07188aa1a68b7997f91dc86b901fe2af5a 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -565,6 +565,17 @@ public:
    */
   Expr doQuantifierElimination(const Expr& e, bool doFull, bool strict=true) throw(TypeCheckingException, ModalException, LogicException);
 
+  /**
+   * Get list of quantified formulas that were instantiated
+   */
+  void getInstantiatedQuantifiedFormulas( std::vector< Expr >& qs );
+   
+  /**
+   * Get instantiations
+   */
+  void getInstantiations( Expr q, std::vector< Expr >& insts );
+  void getInstantiationTermVectors( Expr q, std::vector< std::vector< Expr > >& tvecs );
+
   /**
    * Get an unsatisfiable core (only if immediately preceded by an
    * UNSAT or VALID query).  Only permitted if CVC4 was built with

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 67990ef69c93cced05e6b618a35230bf9281af3a..95b01bc7b03aef4f59145ce4e1a140d7cb5d7836 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1382,6 +1382,29 @@ bool QuantifiersEngine::getUnsatCoreLemmas( std::vector< Node >& active_lemmas,
   }
 }
 
+void QuantifiersEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
+  std::vector< Node > lemmas;
+  getInstantiations( q, lemmas );
+  std::map< Node, Node > quant;
+  std::map< Node, std::vector< Node > > tvec;
+  getExplanationForInstLemmas( lemmas, quant, tvec );
+  for( std::map< Node, std::vector< Node > >::iterator it = tvec.begin(); it != tvec.end(); ++it ){
+    tvecs.push_back( it->second );
+  }
+}
+
+void QuantifiersEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
+  if( options::incrementalSolving() ){
+    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+      getInstantiationTermVectors( it->first, insts[it->first] );
+    }
+  }else{
+    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
+      getInstantiationTermVectors( it->first, insts[it->first] );
+    }
+  }
+}
+
 void QuantifiersEngine::getExplanationForInstLemmas( std::vector< Node >& lems, std::map< Node, Node >& quant, std::map< Node, std::vector< Node > >& tvec ) {
   if( d_trackInstLemmas ){
     if( options::incrementalSolving() ){
@@ -1456,6 +1479,18 @@ void QuantifiersEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
+void QuantifiersEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
+  if( options::incrementalSolving() ){
+    for( std::map< Node, inst::CDInstMatchTrie* >::iterator it = d_c_inst_match_trie.begin(); it != d_c_inst_match_trie.end(); ++it ){
+      qs.push_back( it->first );
+    }
+  }else{
+    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
+      qs.push_back( it->first );
+    }
+  }
+}
+
 void QuantifiersEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
   bool useUnsatCore = false;
   std::vector< Node > active_lemmas;

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 232d1d889d6ed1fdafe0a02972e1067eebabf1b8..ff6a8a36cede380e9916863b1740c41abb83477d 100644 (file)
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -374,9 +374,14 @@ public:
   void printInstantiations( std::ostream& out );
   /** print solution for synthesis conjectures */
   void printSynthSolution( std::ostream& out );
+  /** get list of quantified formulas that were instantiated */
+  void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
   /** get instantiations */
   void getInstantiations( Node q, std::vector< Node >& insts );
   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+  /** get instantiation term vectors */
+  void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
+  void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
   /** get instantiated conjunction */
   Node getInstantiatedConjunction( Node q );
   /** get unsat core lemmas */

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index a14534efea3c162a01fe8a0ff5e27dcefcd727ae..c3e853ec05ffb3f2f3466f56d06ac5ed3cb8e820 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -1445,6 +1445,30 @@ void TheoryEngine::printSynthSolution( std::ostream& out ) {
   }
 }
 
+void TheoryEngine::getInstantiatedQuantifiedFormulas( std::vector< Node >& qs ) {
+  if( d_quantEngine ){
+    d_quantEngine->getInstantiatedQuantifiedFormulas( qs );
+  }else{
+    Assert( false );
+  }
+}
+
+void TheoryEngine::getInstantiations( Node q, std::vector< Node >& insts ) {
+  if( d_quantEngine ){
+    d_quantEngine->getInstantiations( q, insts );
+  }else{
+    Assert( false );
+  }
+}
+
+void TheoryEngine::getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs ) {
+  if( d_quantEngine ){
+    d_quantEngine->getInstantiationTermVectors( q, tvecs );
+  }else{
+    Assert( false );
+  }
+}
+
 void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& insts ) {
   if( d_quantEngine ){
     d_quantEngine->getInstantiations( insts );
@@ -1453,6 +1477,14 @@ void TheoryEngine::getInstantiations( std::map< Node, std::vector< Node > >& ins
   }
 }
 
+void TheoryEngine::getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts ) {
+  if( d_quantEngine ){
+    d_quantEngine->getInstantiationTermVectors( insts );
+  }else{
+    Assert( false );
+  }
+}
+
 Node TheoryEngine::getInstantiatedConjunction( Node q ) {
   if( d_quantEngine ){
     return d_quantEngine->getInstantiatedConjunction( q );

diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 4366f8d3a0196eab16f1e5b1ea9b1ba2bec62f0a..fc98c6e3a5209ad1c87764024c689ba145e422e8 100644 (file)
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -786,9 +786,20 @@ public:
   void printSynthSolution( std::ostream& out );
 
   /**
-   * Get instantiations
+   * Get list of quantified formulas that were instantiated
    */
+  void getInstantiatedQuantifiedFormulas( std::vector< Node >& qs );
+
+  /**
+   * Get instantiation methods
+   *   first inputs forall x.q[x] and returns ( q[a], ..., q[z] )
+   *   second inputs forall x.q[x] and returns ( a, ..., z ) 
+   *   third and fourth return mappings e.g. forall x.q1[x] -> ( q1[a]...q1[z] ) , ... , forall x.qn[x] -> ( qn[a]...qn[z] )
+   */
+  void getInstantiations( Node q, std::vector< Node >& insts );
+  void getInstantiationTermVectors( Node q, std::vector< std::vector< Node > >& tvecs );
   void getInstantiations( std::map< Node, std::vector< Node > >& insts );
+  void getInstantiationTermVectors( std::map< Node, std::vector< std::vector< Node > > >& insts );
   
   /**
    * Get instantiated conjunction, returns q[t1] ^ ... ^ q[tn] where t1...tn are current set of instantiations for q.