Finish --dump-instantiations option. Update scripts.

diff --git a/contrib/run-script-cascj7-fof b/contrib/run-script-cascj7-fof
index 582a14952eb16c9841ca361a3887ab3c73acb358..be656b57a2953d61934ac84c9cd9008ce9f55ced 100755 (executable)
--- a/contrib/run-script-cascj7-fof
+++ b/contrib/run-script-cascj7-fof
@@ -15,7 +15,7 @@ echo "------- cvc4-fof $bench at $2..."
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,11 +25,11 @@ function trywith {
 }
 function finishwith {
   echo "--- Run $@ at $limit...";
-  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+  $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench
 }
 
+trywith 15 --quant-cf --pre-skolem-quant --full-saturate-quant
 trywith 30 --full-saturate-quant
-trywith 15 --decision=internal --full-saturate-quant
 trywith 30 --finite-model-find --fmf-inst-engine --mbqi=gen-ev
 trywith 30 --relevant-triggers --full-saturate-quant
 trywith 15 --finite-model-find --decision=justification-stoponly

diff --git a/contrib/run-script-cascj7-tff b/contrib/run-script-cascj7-tff
index 8033bed1fe3d1a6ce37c0465a167b40ab1e0aa68..4506e511d9b2707ce12dae61b385b0362f8b0ea1 100755 (executable)
--- a/contrib/run-script-cascj7-tff
+++ b/contrib/run-script-cascj7-tff
@@ -9,13 +9,13 @@ filename=${file%.*}
 echo "------- cvc4-tff $bench at $2..."
 
 # use: trywith [params..]
-# to attempt a run.  Only thing printed on stdout is "sat" or "unsat", in
-# which case this run script terminates immediately.  Otherwise, this
+# to attempt a run.  If an SZS ontology result is printed, then
+# the run script terminates immediately.  Otherwise, this
 # function returns normally.
 function trywith {
   limit=$1; shift;
   echo "--- Run $@ at $limit...";
-  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench) 2>/dev/null |
+  (ulimit -t "$limit";$cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench) 2>/dev/null |
   (read w1 w2 w3 result w4 w5;
   case "$result" in
   Unsatisfiable) echo "$w1 $w2 $w3 $result $w4 $w5";cat;exit 0;;
@@ -25,7 +25,7 @@ function trywith {
 }
 function finishwith {
   echo "--- Run $@ at $limit...";
-  $cvc4 --no-checking --no-interactive --dump-instantiations "$@" $bench
+  $cvc4 --no-checking --no-interactive --dump-instantiations --inst-format=szs "$@" $bench
 }
 
 trywith 15 --cbqi-recurse --full-saturate-quant

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4deb43f4257b23f5943f9b98df78171f1734381f..c6b76e8507c68c77294acab32cae5bc11b66de73 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -3801,15 +3801,16 @@ Proof* SmtEngine::getProof() throw(ModalException) {
 }
 
 void SmtEngine::printInstantiations( std::ostream& out ) {
-  //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
-  out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl;
-  //}
+  SmtScope smts(this);
+  if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
+    out << "% SZS CNF output start CNFRefutation for " << d_filename.c_str() << std::endl;
+  }
   if( d_theoryEngine ){
     d_theoryEngine->printInstantiations( out );
   }
-  //if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
-  out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl;
-  //}
+  if( options::instFormatMode()==INST_FORMAT_MODE_SZS ){
+    out << "% SZS CNF output end CNFRefutation for " << d_filename.c_str() << std::endl;
+  }
 }
 
 vector<Expr> SmtEngine::getAssertions() throw(ModalException) {

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index 703a44d03fa9370631c0519b8303790ac45b1a7e..29219016803d24a45f2dfbb894db87944c50b793 100644 (file)
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -27,7 +27,7 @@ namespace CVC4 {
 namespace theory {
 namespace inst {
 
-InstMatch::InstMatch( Node f ) {
+InstMatch::InstMatch( TNode f ) {
   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
     d_vals.push_back( Node::null() );
   }
@@ -198,12 +198,12 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
   }
 }
 
-void InstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const {
+void InstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const {
   if( terms.size()==q[0].getNumChildren() ){
     out << "  ( ";
     for( unsigned i=0; i<terms.size(); i++ ){
-      if( i>0 ) out << ", ";
-      //out << terms[i];
+      if( i>0 ){ out << ", ";}
+      out << terms[i];
     }
     out << " )" << std::endl;
   }else{
@@ -282,13 +282,13 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
   }
 }
 
-void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< Node >& terms ) const{
+void CDInstMatchTrie::print( std::ostream& out, Node q, std::vector< TNode >& terms ) const{
   if( d_valid.get() ){
     if( terms.size()==q[0].getNumChildren() ){
       out << "  ( ";
       for( unsigned i=0; i<terms.size(); i++ ){
         if( i>0 ) out << ", ";
-        //out << terms[i];
+        out << terms[i];
       }
       out << " )" << std::endl;
     }else{

diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index accd3baeddeac13c138c67297135b5797e2a55b9..d728d18a2696fa02b6ad3a20bf2e0f9d8beb3e17 100644 (file)
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -41,7 +41,7 @@ public:
   std::vector< Node > d_vals;
 public:
   InstMatch(){}
-  InstMatch( Node f );
+  explicit InstMatch( TNode f );
   InstMatch( InstMatch* m );
 
   /** fill all unfilled values with m */
@@ -101,7 +101,7 @@ public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
 private:
-  void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
+  void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -129,7 +129,7 @@ public:
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, bool modEq = false,
                      bool modInst = false, ImtIndexOrder* imtio = NULL, bool onlyExist = false, int index = 0 );
   void print( std::ostream& out, Node q ) const{
-    std::vector< Node > terms;
+    std::vector< TNode > terms;
     print( out, q, terms );
   }
 };/* class InstMatchTrie */
@@ -142,7 +142,7 @@ public:
   /** is valid */
   context::CDO< bool > d_valid;
 private:
-  void print( std::ostream& out, Node q, std::vector< Node >& terms ) const;
+  void print( std::ostream& out, Node q, std::vector< TNode >& terms ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie(){}
@@ -170,7 +170,7 @@ public:
   bool addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m, context::Context* c, bool modEq = false,
                      bool modInst = false, int index = 0, bool onlyExist = false );
   void print( std::ostream& out, Node q ) const{
-    std::vector< Node > terms;
+    std::vector< TNode > terms;
     print( out, q, terms );
   }
 };/* class CDInstMatchTrie */

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 83733da428a63de0b20a79d95656d26cf5f0aa8f..3714ca4d09b0d652315712b5adcc90704b3e05b6 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -623,19 +623,18 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
 }
 
 void QuantifiersEngine::printInstantiations( std::ostream& out ) {
-  //Trace("ajr-temp") << "QE print inst." << std::endl;
-  //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 ){
-  //    out << "Instantiations of " << it->first << " : " << std::endl;
-  //    it->second->print( out, it->first );
-  //  }
-  //}else{
+  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 ){
+      out << "Instantiations of " << it->first << " : " << std::endl;
+      it->second->print( out, it->first );
+    }
+  }else{
     for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
       out << "Instantiations of " << it->first << " : " << std::endl;
       it->second.print( out, it->first );
       out << std::endl;
     }
-  //}
+  }
 }
 
 QuantifiersEngine::Statistics::Statistics():