Extend synthesis solver to handle single invocation with additional universal quantification. Refactor query/check-sat to call one internal function in SmtEngine. Make check-synth its own command. Minor work on quant ee.

4 files changed, 136 insertions, 40 deletions

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 80585a33d..850c98437 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -845,6 +845,7 @@ bool SingleInvocationPartition::init( Node n ) {
   if( inferArgTypes( n, typs, visited ) ){
     return init( typs, n );  
   }else{
+    Trace("si-prt") << "Could not infer argument types." << std::endl;
     return false;
   }
 }
@@ -854,7 +855,7 @@ bool SingleInvocationPartition::inferArgTypes( Node n, std::vector< TypeNode >&
     visited[n] = true;
     if( n.getKind()!=FORALL ){
     //if( TermDb::hasBoundVarAttr( n ) ){
-      if( n.getKind()==APPLY_UF ){
+      if( n.getKind()==d_checkKind ){
         for( unsigned i=0; i<n.getNumChildren(); i++ ){
           typs.push_back( n[i].getType() );
         }
@@ -882,6 +883,7 @@ bool SingleInvocationPartition::init( std::vector< TypeNode >& typs, Node n ){
     Node si_v = NodeManager::currentNM()->mkBoundVar( ss.str(), d_arg_types[j] );
     d_si_vars.push_back( si_v );
   }
+  Trace("si-prt") << "Process the formula..." << std::endl;
   process( n );
   return true;
 }
@@ -909,6 +911,7 @@ void SingleInvocationPartition::process( Node n ) {
       std::vector< Node > terms;
       std::vector< Node > subs;
       bool singleInvocation = true;
+      bool ngroundSingleInvocation = false;
       if( processConjunct( cr, visited, args, terms, subs ) ){
         for( unsigned j=0; j<terms.size(); j++ ){
           si_terms.push_back( subs[j] );
@@ -944,6 +947,7 @@ void SingleInvocationPartition::process( Node n ) {
         TermDb::getBoundVars( cr, bvs );
         if( bvs.size()>d_si_vars.size() ){
           Trace("si-prt") << "...not ground single invocation." << std::endl;
+          ngroundSingleInvocation = true;
           singleInvocation = false;
         }else{
           Trace("si-prt") << "...ground single invocation : success." << std::endl;
@@ -984,6 +988,9 @@ void SingleInvocationPartition::process( Node n ) {
         d_conjuncts[0].push_back( cr );
       }else{
         d_conjuncts[1].push_back( cr );
+        if( ngroundSingleInvocation ){
+          d_conjuncts[3].push_back( cr );
+        }
       }
     }
   }else{
@@ -1026,7 +1033,7 @@ bool SingleInvocationPartition::processConjunct( Node n, std::map< Node, bool >&
         }
       }
       if( ret ){
-        if( n.getKind()==APPLY_UF ){
+        if( n.getKind()==d_checkKind ){
           if( std::find( terms.begin(), terms.end(), n )==terms.end() ){
             Node f = n.getOperator();
             //check if it matches the type requirement
@@ -1083,7 +1090,7 @@ bool SingleInvocationPartition::isAntiSkolemizableType( Node f ) {
         }
       }
       if( ret ){
-        Node t = NodeManager::currentNM()->mkNode( APPLY_UF, children );
+        Node t = NodeManager::currentNM()->mkNode( d_checkKind, children );
         d_func_inv[f] = t;
         d_inv_to_func[t] = f;
         std::stringstream ss;
@@ -1117,7 +1124,7 @@ Node SingleInvocationPartition::getSpecificationInst( Node n, std::map< Node, No
       childChanged = childChanged || ( nn!=n[i] );
     }
     Node ret;
-    if( n.getKind()==APPLY_UF ){
+    if( n.getKind()==d_checkKind ){
       std::map< Node, Node >::iterator itl = lam.find( n.getOperator() );
       if( itl!=lam.end() ){
         Assert( itl->second[0].getNumChildren()==children.size() );
@@ -1214,8 +1221,8 @@ void SingleInvocationPartition::debugPrint( const char * c ) {
       Trace(c) << "not incorporated." << std::endl;
     }
   }
-  for( unsigned i=0; i<3; i++ ){
-    Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : "All" ) );
+  for( unsigned i=0; i<4; i++ ){
+    Trace(c) << ( i==0 ? "Single invocation" : ( i==1 ? "Non-single invocation" : ( i==2 ? "All" : "Non-ground single invocation" ) ) );
     Trace(c) << " conjuncts: " << std::endl;
     for( unsigned j=0; j<d_conjuncts[i].size(); j++ ){
       Trace(c) << "  " << (j+1) << " : " << d_conjuncts[i][j] << std::endl;
diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index fe48a0dc3..c25cf7633 100644
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -153,6 +153,8 @@ public:
 class SingleInvocationPartition
 {
 private:
+  //options
+  Kind d_checkKind;
   bool inferArgTypes( Node n, std::vector< TypeNode >& typs, std::map< Node, bool >& visited );
   void process( Node n );
   bool collectConjuncts( Node n, bool pol, std::vector< Node >& conj );
@@ -161,6 +163,8 @@ private:
   Node getSpecificationInst( Node n, std::map< Node, Node >& lam, std::map< Node, Node >& visited );
   void extractInvariant2( Node n, Node& func, int& pol, std::vector< Node >& disjuncts, bool hasPol, std::map< Node, bool >& visited );
 public:
+  SingleInvocationPartition( Kind checkKind = kind::APPLY_UF ) : d_checkKind( checkKind ){}
+  ~SingleInvocationPartition(){}
   bool init( Node n );
   bool init( std::vector< TypeNode >& typs, Node n );
 
@@ -174,8 +178,8 @@ public:
   std::vector< Node > d_func_vars; //the first-order variables corresponding to all functions
   std::vector< Node > d_si_vars;   //the arguments that we based the anti-skolemization on
   std::vector< Node > d_all_vars;  //every free variable of conjuncts[2]
-  // si, nsi, all
-  std::vector< Node > d_conjuncts[3];
+  // si, nsi, all, non-ground si
+  std::vector< Node > d_conjuncts[4];
 
   bool isAntiSkolemizableType( Node f );
 
@@ -189,6 +193,7 @@ public:
   void extractInvariant( Node n, Node& func, int& pol, std::vector< Node >& disjuncts );
 
   bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); }
+  bool isNonGroundSingleInvocation() { return d_conjuncts[3].size()==d_conjuncts[1].size(); }
 
   void debugPrint( const char * c );
 };
diff --git a/src/theory/quantifiers/quant_equality_engine.cpp b/src/theory/quantifiers/quant_equality_engine.cpp
index 54a931196..06ca6f98c 100644
--- a/src/theory/quantifiers/quant_equality_engine.cpp
+++ b/src/theory/quantifiers/quant_equality_engine.cpp
@@ -32,6 +32,7 @@ d_conflict(c, false),
 d_quant_red(c),
 d_quant_unproc(c){
   d_uequalityEngine.addFunctionKind( kind::APPLY_UF );
+  d_intType = NodeManager::currentNM()->integerType();
 }
 
 void QuantEqualityEngine::conflict(TNode t1, TNode t2) {
@@ -86,56 +87,130 @@ void QuantEqualityEngine::registerQuantifier( Node q ) {
 void QuantEqualityEngine::assertNode( Node n ) {
   Assert( n.getKind()==FORALL );
   Trace("qee-debug") << "QEE assert : " << n << std::endl;
-  Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
-  bool pol = n[1].getKind()!=NOT;
-  if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL ){
-    lit = getTermDatabase()->getCanonicalTerm( lit );
-    Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
-    Node t1 = lit.getKind()==APPLY_UF ? lit : lit[0];
+  if( !d_conflict ){
+    Node lit = n[1].getKind()==NOT ? n[1][0] : n[1];
+    bool pol = n[1].getKind()!=NOT;
+    bool success = true;
+    Node t1;
     Node t2;
-    if( lit.getKind()==APPLY_UF ){
-      t2 = pol ? getTermDatabase()->d_true : getTermDatabase()->d_false;
-      pol = true;
+    if( lit.getKind()==APPLY_UF || lit.getKind()==EQUAL || lit.getKind()==IFF ){
+      lit = getTermDatabase()->getCanonicalTerm( lit );
+      Trace("qee-debug") << "Canonical :  " << lit << ", pol = " << pol << std::endl;
+      if( lit.getKind()==APPLY_UF ){
+        t1 = getFunctionAppForPredicateApp( lit );
+        t2 = pol ? getTermDatabase()->d_one : getTermDatabase()->d_zero;
+        pol = true;
+        lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
+      }else if( lit.getKind()==EQUAL ){
+        t1 = lit[0];
+        t2 = lit[1];
+      }else if( lit.getKind()==IFF ){
+        if( lit[0].getKind()==NOT ){
+          t1 = lit[0][0];
+          pol = !pol;
+        }else{
+          t1 = lit[0];
+        }
+        if( lit[1].getKind()==NOT ){
+          t2 = lit[1][0];
+          pol = !pol;
+        }else{
+          t2 = lit[1];
+        }
+        if( t1.getKind()==APPLY_UF && t2.getKind()==APPLY_UF ){
+          t1 = getFunctionAppForPredicateApp( t1 );
+          t2 = getFunctionAppForPredicateApp( t2 );
+          lit = NodeManager::currentNM()->mkNode( EQUAL, t1, t2 );
+        }else{
+          success = false;
+        }
+      }
     }else{
-      t2 = lit[1];
-    }
-    bool alreadyHolds = false;
-    if( pol && areUnivEqual( t1, t2 ) ){
-      alreadyHolds = true;
-    }else if( !pol && areUnivDisequal( t1, t2 ) ){
-      alreadyHolds = true;
+      success = false;
     }
+    if( success ){
+      bool alreadyHolds = false;
+      if( pol && areUnivEqualInternal( t1, t2 ) ){
+        alreadyHolds = true;
+      }else if( !pol && areUnivDisequalInternal( t1, t2 ) ){
+        alreadyHolds = true;
+      }
 
-    if( alreadyHolds ){
-      d_quant_red.push_back( n );
-      Trace("qee-debug") << "...add to redundant" << std::endl;
-    }else{
-      Trace("qee-debug") << "...assert" << std::endl;
-      Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
-      if( lit.getKind()==APPLY_UF ){
-        d_uequalityEngine.assertPredicate(lit, pol, n);
+      if( alreadyHolds ){
+        d_quant_red.push_back( n );
+        Trace("qee-debug") << "...add to redundant" << std::endl;
       }else{
-        d_uequalityEngine.assertEquality(lit, pol, n);
+        Trace("qee-debug") << "...assert" << std::endl;
+        Trace("qee-assert") << "QEE : assert : " << lit << ", pol = " << pol << ", kind = " << lit.getKind() << std::endl;
+        if( lit.getKind()==APPLY_UF ){
+          d_uequalityEngine.assertPredicate(lit, pol, n);
+        }else{
+          d_uequalityEngine.assertEquality(lit, pol, n);
+        }
       }
+    }else{
+      d_quant_unproc[n] = true;
+      Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
     }
-  }else{
-    d_quant_unproc[n] = true;
-    Trace("qee-debug") << "...add to unprocessed (" << lit.getKind() << ")" << std::endl;
   }
 }
 
-bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
+bool QuantEqualityEngine::areUnivDisequalInternal( TNode n1, TNode n2 ) {
   return n1!=n2 && d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areDisequal( n1, n2, false );
 }
 
-bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
+bool QuantEqualityEngine::areUnivEqualInternal( TNode n1, TNode n2 ) {
   return n1==n2 || ( d_uequalityEngine.hasTerm( n1 ) && d_uequalityEngine.hasTerm( n2 ) && d_uequalityEngine.areEqual( n1, n2 ) );
 }
 
-TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
+TNode QuantEqualityEngine::getUnivRepresentativeInternal( TNode n ) {
   if( d_uequalityEngine.hasTerm( n ) ){
     return d_uequalityEngine.getRepresentative( n );
   }else{
     return n;
   }
-}
\ No newline at end of file
+}
+bool QuantEqualityEngine::areUnivDisequal( TNode n1, TNode n2 ) {
+  //TODO: must convert to internal representation
+  return areUnivDisequalInternal( n1, n2 );
+}
+
+bool QuantEqualityEngine::areUnivEqual( TNode n1, TNode n2 ) {
+  //TODO: must convert to internal representation
+  return areUnivEqualInternal( n1, n2 );
+}
+
+TNode QuantEqualityEngine::getUnivRepresentative( TNode n ) {
+  //TODO: must convert to internal representation
+  return getUnivRepresentativeInternal( n );
+}
+
+Node QuantEqualityEngine::getFunctionForPredicate( Node f ) {
+  std::map< Node, Node >::iterator it = d_pred_to_func.find( f );
+  if( it==d_pred_to_func.end() ){
+    std::vector< TypeNode > argTypes;
+    TypeNode tn = f.getType();
+    for( unsigned i=0; i<(tn.getNumChildren()-1); i++ ){
+      argTypes.push_back( tn[i] );
+    }
+    TypeNode ftn = NodeManager::currentNM()->mkFunctionType( argTypes, d_intType  );
+    std::stringstream ss;
+    ss << "ee_" << f;
+    Node op = NodeManager::currentNM()->mkSkolem( ss.str(), ftn, "op created for internal ee" );
+    d_pred_to_func[f] = op;
+    return op;
+  }else{
+    return it->second;
+  }
+}
+
+Node QuantEqualityEngine::getFunctionAppForPredicateApp( Node n ) {
+  Assert( n.getKind()==APPLY_UF );
+  std::vector< Node > children;
+  children.push_back( getFunctionForPredicate( n.getOperator() ) );
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    children.push_back( n[i] );
+  }
+  return NodeManager::currentNM()->mkNode( APPLY_UF, children );
+}
+
diff --git a/src/theory/quantifiers/quant_equality_engine.h b/src/theory/quantifiers/quant_equality_engine.h
index 35a328147..f3d8db8aa 100644
--- a/src/theory/quantifiers/quant_equality_engine.h
+++ b/src/theory/quantifiers/quant_equality_engine.h
@@ -56,12 +56,21 @@ private:
   context::CDList<Node> d_quant_red;
   /** unprocessed quantifiers in current context */
   NodeBoolMap d_quant_unproc;
+  // map predicates to functions over int
+  TypeNode d_intType;
+  std::map< Node, Node > d_pred_to_func;
+  Node getFunctionForPredicate( Node f );
+  Node getFunctionAppForPredicateApp( Node n );
 private:
   void conflict(TNode t1, TNode t2);
   void eqNotifyNewClass(TNode t);
   void eqNotifyPreMerge(TNode t1, TNode t2);
   void eqNotifyPostMerge(TNode t1, TNode t2);
   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+  //queries
+  bool areUnivDisequalInternal( TNode n1, TNode n2 );
+  bool areUnivEqualInternal( TNode n1, TNode n2 );  
+  TNode getUnivRepresentativeInternal( TNode n );
 public:
   QuantEqualityEngine( QuantifiersEngine * qe, context::Context* c );
   virtual ~QuantEqualityEngine() throw (){}