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

4 files changed, 19 insertions, 19 deletions

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++ ){