Fixes to quantifiers rewriter to prevent miniscoping nested quantifiers. Minor fixes to ambqi. Preparation for CASC proof output. Add NNF option.

9 files changed, 145 insertions, 82 deletions

diff --git a/src/theory/quantifiers/ambqi_builder.cpp b/src/theory/quantifiers/ambqi_builder.cpp
index e3f031d11..7f119ae93 100755
--- a/src/theory/quantifiers/ambqi_builder.cpp
+++ b/src/theory/quantifiers/ambqi_builder.cpp
@@ -863,7 +863,7 @@ bool AbsMbqiBuilder::doExhaustiveInstantiation( FirstOrderModel * fm, Node q, in
 

 bool AbsMbqiBuilder::doCheck( FirstOrderModelAbs * m, TNode q, AbsDef & ad, TNode n ) {

   Assert( n.getKind()!=FORALL );

-  if( n.getKind()==NOT ){

+  if( n.getKind()==NOT && n[0].getKind()!=FORALL ){

     doCheck( m, q, ad, n[0] );

     ad.negate();

     return true;

diff --git a/src/theory/quantifiers/inst_match.cpp b/src/theory/quantifiers/inst_match.cpp
index a74c51a9a..096d0cab2 100644
--- a/src/theory/quantifiers/inst_match.cpp
+++ b/src/theory/quantifiers/inst_match.cpp
@@ -198,6 +198,24 @@ bool InstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< No
   }
 }
 
+void InstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const {
+  if( terms.size()==q[0].getNumChildren() ){
+    Trace(c) << "  ( ";
+    for( unsigned i=0; i<terms.size(); i++ ){
+      if( i>0 ) Trace(c) << ", ";
+      Trace(c) << terms[i];
+    }
+    Trace(c) << " )" << std::endl;
+  }else{
+    for( std::map< Node, InstMatchTrie >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
+      terms.push_back( it->first );
+      it->second.print( c, q, terms );
+      terms.pop_back();
+    }
+  }
+}
+
+
 bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector< Node >& m,
                                     context::Context* c, bool modEq, bool modInst, int index, bool onlyExist ){
   bool reset = false;
@@ -264,6 +282,25 @@ bool CDInstMatchTrie::addInstMatch( QuantifiersEngine* qe, Node f, std::vector<
   }
 }
 
+void CDInstMatchTrie::print( const char * c, Node q, std::vector< Node >& terms ) const{
+  if( d_valid.get() ){
+    if( terms.size()==q[0].getNumChildren() ){
+      Trace(c) << "  ( ";
+      for( unsigned i=0; i<terms.size(); i++ ){
+        if( i>0 ) Trace(c) << ", ";
+        Trace(c) << terms[i];
+      }
+      Trace(c) << " )" << std::endl;
+    }else{
+      for( std::map< Node, CDInstMatchTrie* >::const_iterator it = d_data.begin(); it != d_data.end(); ++it ){
+        terms.push_back( it->first );
+        it->second->print( c, q, terms );
+        terms.pop_back();
+      }
+    }
+  }
+}
+
 }/* CVC4::theory::inst namespace */
 }/* CVC4::theory namespace */
 }/* CVC4 namespace */
diff --git a/src/theory/quantifiers/inst_match.h b/src/theory/quantifiers/inst_match.h
index c366c4a09..2cf63210b 100644
--- a/src/theory/quantifiers/inst_match.h
+++ b/src/theory/quantifiers/inst_match.h
@@ -100,6 +100,8 @@ public:
 public:
   /** the data */
   std::map< Node, InstMatchTrie > d_data;
+private:
+  void print( const char * c, Node q, std::vector< Node >& terms ) const;
 public:
   InstMatchTrie(){}
   ~InstMatchTrie(){}
@@ -126,6 +128,10 @@ 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( const char * c, Node q ) const{
+    std::vector< Node > terms;
+    print( c, q, terms );
+  }
 };/* class InstMatchTrie */
 
 /** trie for InstMatch objects */
@@ -135,6 +141,8 @@ public:
   std::map< Node, CDInstMatchTrie* > d_data;
   /** is valid */
   context::CDO< bool > d_valid;
+private:
+  void print( const char * c, Node q, std::vector< Node >& terms ) const;
 public:
   CDInstMatchTrie( context::Context* c ) : d_valid( c, false ){}
   ~CDInstMatchTrie(){}
@@ -161,6 +169,10 @@ 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( const char * c, Node q ) const{
+    std::vector< Node > terms;
+    print( c, q, terms );
+  }
 };/* class CDInstMatchTrie */
 
 
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 10c538dd9..38db10feb 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -33,6 +33,9 @@ option simpleIteLiftQuant /--disable-ite-lift-quant bool :default true
 # Whether to CNF quantifier bodies
 option cnfQuant --cnf-quant bool :default false
  apply CNF conversion to quantified formulas
+# Whether to NNF quantifier bodies
+option nnfQuant --nnf-quant bool :default false
+ apply NNF conversion to quantified formulas
 
 option clauseSplit --clause-split bool :default false
  apply clause splitting to quantified formulas
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index 38fc1d919..c42c16043 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -139,7 +139,7 @@ void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< No
     if( n.getKind()==FORALL || n.getKind()==EXISTS ){
       Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
       NestedQuantAttribute nqai;
-      n.setAttribute(nqai,q);
+      n[0].setAttribute(nqai,q);
     }
     for( int i=0; i<(int)n.getNumChildren(); i++ ){
       setNestedQuantifiers2( n[i], q, processed );
@@ -148,8 +148,8 @@ void QuantifiersRewriter::setNestedQuantifiers2( Node n, Node q, std::vector< No
 }
 
 RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
-  Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
+    Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in[0].hasAttribute(NestedQuantAttribute()) << std::endl;
     if( !in.hasAttribute(NestedQuantAttribute()) ){
       setNestedQuantifiers( in[ 1 ], in );
     }
@@ -188,7 +188,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
   Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << std::endl;
-  Trace("quantifiers-rewrite-debug") << "Attributes : " << in.hasAttribute(NestedQuantAttribute())  << std::endl;
+  Trace("quantifiers-rewrite-debug") << "Attributes : " << in[0].hasAttribute(NestedQuantAttribute())  << std::endl;
   if( !options::quantRewriteRules() || !TermDb::isRewriteRule( in ) ){
     RewriteStatus status = REWRITE_DONE;
     Node ret = in;
@@ -214,10 +214,10 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       ret = ret.negate();
       status = REWRITE_AGAIN_FULL;
     }else{
-      bool isNested = in.hasAttribute(NestedQuantAttribute());
+      bool isNested = in[0].hasAttribute(NestedQuantAttribute());
       for( int op=0; op<COMPUTE_LAST; op++ ){
         if( doOperation( in, isNested, op ) ){
-          ret = computeOperation( in, op );
+          ret = computeOperation( in, isNested, op );
           if( ret!=in ){
             status = REWRITE_AGAIN_FULL;
             break;
@@ -231,9 +231,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
       Trace("quantifiers-rewrite") << " to " << std::endl;
       Trace("quantifiers-rewrite") << ret << std::endl;
-      Trace("quantifiers-rewrite-debug") << "Attributes : " << ret.hasAttribute(NestedQuantAttribute()) << std::endl;
-
-
+      //Trace("quantifiers-rewrite-debug") << "Attributes : " << ret[0].hasAttribute(NestedQuantAttribute()) << std::endl;
     }
     return RewriteResponse( status, ret );
   }
@@ -421,12 +419,11 @@ Node QuantifiersRewriter::computeClause( Node n ){
 }
 
 void QuantifiersRewriter::setAttributes( Node in, Node n ) {
-  if( in.hasAttribute(NestedQuantAttribute()) ){
-    setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
+  if( n.getKind()==FORALL && in.getKind()==FORALL ){
+    if( in[0].hasAttribute(NestedQuantAttribute()) ){
+      setNestedQuantifiers( n[0], in[0].getAttribute(NestedQuantAttribute()) );
+    }
   }
-  //if( in.hasAttribute(QRewriteRuleAttribute()) ){
-  //  n.setAttribute(QRewriteRuleAttribute(), in.getAttribute(QRewriteRuleAttribute()));
-  //}
 }
 
 Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){
@@ -691,68 +688,6 @@ Node QuantifiersRewriter::computeSplit( Node f, Node body, std::vector< Node >&
   return f;
 }
 
-//general method for computing various rewrites
-Node QuantifiersRewriter::computeOperation( Node f, int computeOption ){
-  if( f.getKind()==FORALL ){
-    Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
-    std::vector< Node > args;
-    for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
-      args.push_back( f[0][i] );
-    }
-    NodeBuilder<> defs(kind::AND);
-    Node n = f[1];
-    Node ipl;
-    if( f.getNumChildren()==3 ){
-      ipl = f[2];
-    }
-    if( computeOption==COMPUTE_ELIM_SYMBOLS ){
-      n = computeElimSymbols( n );
-    }else if( computeOption==COMPUTE_MINISCOPING ){
-      //return directly
-      return computeMiniscoping( f, args, n, ipl, f.hasAttribute(NestedQuantAttribute()) );
-    }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
-      return computeAggressiveMiniscoping( args, n, f.hasAttribute(NestedQuantAttribute()) );
-    }else if( computeOption==COMPUTE_NNF ){
-      n = computeNNF( n );
-    }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
-      n = computeSimpleIteLift( n );
-    }else if( computeOption==COMPUTE_PRENEX ){
-      n = computePrenex( n, args, true );
-    }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
-      Node prev;
-      do{
-        prev = n;
-        n = computeVarElimination( n, args, ipl );
-      }while( prev!=n && !args.empty() );
-    }else if( computeOption==COMPUTE_CNF ){
-      //n = computeNNF( n );
-      n = computeCNF( n, args, defs, false );
-      ipl = Node::null();
-    }else if( computeOption==COMPUTE_SPLIT ) {
-      return computeSplit(f, n, args );
-    }
-    Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
-    if( f[1]==n && args.size()==f[0].getNumChildren() ){
-      return f;
-    }else{
-      if( args.empty() ){
-        defs << n;
-      }else{
-        std::vector< Node > children;
-        children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
-        children.push_back( n );
-        if( !ipl.isNull() ){
-          children.push_back( ipl );
-        }
-        defs << NodeManager::currentNM()->mkNode(kind::FORALL, children );
-      }
-      return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode();
-    }
-  }else{
-    return f;
-  }
-}
-
 Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, Node ipl ){
   std::vector< Node > activeArgs;
   computeArgVec( args, activeArgs, body );
@@ -973,15 +908,15 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
     return options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_NNF ){
-    return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
+    return options::nnfQuant();
   }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
-    return options::simpleIteLiftQuant();//!options::finiteModelFind();
+    return options::simpleIteLiftQuant();
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant() && !options::aggressiveMiniscopeQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     return options::varElimQuant();
   }else if( computeOption==COMPUTE_CNF ){
-    return false;//return options::cnfQuant() ;
+    return false;//return options::cnfQuant() ; FIXME
   }else if( computeOption==COMPUTE_SPLIT ){
     return options::clauseSplit();
   }else{
@@ -989,7 +924,67 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption
   }
 }
 
-
+//general method for computing various rewrites
+Node QuantifiersRewriter::computeOperation( Node f, bool isNested, int computeOption ){
+  if( f.getKind()==FORALL ){
+    Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << ", nested = " << isNested << std::endl;
+    std::vector< Node > args;
+    for( int i=0; i<(int)f[0].getNumChildren(); i++ ){
+      args.push_back( f[0][i] );
+    }
+    NodeBuilder<> defs(kind::AND);
+    Node n = f[1];
+    Node ipl;
+    if( f.getNumChildren()==3 ){
+      ipl = f[2];
+    }
+    if( computeOption==COMPUTE_ELIM_SYMBOLS ){
+      n = computeElimSymbols( n );
+    }else if( computeOption==COMPUTE_MINISCOPING ){
+      //return directly
+      return computeMiniscoping( f, args, n, ipl, isNested );
+    }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
+      return computeAggressiveMiniscoping( args, n, isNested );
+    }else if( computeOption==COMPUTE_NNF ){
+      n = computeNNF( n );
+    }else if( computeOption==COMPUTE_SIMPLE_ITE_LIFT ){
+      n = computeSimpleIteLift( n );
+    }else if( computeOption==COMPUTE_PRENEX ){
+      n = computePrenex( n, args, true );
+    }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
+      Node prev;
+      do{
+        prev = n;
+        n = computeVarElimination( n, args, ipl );
+      }while( prev!=n && !args.empty() );
+    }else if( computeOption==COMPUTE_CNF ){
+      //n = computeNNF( n );
+      n = computeCNF( n, args, defs, false );
+      ipl = Node::null();
+    }else if( computeOption==COMPUTE_SPLIT ) {
+      return computeSplit(f, n, args );
+    }
+    Trace("quantifiers-rewrite-debug") << "Compute Operation: return " << n << ", " << args.size() << std::endl;
+    if( f[1]==n && args.size()==f[0].getNumChildren() ){
+      return f;
+    }else{
+      if( args.empty() ){
+        defs << n;
+      }else{
+        std::vector< Node > children;
+        children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+        children.push_back( n );
+        if( !ipl.isNull() ){
+          children.push_back( ipl );
+        }
+        defs << NodeManager::currentNM()->mkNode(kind::FORALL, children );
+      }
+      return defs.getNumChildren()==1 ? defs.getChild( 0 ) : defs.constructNode();
+    }
+  }else{
+    return f;
+  }
+}
 
 
 Node QuantifiersRewriter::rewriteRewriteRule( Node r ) {
diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 0cb76f686..a6a8a6780 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -69,7 +69,7 @@ private:
     COMPUTE_SPLIT,
     COMPUTE_LAST
   };
-  static Node computeOperation( Node f, int computeOption );
+  static Node computeOperation( Node f, bool isNested, int computeOption );
 public:
   static RewriteResponse preRewrite(TNode in);
   static RewriteResponse postRewrite(TNode in);
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index 964ea9c73..64965f5ce 100644
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -506,7 +506,7 @@ Node TermDb::mkSkolemizedBody( Node f, Node n, std::vector< TypeNode >& argTypes
       }
     }
   }
-
+  Trace("quantifiers-sk") << "mkSkolem body for " << f << " returns : " << ret << std::endl;
   return ret;
 }
 
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 929a638d7..8fecc6ee0 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -623,6 +623,20 @@ void QuantifiersEngine::getPhaseReqTerms( Node f, std::vector< Node >& nodes ){
   }
 }
 
+void QuantifiersEngine::printInstantiations( const char * c ) {
+  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 ){
+      Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
+      it->second->print( c, it->first );
+    }
+  }else{
+    for( std::map< Node, inst::InstMatchTrie >::iterator it = d_inst_match_trie.begin(); it != d_inst_match_trie.end(); ++it ){
+      Trace(c) << "Instantiations of " << it->first << " : " << std::endl;
+      it->second.print( c, it->first );
+    }
+  }
+}
+
 QuantifiersEngine::Statistics::Statistics():
   d_num_quant("QuantifiersEngine::Num_Quantifiers", 0),
   d_instantiation_rounds("QuantifiersEngine::Rounds_Instantiation_Full", 0),
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index eb9803592..7a899db0c 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -235,6 +235,8 @@ public:
   /** get the master equality engine */
   eq::EqualityEngine* getMasterEqualityEngine() ;
 public:
+  /** print instantiations */
+  void printInstantiations( const char * c );
   /** statistics class */
   class Statistics {
   public: