initial draft of skolemization during pre-processing, made simple cliques the default option for uf strong solver

5 files changed, 154 insertions, 19 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b968da2e0..5e8cef250 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -261,6 +261,11 @@ class SmtEnginePrivate : public NodeManagerListener {
    */
   bool simplifyAssertions() throw(TypeCheckingException);
 
+  /**
+   * contains quantifiers
+   */
+  bool containsQuantifiers( Node n );
+
 public:
 
   SmtEnginePrivate(SmtEngine& smt) :
@@ -352,6 +357,11 @@ public:
   Node expandDefinitions(TNode n, hash_map<Node, Node, NodeHashFunction>& cache)
     throw(TypeCheckingException);
 
+  /**
+   * pre-skolemize quantifiers
+   */
+  Node preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs );
+
 };/* class SmtEnginePrivate */
 
 }/* namespace CVC4::smt */
@@ -999,6 +1009,104 @@ Node SmtEnginePrivate::expandDefinitions(TNode n, hash_map<Node, Node, NodeHashF
   }
 }
 
+Node SmtEnginePrivate::preSkolemizeQuantifiers( Node n, bool polarity, std::vector< Node >& fvs ){
+  Trace("pre-sk") << "Pre-skolem " << n << " " << polarity << " " << fvs.size() << std::endl;
+  if( n.getKind()==kind::NOT ){
+    Node nn = preSkolemizeQuantifiers( n[0], !polarity, fvs );
+    return nn.negate();
+  }else if( n.getKind()==kind::FORALL ){
+    if( polarity ){
+      std::vector< Node > children;
+      children.push_back( n[0] );
+      //add children to current scope
+      std::vector< Node > fvss;
+      fvss.insert( fvss.begin(), fvs.begin(), fvs.end() );
+      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+        fvss.push_back( n[0][i] );
+      }
+      //process body
+      children.push_back( preSkolemizeQuantifiers( n[1], polarity, fvss ) );
+      if( n.getNumChildren()==3 ){
+        children.push_back( n[2] );
+      }
+      //return processed quantifier
+      return NodeManager::currentNM()->mkNode( kind::FORALL, children );
+    }else{
+      //process body
+      Node nn = preSkolemizeQuantifiers( n[1], polarity, fvs );
+      //now, substitute skolems for the variables
+      std::vector< TypeNode > argTypes;
+      for( int i=0; i<(int)fvs.size(); i++ ){
+        argTypes.push_back( fvs[i].getType() );
+      }
+      //calculate the variables and substitution
+      std::vector< Node > vars;
+      std::vector< Node > subs;
+      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+        vars.push_back( n[0][i] );
+      }
+      for( int i=0; i<(int)n[0].getNumChildren(); i++ ){
+        //make the new function symbol
+        if( argTypes.empty() ){
+          Node s = NodeManager::currentNM()->mkSkolem( "sk_$$", n[0][i].getType(), "created during pre-skolemization" );
+          subs.push_back( s );
+        }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() );
+          subs.push_back( NodeManager::currentNM()->mkNode( kind::APPLY_UF, funcArgs ) );
+        }
+      }
+      //apply substitution
+      nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
+      return nn;
+    }
+  }else{
+    //check if it contains a quantifier as a subterm
+    bool containsQuant = false;
+    if( n.getType().isBoolean() ){
+      for( int i=0; i<(int)n.getNumChildren(); i++ ){
+        if( containsQuantifiers( n[i] ) ){
+          containsQuant = true;
+          break;
+        }
+      }
+    }
+    //if so, we will write this node
+    if( containsQuant ){
+      if( n.getKind()==kind::ITE || n.getKind()==kind::IFF || n.getKind()==kind::XOR || n.getKind()==kind::IMPLIES ){
+        Node nn;
+        //must remove structure
+        if( n.getKind()==kind::ITE ){
+          nn = NodeManager::currentNM()->mkNode( kind::AND,
+                 NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] ),
+                 NodeManager::currentNM()->mkNode( kind::OR, n[0], n[2] ) );
+        }else if( n.getKind()==kind::IFF || n.getKind()==kind::XOR ){
+          nn = NodeManager::currentNM()->mkNode( kind::AND,
+                 NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n.getKind()==kind::XOR ? n[1].notNode() : n[1] ),
+                 NodeManager::currentNM()->mkNode( kind::OR, n[0], n.getKind()==kind::XOR ? n[1] : n[1].notNode() ) );
+        }else if( n.getKind()==kind::IMPLIES ){
+          nn = NodeManager::currentNM()->mkNode( kind::OR, n[0].notNode(), n[1] );
+        }
+        return preSkolemizeQuantifiers( nn, polarity, fvs );
+      }else{
+        Assert( n.getKind()==AND || n.getKind()==OR );
+        std::vector< Node > children;
+        for( int i=0; i<(int)n.getNumChildren(); i++ ){
+          children.push_back( preSkolemizeQuantifiers( n[i], polarity, fvs ) );
+        }
+        return NodeManager::currentNM()->mkNode( n.getKind(), children );
+      }
+    }else{
+      return n;
+    }
+  }
+}
+
 void SmtEnginePrivate::removeITEs() {
   d_smt.finalOptionsAreSet();
 
@@ -1454,6 +1562,20 @@ bool SmtEnginePrivate::simplifyAssertions()
   return true;
 }
 
+
+bool SmtEnginePrivate::containsQuantifiers( Node n ){
+  if( n.getKind()==kind::FORALL ){
+    return true;
+  }else{
+    for( int i=0; i<(int)n.getNumChildren(); i++ ){
+      if( containsQuantifiers( n[i] ) ){
+        return true;
+      }
+    }
+    return false;
+  }
+}
+
 Result SmtEngine::check() {
   Assert(d_fullyInited);
   Assert(d_pendingPops == 0);
@@ -1556,6 +1678,19 @@ void SmtEnginePrivate::processAssertions() {
     Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << endl;
   }
 
+  if( options::preSkolemQuant() ){
+    //apply pre-skolemization to existential quantifiers
+    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
+      Node prev = d_assertionsToPreprocess[i];
+      std::vector< Node > fvs;
+      d_assertionsToPreprocess[i] = Rewriter::rewrite( preSkolemizeQuantifiers( d_assertionsToPreprocess[i], true, fvs ) );
+      if( prev!=d_assertionsToPreprocess[i] ){
+        Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << std::endl;
+        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << std::endl;
+      }
+    }
+  }
+
   Chat() << "simplifying assertions..." << endl;
   bool noConflict = simplifyAssertions();
 
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp
index c6987a85a..17fd3ba41 100644
--- a/src/theory/quantifiers/quantifiers_rewriter.cpp
+++ b/src/theory/quantifiers/quantifiers_rewriter.cpp
@@ -134,7 +134,7 @@ bool QuantifiersRewriter::hasArg( std::vector< Node >& args, Node n ){
 
 void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
   if( n.getKind()==FORALL || n.getKind()==EXISTS ){
-    Debug("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
+    Trace("quantifiers-rewrite-debug") << "Set nested quant attribute " << n << std::endl;
     NestedQuantAttribute nqai;
     n.setAttribute(nqai,q);
   }
@@ -144,7 +144,7 @@ void QuantifiersRewriter::setNestedQuantifiers( Node n, Node q ){
 }
 
 RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
-  Debug("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
+  Trace("quantifiers-rewrite-debug") << "pre-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
     if( !in.hasAttribute(NestedQuantAttribute()) ){
       setNestedQuantifiers( in[ 1 ], in );
@@ -174,9 +174,9 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
         if( in.hasAttribute(NestedQuantAttribute()) ){
           setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
         }
-        Debug("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
-        Debug("quantifiers-pre-rewrite") << " to " << std::endl;
-        Debug("quantifiers-pre-rewrite") << n << std::endl;
+        Trace("quantifiers-pre-rewrite") << "*** pre-rewrite " << in << std::endl;
+        Trace("quantifiers-pre-rewrite") << " to " << std::endl;
+        Trace("quantifiers-pre-rewrite") << n << std::endl;
       }
       return RewriteResponse(REWRITE_DONE, n);
     }
@@ -185,7 +185,7 @@ RewriteResponse QuantifiersRewriter::preRewrite(TNode in) {
 }
 
 RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
-  Debug("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
+  Trace("quantifiers-rewrite-debug") << "post-rewriting " << in << " " << in.hasAttribute(NestedQuantAttribute()) << std::endl;
   if( in.getKind()==kind::EXISTS || in.getKind()==kind::FORALL ){
     //get the arguments
     std::vector< Node > args;
@@ -200,7 +200,7 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
     //get the instantiation pattern list
     Node ipl;
     if( in.getNumChildren()==3 ){
-      ipl = in[2];  
+      ipl = in[2];
     }
     bool isNested = in.hasAttribute(NestedQuantAttribute());
     //compute miniscoping first
@@ -219,9 +219,9 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) {
       if( in.hasAttribute(NestedQuantAttribute()) ){
         setNestedQuantifiers( n, in.getAttribute(NestedQuantAttribute()) );
       }
-      Debug("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
-      Debug("quantifiers-rewrite") << " to " << std::endl;
-      Debug("quantifiers-rewrite") << n << std::endl;
+      Trace("quantifiers-rewrite") << "*** rewrite " << in << std::endl;
+      Trace("quantifiers-rewrite") << " to " << std::endl;
+      Trace("quantifiers-rewrite") << n << std::endl;
       if( in.hasAttribute(InstConstantAttribute()) ){
         InstConstantAttribute ica;
         n.setAttribute(ica,in.getAttribute(InstConstantAttribute()) );
@@ -389,7 +389,7 @@ Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBui
       predArgs.push_back( op );
       predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() );
       Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs );
-      Debug("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl;
+      Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl;
       //create the bound var list
       Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs );
       //now, look at the structure of nt
@@ -676,9 +676,9 @@ Node QuantifiersRewriter::rewriteQuant( Node n, bool isNested, bool duringRewrit
       Node prev2 = n;
       n = computeOperation( n, op );
       if( prev2!=n ){
-        Debug("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl;
-        Debug("quantifiers-rewrite-op") << " to " << std::endl;
-        Debug("quantifiers-rewrite-op") << n << std::endl;
+        Trace("quantifiers-rewrite-op") << "Rewrite op " << op << ": rewrite " << prev2 << std::endl;
+        Trace("quantifiers-rewrite-op") << " to " << std::endl;
+        Trace("quantifiers-rewrite-op") << n << std::endl;
       }
     }
   }
@@ -710,7 +710,7 @@ bool QuantifiersRewriter::doOperation( Node f, bool isNested, int computeOption,
   if( computeOption==COMPUTE_NNF ){
     return false;//TODO: compute NNF (current bad idea since arithmetic rewrites equalities)
   }else if( computeOption==COMPUTE_PRE_SKOLEM ){
-    return options::preSkolemQuant() && !duringRewrite;
+    return false;//options::preSkolemQuant() && !duringRewrite;
   }else if( computeOption==COMPUTE_PRENEX ){
     return options::prenexQuant();
   }else if( computeOption==COMPUTE_VAR_ELIMINATION ){
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp
index 3bd2945e8..49a1f8332 100644
--- a/src/theory/quantifiers/trigger.cpp
+++ b/src/theory/quantifiers/trigger.cpp
@@ -285,7 +285,7 @@ bool Trigger::isUsableTrigger( Node n, Node f ){
 }
 
 bool Trigger::isAtomicTrigger( Node n ){
-  return n.getKind()==APPLY_UF || n.getKind()==SELECT || n.getKind()==STORE ||
+  return ( n.getKind()==APPLY_UF && !n.getOperator().getAttribute(NoMatchAttribute()) ) || n.getKind()==SELECT || n.getKind()==STORE ||
          n.getKind()==APPLY_CONSTRUCTOR || n.getKind()==APPLY_SELECTOR || n.getKind()==APPLY_TESTER;
 }
 bool Trigger::isSimpleTrigger( Node n ){
diff --git a/src/theory/uf/options b/src/theory/uf/options
index 3b6a0818f..f199f6c1b 100644
--- a/src/theory/uf/options
+++ b/src/theory/uf/options
@@ -25,7 +25,7 @@ option ufssSmartSplits --uf-ss-smart-split bool :default false
  use smart splitting heuristic for uf strong solver
 option ufssModelInference --uf-ss-model-infer bool :default false
  use model inference method for uf strong solver
-option ufssSimpleCliques --uf-ss-simple-cliques bool :default false
- add simple clique lemmas for uf strong solver
+option ufssExplainedCliques --uf-ss-explained-cliques bool :default false
+ add explained clique lemmas for uf strong solver
 
 endmodule
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 3f82a6948..712d6426b 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -1009,7 +1009,7 @@ void StrongSolverTheoryUf::SortRepModel::addCliqueLemma( std::vector< Node >& cl
   while( clique.size()>size_t(d_cardinality+1) ){
     clique.pop_back();
   }
-  if( options::ufssSimpleCliques() ){
+  if( !options::ufssExplainedCliques() ){
     //add as lemma
     std::vector< Node > eqs;
     for( int i=0; i<(int)clique.size(); i++ ){