Option for prenex normal form

diff --git a/src/options/quantifiers_options b/src/options/quantifiers_options
index f99333de2e3b7e6d7e7d5891bc586611e3e23fa7..462995becb22b65b3b412d3699e81a1ce715cc9a 100644 (file)
--- a/src/options/quantifiers_options
+++ b/src/options/quantifiers_options
@@ -17,10 +17,12 @@ option miniscopeQuant --miniscope-quant bool :default true :read-write
 # ( forall x. P( x ) ) V Q
 option miniscopeQuantFreeVar --miniscope-quant-fv bool :default true :read-write
  miniscope quantifiers for ground subformulas
-option quantSplit --quant-split bool :default true
+option quantSplit --quant-split bool :default true :read-write
  apply splitting to quantified formulas based on variable disjoint disjuncts
 option prenexQuant --prenex-quant=MODE CVC4::theory::quantifiers::PrenexQuantMode :default CVC4::theory::quantifiers::PRENEX_NO_USER_PAT :include "options/quantifiers_modes.h" :read-write :handler stringToPrenexQuantMode
  prenex mode for quantified formulas
+option prenexQuantAgg --prenex-quant-agg bool :default false :read-write
+ aggressive prenexing to ensure prenex normal form
 # Whether to variable-eliminate quantifiers.
 # For example, forall x y. ( P( x, y ) V x != c ) will be rewritten to
 #   forall y. P( c, y )

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 76a1e72c3f3ff5a68f821d890a5ac5b84a075d59..8a636c85ea61cfc5654d715cd42752855d2d1ef7 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1858,6 +1858,9 @@ void SmtEngine::setDefaults() {
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }
+  if( options::cbqiNestedQE() ){
+    options::prenexQuantAgg.set( true );
+  }
   //for induction techniques
   if( options::quantInduction() ){
     if( !options::dtStcInduction.wasSetByUser() ){
@@ -3951,7 +3954,7 @@ void SmtEnginePrivate::processAssertions() {
   }
   if( d_smt.d_logic.isQuantified() ){
     Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-quant-preprocess" << endl;
-
+    
     dumpAssertions("pre-skolem-quant", d_assertions);
     //remove rewrite rules, apply pre-skolemization to existential quantifiers
     for (unsigned i = 0; i < d_assertions.size(); ++ i) {

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.cpp b/src/theory/quantifiers/inst_strategy_cbqi.cpp
index 2c0e0a32fa74307d45e90475129669cff3006412..814b276d32c746cdb6bda3f7bae9295cdfe658cd 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.cpp
+++ b/src/theory/quantifiers/inst_strategy_cbqi.cpp
@@ -143,7 +143,7 @@ bool InstStrategyCbqi::registerCbqiLemma( Node q ) {
           //record these as counterexample quantifiers
           QAttributes qa;
           TermDb::computeQuantAttributes( quants[i], qa );
-          if( qa.d_qid_num!=-1 ){
+          if( !qa.d_qid_num.isNull() ){
             d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
             d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
             Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
@@ -292,7 +292,7 @@ Node InstStrategyCbqi::getIdMarkedQuantNode( Node n, std::map< Node, Node >& vis
     if( n.getKind()==FORALL ){
       QAttributes qa;
       TermDb::computeQuantAttributes( n, qa );
-      if( qa.d_qid_num==-1 ){
+      if( qa.d_qid_num.isNull() ){
         std::vector< Node > rc;
         rc.push_back( n[0] );
         rc.push_back( getIdMarkedQuantNode( n[1], visited ) );
@@ -403,9 +403,9 @@ Node InstStrategyCbqi::doNestedQERec( Node q, Node n, std::map< Node, Node >& vi
     if( n.getKind()==FORALL ){
       QAttributes qa;
       TermDb::computeQuantAttributes( n, qa );
-      if( qa.d_qid_num!=-1 ){
+      if( !qa.d_qid_num.isNull() ){
         //if it has an id, check whether we have done quantifier elimination for this id
-        std::map< int, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
+        std::map< Node, Node >::iterator it = d_id_to_ce_quant.find( qa.d_qid_num );
         if( it!=d_id_to_ce_quant.end() ){
           Node ceq = it->second;
           bool doNestedQe = d_elim_quants.contains( ceq );
@@ -998,7 +998,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
       return true;
     }else{
       //this should never happen for monotonic selection strategies
-      Trace("cbqi-warn") << "Existing instantiation" << std::endl;
+      Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
       Assert( !options::cbqiNestedQE() || options::cbqiAll() );
       return false;
     }

diff --git a/src/theory/quantifiers/inst_strategy_cbqi.h b/src/theory/quantifiers/inst_strategy_cbqi.h
index eb80de3cec3ee32d8ffad099c59afd060c38bcc3..e88842822f5f5991f997d4f67ceb6496cad54dce 100644 (file)
--- a/src/theory/quantifiers/inst_strategy_cbqi.h
+++ b/src/theory/quantifiers/inst_strategy_cbqi.h
@@ -71,8 +71,8 @@ protected:
   //mark ids on quantifiers 
   Node getIdMarkedQuantNode( Node n, std::map< Node, Node >& visited );
   // id to ce quant
-  std::map< int, Node > d_id_to_ce_quant;
-  std::map< Node, int > d_ce_quant_to_id;
+  std::map< Node, Node > d_id_to_ce_quant;
+  std::map< Node, Node > d_ce_quant_to_id;
   //do nested quantifier elimination recursive
   Node doNestedQENode( Node q, Node ceq, Node n, std::vector< Node >& inst_terms, bool doVts );
   Node doNestedQERec( Node q, Node n, std::map< Node, Node >& visited, std::vector< Node >& inst_terms, bool doVts );

diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index b0718699e9cf68d73c2d5428bc028e083140a6f0..24a6b78b0037eb9fad5ed4252c48af2d3285357d 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -1074,9 +1074,9 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >&
   return body;
 }
 
-Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){
+Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol ){
   if( body.getKind()==FORALL ){
-    if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
+    if( ( pol || options::prenexQuantAgg() ) && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){
       std::vector< Node > terms;
       std::vector< Node > subs;
       //for doing prenexing of same-signed quantifiers
@@ -1085,14 +1085,27 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
         terms.push_back( body[0][i] );
         subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) );
       }
-      args.insert( args.end(), subs.begin(), subs.end() );
+      if( pol ){
+        args.insert( args.end(), subs.begin(), subs.end() );
+      }else{
+        nargs.insert( nargs.end(), subs.begin(), subs.end() );
+      }
       Node newBody = body[1];
       newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() );
       return newBody;
-    }else{
-      return body;
     }
-  }else{
+  //must remove structure
+  }else if( options::prenexQuantAgg() && body.getKind()==kind::ITE && body.getType().isBoolean() ){
+    Node nn = NodeManager::currentNM()->mkNode( kind::AND,
+              NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
+              NodeManager::currentNM()->mkNode( kind::OR, body[0], body[2] ) );
+    return computePrenex( nn, args, nargs, pol );
+  }else if( options::prenexQuantAgg() && body.getKind()==kind::IFF ){
+    Node nn = NodeManager::currentNM()->mkNode( kind::AND,
+              NodeManager::currentNM()->mkNode( kind::OR, body[0].notNode(), body[1] ),
+              NodeManager::currentNM()->mkNode( kind::OR, body[0], body[1].notNode() ) );
+    return computePrenex( nn, args, nargs, pol );
+  }else if( body.getType().isBoolean() ){
     Assert( body.getKind()!=EXISTS );
     bool childrenChanged = false;
     std::vector< Node > newChildren;
@@ -1101,7 +1114,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       bool newPol;
       QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol );
       if( newHasPol ){
-        Node n = computePrenex( body[i], args, newPol );
+        Node n = computePrenex( body[i], args, nargs, newPol );
         newChildren.push_back( n );
         if( n!=body[i] ){
           childrenChanged = true;
@@ -1116,10 +1129,61 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b
       }else{
         return NodeManager::currentNM()->mkNode( body.getKind(), newChildren );
       }
+    }
+  }
+  return body;
+}
+
+Node QuantifiersRewriter::computePrenexAgg( Node n ){
+  if( containsQuantifiers( n ) ){
+    if( n.getKind()==NOT ){
+      return computePrenexAgg( n[0] ).negate();
+    }else if( n.getKind()==FORALL ){
+      Node nn = computePrenexAgg( n[1] );
+      if( nn!=n[1] ){
+        if( n.getNumChildren()==2 ){
+          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn );
+        }else{
+          return NodeManager::currentNM()->mkNode( FORALL, n[0], nn, n[2] );
+        }
+      }
     }else{
-      return body;
+      std::vector< Node > args;
+      std::vector< Node > nargs;
+      Node nn = computePrenex( n, args, nargs, true );
+      if( n!=nn ){
+        Node nnn = computePrenexAgg( nn );
+        //merge prenex
+        if( nnn.getKind()==FORALL ){
+          for( unsigned i=0; i<nnn[0].getNumChildren(); i++ ){
+            args.push_back( nnn[0][i] );
+          }
+          nnn = nnn[1];
+          //pos polarity variables are inner
+          if( !args.empty() ){
+            nnn = mkForall( args, nnn, true );
+          }
+          args.clear();
+        }else if( nnn.getKind()==NOT && nnn[0].getKind()==FORALL ){
+          for( unsigned i=0; i<nnn[0][0].getNumChildren(); i++ ){
+            nargs.push_back( nnn[0][0][i] );
+          }
+          nnn = nnn[0][1].negate();
+        }
+        if( !nargs.empty() ){
+          nnn = mkForall( nargs, nnn.negate(), true ).negate();
+        }
+        if( !args.empty() ){
+          nnn = mkForall( args, nnn, true );
+        }
+        return nnn;
+      }else{
+        Assert( args.empty() );
+        Assert( nargs.empty() );
+      }
     }
   }
+  return n;
 }
 
 Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) {
@@ -1237,6 +1301,26 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri
     return NodeManager::currentNM()->mkNode( kind::FORALL, children );
   }
 }
+Node QuantifiersRewriter::mkForall( std::vector< Node >& args, Node body, bool marked ) {
+  if( args.empty() ){
+    return body;
+  }else{
+    std::vector< Node > children;
+    children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) );
+    children.push_back( body );
+    std::vector< Node > iplc;
+    if( marked ){
+      Node avar = NodeManager::currentNM()->mkSkolem( "id", NodeManager::currentNM()->booleanType() );
+      QuantIdNumAttribute ida;
+      avar.setAttribute(ida,0);
+      iplc.push_back( NodeManager::currentNM()->mkNode( INST_ATTRIBUTE, avar ) );
+    }
+    if( !iplc.empty() ){
+      children.push_back( NodeManager::currentNM()->mkNode( INST_PATTERN_LIST, iplc ) );
+    }
+    return NodeManager::currentNM()->mkNode( FORALL, children );
+  }
+}
 
 //computes miniscoping, also eliminates variables that do not occur free in body
 Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){
@@ -1423,7 +1507,7 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q
 
 //general method for computing various rewrites
 Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttributes& qa ){
-  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << std::endl;
+  Trace("quantifiers-rewrite-debug") << "Compute operation " << computeOption << " on " << f << " " << qa.d_qid_num << std::endl;
   std::vector< Node > args;
   for( unsigned i=0; i<f[0].getNumChildren(); i++ ){
     args.push_back( f[0][i] );
@@ -1432,6 +1516,12 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   if( computeOption==COMPUTE_ELIM_SYMBOLS ){
     n = computeElimSymbols( n );
   }else if( computeOption==COMPUTE_MINISCOPING ){
+    if( options::prenexQuantAgg() ){
+      //if( isPrenexNormalForm( n ) ){
+      if( !qa.d_qid_num.isNull() ){
+        return f;
+      }
+    }
     //return directly
     return computeMiniscoping( args, n, qa );
   }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){
@@ -1446,7 +1536,16 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut
   }else if( computeOption==COMPUTE_COND_SPLIT ){
     n = computeCondSplit( n, qa );
   }else if( computeOption==COMPUTE_PRENEX ){
-    n = computePrenex( n, args, true );
+    if( options::prenexQuantAgg() ){
+      //Node pf = computePrenexAgg( f );
+      //Assert( isPrenexNormalForm( pf ) );
+      //will do it at preprocess time
+      return f;
+    }else{
+      std::vector< Node > nargs;
+      n = computePrenex( n, args, nargs, true );
+      Assert( nargs.empty() );
+    }
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
     n = computeVarElimination( n, args, qa );
   }
@@ -1592,6 +1691,15 @@ bool QuantifiersRewriter::containsQuantifiers( Node n ){
     return cq;
   }
 }
+bool QuantifiersRewriter::isPrenexNormalForm( Node n ) {
+  if( n.getKind()==FORALL ){
+    return n[1].getKind()!=FORALL && isPrenexNormalForm( n[1] );
+  }else if( n.getKind()==NOT ){
+    return n[0].getKind()!=NOT && isPrenexNormalForm( n[0] );
+  }else{
+    return !containsQuantifiers( n );
+  }
+}
 
 Node QuantifiersRewriter::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector< TNode >& fvs ){
   Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << endl;
@@ -1677,6 +1785,11 @@ Node QuantifiersRewriter::preprocess( Node n, bool isInst ) {
       }
     }
   }
+  //pull all quantifiers globally
+  if( options::prenexQuantAgg() ){
+    n = quantifiers::QuantifiersRewriter::computePrenexAgg( n );
+    Assert( isPrenexNormalForm( n ) );
+  }
   if( n!=prev ){       
     Trace("quantifiers-preprocess") << "Preprocess " << prev << std::endl;
     Trace("quantifiers-preprocess") << "..returned " << n << std::endl;

diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h
index 60dc8ab10bbb5548e30944fc7e4035fb30acbedf..bb352f65cd0ca5df24ce6c6365f2a63a72944094 100644 (file)
--- a/src/theory/quantifiers/quantifiers_rewriter.h
+++ b/src/theory/quantifiers/quantifiers_rewriter.h
@@ -38,7 +38,6 @@ public:
 private:
   static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged );
   static void addNodeToOrBuilder( Node n, NodeBuilder<>& t );
-  static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
   static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited );
   static void computeArgVec( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n );
   static void computeArgVec2( std::vector< Node >& args, std::vector< Node >& activeArgs, Node n, Node ipl );
@@ -53,14 +52,15 @@ private:
   static bool computeVariableElimLit( Node n, bool pol, std::vector< Node >& args, std::vector< Node >& var, std::vector< Node >& subs,
                                       std::map< Node, std::map< bool, std::map< Node, bool > > >& num_bounds );
   static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa );
-private:
+public:
   static Node computeElimSymbols( Node body );
   static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
   //cache is dependent upon currCond, icache is not, new_conds are negated conditions
   static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa );
   static Node computeCondSplit( Node body, QAttributes& qa );
-  static Node computePrenex( Node body, std::vector< Node >& args, bool pol );
+  static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol );
+  static Node computePrenexAgg( Node n );
   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
   static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa );
 private:
@@ -89,8 +89,11 @@ private:
   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 public:
   static Node rewriteRewriteRule( Node r );
-  static bool containsQuantifiers(Node n);
+  static bool containsQuantifiers( Node n );
+  static bool isPrenexNormalForm( Node n );
   static Node preprocess( Node n, bool isInst = false );
+  static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
+  static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
 };/* class QuantifiersRewriter */
 
 }/* CVC4::theory::quantifiers namespace */

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index f253d655b66d059e6ff6a0d70f20e137607de7a4..e7b7268b5a7839a1c6753904653e9045523ac8ac 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -2170,8 +2170,8 @@ void TermDb::computeQuantAttributes( Node q, QAttributes& qa ){
           //don't set owner, should happen naturally
         }
         if( avar.hasAttribute(QuantIdNumAttribute()) ){
-          qa.d_qid_num = avar.getAttribute(QuantIdNumAttribute());
-          Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num << " : " << q << std::endl;
+          qa.d_qid_num = avar;
+          Trace("quant-attr") << "Attribute : id number " << qa.d_qid_num.getAttribute(QuantIdNumAttribute()) << " : " << q << std::endl;
         }
         if( avar.getKind()==REWRITE_RULE ){
           Trace("quant-attr") << "Attribute : rewrite rule : " << q << std::endl;
@@ -2265,9 +2265,19 @@ bool TermDb::isQAttrQuantElimPartial( Node q ) {
 }
 
 int TermDb::getQAttrQuantIdNum( Node q ) {
+  std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
+  if( it!=d_qattr.end() ){
+    if( !it->second.d_qid_num.isNull() ){
+      return it->second.d_qid_num.getAttribute(QuantIdNumAttribute());
+    }
+  }
+  return -1;
+}
+
+Node TermDb::getQAttrQuantIdNumNode( Node q ) {
   std::map< Node, QAttributes >::iterator it = d_qattr.find( q );
   if( it==d_qattr.end() ){
-    return -1;
+    return Node::null();
   }else{
     return it->second.d_qid_num;
   }

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 29b7b93c66de5614dcc07176a60cfec36daeab85..dd91cde3390306a7f568c040bfbc68af3f287f3d 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -136,7 +136,7 @@ public:
 class QAttributes{
 public:
   QAttributes() : d_hasPattern(false), d_conjecture(false), d_axiom(false), d_sygus(false),
-                  d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false), d_qid_num(-1){}
+                  d_synthesis(false), d_rr_priority(-1), d_qinstLevel(-1), d_quant_elim(false), d_quant_elim_partial(false){}
   ~QAttributes(){}
   bool d_hasPattern;
   Node d_rr;
@@ -150,7 +150,7 @@ public:
   bool d_quant_elim;
   bool d_quant_elim_partial;
   Node d_ipl;
-  int d_qid_num;
+  Node d_qid_num;
   bool isRewriteRule() { return !d_rr.isNull(); }
   bool isFunDef() { return !d_fundef_f.isNull(); }
 };
@@ -551,6 +551,8 @@ public:
   bool isQAttrQuantElimPartial( Node q );
   /** get quant id num */
   int getQAttrQuantIdNum( Node q );
+  /** get quant id num */
+  Node getQAttrQuantIdNumNode( Node q );
   /** compute quantifier attributes */
   static void computeQuantAttributes( Node q, QAttributes& qa );
 };/* class TermDb */