Handle missing cases for single inv solution reconstruction. Minor fixes. Refactor.

diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index 3fa27e47450cea126e8cc3f4e8702c98c34e400e..902e745ea96e187aaa9491d4e0ec87f79ade42d6 100644 (file)
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -709,6 +709,9 @@ sygusGTerm[std::string& fun, std::vector<CVC4::Expr>& ops, std::vector<std::stri
   : LPAREN_TOK
     ( builtinOp[k]
       { Debug("parser-sygus") << "Sygus grammar " << fun << " : builtin op : " << name << std::endl;
+        if( k==CVC4::kind::BITVECTOR_UDIV ){
+          k = CVC4::kind::BITVECTOR_UDIV_TOTAL;
+        }
         ops.push_back(EXPR_MANAGER->operatorOf(k));
         name = kind::kindToString(k);
       }

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index 3475e9e97afd437b57fd549272f976a4b34c6c7c..e291dce9d260f9ece098fbb9d4a87033290e8ae1 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -60,7 +60,7 @@ void CegConjecture::assign( QuantifiersEngine * qe, Node q ) {
     }
     d_syntax_guided = true;
     if( options::cegqiSingleInv() ){
-      d_ceg_si = new CegConjectureSingleInv( q, this );
+      d_ceg_si = new CegConjectureSingleInv( qe, q, this );
       d_ceg_si->initialize();
     }
   }else if( qe->getTermDatabase()->isQAttrSynthesis( q ) ){
@@ -255,7 +255,7 @@ void CegInstantiation::checkCegConjecture( CegConjecture * conj ) {
     if( getTermDatabase()->isQAttrSygus( q ) ){
       if( conj->d_ceg_si ){
         std::vector< Node > lems;
-        conj->d_ceg_si->check( d_quantEngine, lems );
+        conj->d_ceg_si->check( lems );
         if( !lems.empty() ){
           d_last_inst_si = true;
           for( unsigned j=0; j<lems.size(); j++ ){
@@ -494,7 +494,7 @@ void CegInstantiation::printSynthSolution( std::ostream& out ) {
       int status;
       if( d_last_inst_si ){
         Assert( d_conj->d_ceg_si );
-        sol = d_conj->d_ceg_si->getSolution( d_quantEngine, i, tn, status );
+        sol = d_conj->d_ceg_si->getSolution( i, tn, status );
       }else{
         if( !d_conj->d_candidate_inst[i].empty() ){
           sol = d_conj->d_candidate_inst[i].back();

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index 1dd60e583f697418ae792b5aa1508745a1ff9ada..51cce2407d38a3009bbf7f0c29305bcb04d7784f 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -22,6 +22,7 @@
 #include "theory/datatypes/datatypes_rewriter.h"
 #include "util/datatype.h"
 #include "theory/quantifiers/quant_util.h"
+#include "theory/quantifiers/trigger.h"
 
 using namespace CVC4;
 using namespace CVC4::kind;
@@ -44,7 +45,7 @@ Node simpleNegate( Node n ){
 }
 
 
-CegConjectureSingleInv::CegConjectureSingleInv( Node q, CegConjecture * p ) : d_parent( p ), d_quant( q ){
+CegConjectureSingleInv::CegConjectureSingleInv( QuantifiersEngine * d_qe, Node q, CegConjecture * p ) : d_qe( d_qe ), d_parent( p ), d_quant( q ){
 
 }
 
@@ -271,6 +272,19 @@ void CegConjectureSingleInv::initialize() {
           Node bd = conjuncts.size()==1 ? conjuncts[0] : NodeManager::currentNM()->mkNode( OR, conjuncts );
           d_single_inv = NodeManager::currentNM()->mkNode( FORALL, pbvl, bd );
           Trace("cegqi-si-debug") << "...formula is : " << d_single_inv << std::endl;
+          if( options::eMatching.wasSetByUser() ){
+            Node bd = d_qe->getTermDatabase()->getInstConstantBody( d_single_inv );
+            std::vector< Node > patTerms;
+            std::vector< Node > exclude;
+            inst::Trigger::collectPatTerms( d_qe, d_single_inv, bd, patTerms, inst::Trigger::TS_ALL, exclude );
+            if( !patTerms.empty() ){
+              Trace("cegqi-si-em") << "Triggers : " << std::endl;
+              for( unsigned i=0; i<patTerms.size(); i++ ){
+                Trace("cegqi-si-em") << "   " << patTerms[i] << std::endl;
+              }
+            }
+          }
+
           /*
           //equality resolution
           for( unsigned j=0; j<conjuncts.size(); j++ ){
@@ -447,9 +461,9 @@ bool CegConjectureSingleInv::analyzeSygusTerm( Node n, std::map< Node, std::vect
 }
 
 
-void CegConjectureSingleInv::check( QuantifiersEngine * qe, std::vector< Node >& lems ) {
+void CegConjectureSingleInv::check( std::vector< Node >& lems ) {
   if( !d_single_inv.isNull() ) {
-    eq::EqualityEngine* ee = qe->getMasterEqualityEngine();
+    eq::EqualityEngine* ee = d_qe->getMasterEqualityEngine();
     Trace("cegqi-engine") << "  * single invocation: " << std::endl;
     std::vector< Node > subs;
     std::map< Node, int > subs_from_model;
@@ -500,7 +514,7 @@ void CegConjectureSingleInv::check( QuantifiersEngine * qe, std::vector< Node >&
       }
       if( slv.isNull() ){
         //get model value
-        Node mv = qe->getModel()->getValue( pv );
+        Node mv = d_qe->getModel()->getValue( pv );
         subs.push_back( mv );
         subs_from_model[pv] = i;
         if( Trace.isOn("cegqi-engine") || Trace.isOn("cegqi-engine-debug") ){
@@ -682,7 +696,7 @@ Node CegConjectureSingleInv::constructSolution( unsigned i, unsigned index ) {
   }
 }
 
-Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed ){
+Node CegConjectureSingleInv::getSolution( unsigned i, TypeNode stn, int& reconstructed ){
   Assert( !d_lemmas_produced.empty() );
   Node s = constructSolution( i, 0 );
   const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
@@ -702,6 +716,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Ty
       vars.push_back( prog_app[i] );
     }
     subs.push_back( varList[i-1] );
+    d_varlist.push_back( varList[i-1] );
   }
   s = s.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() );
   d_orig_solution = s;
@@ -715,7 +730,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Ty
   std::vector< Node > svars;
   std::vector< Node > ssubs;
   Trace("cegqi-si-debug-sol") << "Solution (pre-simplification): " << s << std::endl;
-  s = simplifySolution( qe, s, sassign, svars, ssubs, subs, 0 );
+  s = simplifySolution( s, sassign, svars, ssubs, subs, 0 );
   Trace("cegqi-si-debug-sol") << "Solution (post-simplification): " << s << std::endl;
   s = Rewriter::rewrite( s );
   Trace("cegqi-si-debug-sol") << "Solution (post-rewrite): " << s << std::endl;
@@ -723,7 +738,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Ty
   reconstructed = 0;
   if( options::cegqiSingleInvReconstruct() && !stn.isNull() ){
     int status;
-    d_templ_solution = collectReconstructNodes( qe->getTermDatabaseSygus(), d_solution, stn, status );
+    d_templ_solution = collectReconstructNodes( d_qe->getTermDatabaseSygus(), d_solution, stn, status );
     if( status==1 ){
       setNeedsReconstruction( d_templ_solution, stn, Node::null(), TypeNode::null() );
     }
@@ -752,13 +767,13 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Ty
         if( it->second.empty() ){
           to_erase.push_back( stn );
         }else{
-          Node ns = qe->getTermDatabase()->getEnumerateTerm( stn, index );
+          Node ns = d_qe->getTermDatabase()->getEnumerateTerm( stn, index );
           if( ns.isNull() ){
             to_erase.push_back( stn );
             incomplete.push_back( stn );
           }else{
-            Node nb = qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn );
-            Node nr = Rewriter::rewrite( nb );//qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false );
+            Node nb = d_qe->getTermDatabaseSygus()->sygusToBuiltin( ns, stn );
+            Node nr = Rewriter::rewrite( nb );//d_qe->getTermDatabaseSygus()->getNormalized( stn, nb, false, false );
             Trace("cegqi-si-rcons-debug2") << "  - try " << ns << " -> " << nr << " for " << stn << " " << nr.getKind() << std::endl;
             if( it->second.find( nr )!=it->second.end() ){
               Trace("cegqi-si-rcons") << "...reconstructed " << ns << " for term " << nr << std::endl;
@@ -777,7 +792,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Ty
                 Trace("cegqi-si-rcons") << " as " << itk->second.size() << " waiting terms." << std::endl;
                 Assert( !itk->second.empty() );
                 for( std::map< Node, bool >::iterator itkn = itk->second.begin(); itkn != itk->second.end(); ++itkn ){
-                  
+
                 }
               }
               */
@@ -798,7 +813,7 @@ Node CegConjectureSingleInv::getSolution( QuantifiersEngine * qe, unsigned i, Ty
         if( incomplete.empty() ){
           reconstructed = 1;
           Trace("cegqi-si-debug-sol") << "Reconstructing sygus solution..." << std::endl;
-          d_sygus_solution = getReconstructedSolution( qe->getTermDatabaseSygus(), stn, d_templ_solution );
+          d_sygus_solution = getReconstructedSolution( d_qe->getTermDatabaseSygus(), stn, d_templ_solution );
           Trace("cegqi-si-debug-sol") << "Sygus solution is : " << d_sygus_solution << std::endl;
         }
       }
@@ -1032,33 +1047,34 @@ Node CegConjectureSingleInv::flattenITEs( Node n, bool rec ) {
 // assign is from literals to booleans
 // union_find is from args to values
 
-bool CegConjectureSingleInv::getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars,
+bool CegConjectureSingleInv::getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign, std::vector< Node >& vars,
                                         std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ) {
   std::map< Node, bool >::iterator ita = assign.find( n );
   if( ita!=assign.end() ){
     Trace("csi-simp-debug") << "---already assigned, lookup " << pol << " " << ita->second << std::endl;
     return pol==ita->second;
+  }else if( n.isConst() ){
+    return pol==(n==d_qe->getTermDatabase()->d_true);
   }else{
     Trace("csi-simp-debug") << "---assign " << n << " " << pol << std::endl;
     assign[n] = pol;
     new_assign.push_back( n );
     if( ( pol && n.getKind()==AND ) || ( !pol && n.getKind()==OR ) ){
       for( unsigned i=0; i<n.getNumChildren(); i++ ){
-        if( !getAssign( qe, pol, n[i], assign, new_assign, vars, new_vars, new_subs, args ) ){
+        if( !getAssign( pol, n[i], assign, new_assign, vars, new_vars, new_subs, args ) ){
           return false;
         }
       }
     }else if( n.getKind()==NOT ){
-      return getAssign( qe, !pol, n[0], assign, new_assign, vars, new_vars, new_subs, args );
+      return getAssign( !pol, n[0], assign, new_assign, vars, new_vars, new_subs, args );
     }else if( pol && ( n.getKind()==IFF || n.getKind()==EQUAL ) ){
-      getAssignEquality( qe, n, vars, new_vars, new_subs, args );
+      getAssignEquality( n, vars, new_vars, new_subs, args );
     }
   }
   return true;
 }
 
-bool CegConjectureSingleInv::getAssignEquality( QuantifiersEngine * qe, Node eq,
-                                                std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ) {
+bool CegConjectureSingleInv::getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args ) {
   Assert( eq.getKind()==IFF || eq.getKind()==EQUAL );
   //try to find valid argument
   for( unsigned r=0; r<2; r++ ){
@@ -1066,7 +1082,7 @@ bool CegConjectureSingleInv::getAssignEquality( QuantifiersEngine * qe, Node eq,
       Assert( std::find( vars.begin(), vars.end(), eq[r] )==vars.end() );
       if( std::find( new_vars.begin(), new_vars.end(), eq[r] )==new_vars.end() ){
         Node eqro = eq[r==0 ? 1 : 0 ];
-        if( !qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){
+        if( !d_qe->getTermDatabase()->containsTerm( eqro, eq[r] ) ){
           Trace("csi-simp-debug") << "---equality " << eq[r] << " = " << eqro << std::endl;
           new_vars.push_back( eq[r] );
           new_subs.push_back( eqro );
@@ -1087,7 +1103,7 @@ bool CegConjectureSingleInv::getAssignEquality( QuantifiersEngine * qe, Node eq,
   return false;
 }
 
-Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign,
+Node CegConjectureSingleInv::simplifySolution( Node sol, std::map< Node, bool >& assign,
                                                std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status ) {
   Assert( vars.size()==subs.size() );
   std::map< Node, bool >::iterator ita = assign.find( sol );
@@ -1101,7 +1117,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
         std::vector< Node > new_assign;
         std::vector< Node > new_vars;
         std::vector< Node > new_subs;
-        if( getAssign( qe, r==1, sol[0], assign, new_assign, vars, new_vars, new_subs, args ) ){
+        if( getAssign( r==1, sol[0], assign, new_assign, vars, new_vars, new_subs, args ) ){
           Trace("csi-simp") << "- branch " << r << " led to " << new_assign.size() << " assignments, " << new_vars.size() << " equalities." << std::endl;
           unsigned prev_size = vars.size();
           Node nc = sol[r];
@@ -1110,7 +1126,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
             vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
             subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
           }
-          nc = simplifySolution( qe, nc, assign, vars, subs, args, 0 );
+          nc = simplifySolution( nc, assign, vars, subs, args, 0 );
           children.push_back( nc );
           //clean up substitution
           if( !new_vars.empty() ){
@@ -1129,7 +1145,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
         return children[0];
       }else{
         Assert( children.size()==2 );
-        Node ncond = simplifySolution( qe, sol[0], assign, vars, subs, args, 0 );
+        Node ncond = simplifySolution( sol[0], assign, vars, subs, args, 0 );
         return NodeManager::currentNM()->mkNode( ITE, ncond, children[0], children[1] );
       }
     }else if( sol.getKind()==OR || sol.getKind()==AND ){
@@ -1140,7 +1156,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
       std::vector< Node > children;
       std::vector< Node > new_vars;
       std::vector< Node > new_subs;
-      Node bc = sol.getKind()==OR ? qe->getTermDatabase()->d_true : qe->getTermDatabase()->d_false;
+      Node bc = sol.getKind()==OR ? d_qe->getTermDatabase()->d_true : d_qe->getTermDatabase()->d_false;
       for( unsigned i=0; i<sol.getNumChildren(); i++ ){
         bool do_exc = false;
         Node c = sol[i];
@@ -1161,7 +1177,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
             if( status==0 && ( atom.getKind()==IFF || atom.getKind()==EQUAL ) ){
               if( pol==( sol.getKind()==AND ) ){
                 Trace("csi-simp") << "  ...equality." << std::endl;
-                if( getAssignEquality( qe, atom, vars, new_vars, new_subs, args ) ){
+                if( getAssignEquality( atom, vars, new_vars, new_subs, args ) ){
                   children.push_back( sol[i] );
                   do_exc = true;
                 }
@@ -1193,7 +1209,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
           unsigned prev_size = vars.size();
           vars.insert( vars.end(), new_vars.begin(), new_vars.end() );
           subs.insert( subs.end(), new_subs.begin(), new_subs.end() );
-          ret = simplifySolution( qe, ret, assign, vars, subs, args, 1 );
+          ret = simplifySolution( ret, assign, vars, subs, args, 1 );
           //clean up substitution
           if( !vars.empty() ){
             vars.resize( prev_size );
@@ -1211,7 +1227,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
       }else{
         //recurse on children
         for( unsigned i=0; i<inc.size(); i++ ){
-          Node retc = simplifySolution( qe, inc[i], assign, vars, subs, args, 0 );
+          Node retc = simplifySolution( inc[i], assign, vars, subs, args, 0 );
           if( retc.isConst() ){
             if( retc==bc ){
               return bc;
@@ -1231,13 +1247,13 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
           if( pol!=( sol.getKind()==AND ) ){
             std::vector< Node > tmp_vars;
             std::vector< Node > tmp_subs;
-            if( getAssignEquality( qe, atom, vars, tmp_vars, tmp_subs, args ) ){
+            if( getAssignEquality( atom, vars, tmp_vars, tmp_subs, args ) ){
               Trace("csi-simp-debug") << "Check if " << children[i] << " is redundant in " << sol << std::endl;
               for( unsigned j=0; j<children.size(); j++ ){
                 if( j!=i && ( j>i || std::find( final_children.begin(), final_children.end(), children[j] )!=final_children.end() ) ){
                   Node sj = children[j].substitute( tmp_vars.begin(), tmp_vars.end(), tmp_subs.begin(), tmp_subs.end() );
                   sj = Rewriter::rewrite( sj );
-                  if( sj==qe->getTermDatabase()->d_true ){
+                  if( sj==d_qe->getTermDatabase()->d_true ){
                     Trace("csi-simp") << "--- " << children[i].negate() << " is implied by " << children[j].negate() << std::endl;
                     red = true;
                     break;
@@ -1251,8 +1267,8 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
           final_children.push_back( children[i] );
         }
       }
-      
-      return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) : 
+
+      return final_children.size()==0 ? NodeManager::currentNM()->mkConst( sol.getKind()==AND ) :
              ( final_children.size()==1 ? final_children[0] : NodeManager::currentNM()->mkNode( sol.getKind(), final_children ) );
     }else{
       //generic simplification
@@ -1262,7 +1278,7 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
       }
       bool childChanged = false;
       for( unsigned i=0; i<sol.getNumChildren(); i++ ){
-        Node nc = simplifySolution( qe, sol[i], assign, vars, subs, args, 0 );
+        Node nc = simplifySolution( sol[i], assign, vars, subs, args, 0 );
         childChanged = childChanged || nc!=sol[i];
         children.push_back( nc );
       }
@@ -1274,24 +1290,15 @@ Node CegConjectureSingleInv::simplifySolution( QuantifiersEngine * qe, Node sol,
   }
 }
 
+//TODO : accumulate assignment to literals as we traverse ITE
 Node CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, int& status ) {
-  /*
-  if( ignoreBoolean && t.getType().isBoolean() ){
-    if( t.getKind()==OR || t.getKind()==AND || t.getKind()==IFF || t.getKind()==ITE || t.getKind()==NOT ){ //FIXME
-      for( unsigned i=0; i<t.getNumChildren(); i++ ){
-        collectReconstructNodes( tds, t[i], stn, parent, pstn, ignoreBoolean );
-      }
-      return;
-    }
-  }
-  */
   std::map< TypeNode, Node >::iterator it = d_rcons_processed[t].find( stn );
   if( it==d_rcons_processed[t].end() ){
     TypeNode tn = t.getType();
     Assert( datatypes::DatatypesRewriter::isTypeDatatype( stn ) );
     const Datatype& dt = ((DatatypeType)(stn).toType()).getDatatype();
     Assert( dt.isSygus() );
-    Trace("cegqi-si-rcons-debug") << "Check reconstruct " << t << " type " << tn << ", sygus type " << dt.getName() << std::endl;
+    Trace("cegqi-si-rcons-debug") << "Check reconstruct " << t << " type " << tn << ", sygus type " << dt.getName() << ", kind " << t.getKind() << std::endl;
     tds->registerSygusType( stn );
     Node ret;
     std::vector< Node > children;
@@ -1308,57 +1315,91 @@ Node CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t,
     int karg = tds->getKindArg( stn, tk );
     //preprocessing to fit syntax
     Node orig_t = t;
-    if( karg==-1 && t.getNumChildren()>0 ){
-      Node new_t;
-      Kind dk;
-      if( tds->isAntisymmetric( tk, dk ) ){
-        if( tds->hasKind( stn, dk ) ){
-          new_t = NodeManager::currentNM()->mkNode( dk, t[1], t[0] );
+    if( t.getNumChildren()>0 ){
+      // first, do standard minimizations
+      t = tds->minimizeBuiltinTerm( t );
+      bool success = true;
+      while( karg==-1 && success ){
+        success = false;
+        Node new_t;
+        Kind dk;
+        if( tds->isAntisymmetric( tk, dk ) ){
+          if( tds->hasKind( stn, dk ) ){
+            new_t = NodeManager::currentNM()->mkNode( dk, t[1], t[0] );
+          }
         }
-      }
-      if( new_t.isNull() ){
-        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
-          Node g = tds->getGenericBase( stn, i );
-          if( g.getKind()==t.getKind() ){
-            Trace("cegqi-si-rcons-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl;
-            std::map< int, Node > sigma;
-            if( tds->getMatch( g, t, sigma ) ){
-              //we found an exact match
-              bool success = true;
-              for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
-                if( sigma[j].isNull() ){
-                  success = false;
+        if( new_t.isNull() ){
+          for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
+            Node g = tds->getGenericBase( stn, i );
+            if( g.getKind()==t.getKind() ){
+              Trace("cegqi-si-rcons-debug") << "Possible match ? " << g << " " << t << " for " << dt[i].getName() << std::endl;
+              std::map< int, Node > sigma;
+              if( tds->getMatch( g, t, sigma ) ){
+                //we found an exact match
+                bool msuccess = true;
+                for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
+                  if( sigma[j].isNull() ){
+                    msuccess = false;
+                    break;
+                  }
+                }
+                if( msuccess ){
+                  std::map< TypeNode, int > var_count;
+                  new_t = tds->mkGeneric( dt, i, var_count, sigma );
+                  Trace("cegqi-si-rcons-debug") << "Rewrote to : " << new_t << std::endl;
                   break;
                 }
               }
-              if( success ){
-                std::map< TypeNode, int > var_count;
-                new_t = tds->mkGeneric( dt, i, var_count, sigma );
-                Trace("cegqi-si-rcons-debug") << "Rewrote to : " << new_t << std::endl;
-                break;
-              }
+            }
+          }
+          //expand things that have compact representations (these will not be found by enumeration if they aren't already in the syntax)
+          if( new_t.isNull() ){
+            if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){
+              new_t = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
+                                                            NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
+            }else if( t.getKind()==ITE ){
+              new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
+                                                            NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
+            }else if( t.getKind()==IFF ){
+              new_t = NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
+                                                            NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
+            }else if( ( t.getKind()==OR || t.getKind()==AND ) && tds->hasKind( stn, NOT ) ){
+              new_t = simpleNegate( t ).negate();
             }
           }
         }
+        if( !new_t.isNull() ){
+          t = new_t;
+          karg = tds->getKindArg( stn, t.getKind() );
+          success = true;
+          Trace("cegqi-si-rcons-debug") << "Try rewriting to " << new_t << ", now karg=" << karg << std::endl;
+        }
       }
-      if( !new_t.isNull() ){
-        t = new_t;
-      }
-    }else{
+    }
+    if( karg!=-1 ){
       //flatten ITEs if necessary
       if( t.getKind()==ITE ){
         TypeNode cstn = tds->getArgType( dt[karg], 0 );
         tds->registerSygusType( cstn );
-        if( !tds->hasKind( cstn, t[0].getKind() ) ){
+        Node prev_t;
+        while( !tds->hasKind( cstn, t[0].getKind() ) && t!=prev_t ){
+          prev_t = t;
+          Node exp_c = tds->expandBuiltinTerm( t[0] );
+          if( !exp_c.isNull() ){
+            t = NodeManager::currentNM()->mkNode( ITE, exp_c, t[1], t[2] );
+            Trace("cegqi-si-rcons-debug") << "Pre expand to " << t << std::endl;
+          }
           t = flattenITEs( t, false );
+          if( t!=prev_t ){
+            Trace("cegqi-si-rcons-debug") << "Flatten ITE to " << t << std::endl;
+            std::map< Node, bool > sassign;
+            std::vector< Node > svars;
+            std::vector< Node > ssubs;
+            t = simplifySolution( t, sassign, svars, ssubs, d_varlist, 0 );
+          }
           Assert( t.getKind()==ITE );
         }
       }
-    }
-    if( t!=orig_t ){
-      karg = tds->getKindArg( stn, t.getKind() );
-    }
-    if( karg!=-1 ){
       if( t.getNumChildren()==dt[karg].getNumArgs() ){
         Trace("cegqi-si-rcons-debug") << "  Type has kind " << t.getKind() << ", recurse." << std::endl;
         for( unsigned i=0; i<t.getNumChildren(); i++ ){
@@ -1426,7 +1467,6 @@ Node CegConjectureSingleInv::collectReconstructNodes( TermDbSygus * tds, Node t,
       if( !childChanged ){
         ret = t;
       }else{
-        Trace("cegqi-si-rcons-debug") << "Make return node " << t.getKind() << " with " << children.size() << " children." << std::endl;
         ret = NodeManager::currentNM()->mkNode( t.getKind(), children );
       }
     }

diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 44a8ed6e44a5c407e66f072eb3a9aeb85a326607..85ba25a0fa6b2e7e63a285846505c5fde06e28a2 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -30,6 +30,7 @@ class CegConjecture;
 class CegConjectureSingleInv
 {
 private:
+  QuantifiersEngine * d_qe;
   CegConjecture * d_parent;
   bool analyzeSygusConjunct( Node n, Node p, std::map< Node, std::vector< Node > >& children,
                             std::map< Node, std::map< Node, std::vector< Node > > >& prog_invoke,
@@ -45,7 +46,7 @@ private:
   Node applyProgVarSubstitution( Node n, std::map< Node, int >& subs_from_model, std::vector< Node >& subs );
 
 public:
-  CegConjectureSingleInv( Node q, CegConjecture * p );
+  CegConjectureSingleInv( QuantifiersEngine * qe, Node q, CegConjecture * p );
   // original conjecture
   Node d_quant;
   // single invocation version of quant
@@ -66,6 +67,7 @@ public:
   std::vector< Node > d_lemmas_produced;
   std::vector< std::vector< Node > > d_inst;
   // solution
+  std::vector< Node > d_varlist;
   Node d_orig_solution;
   Node d_solution;
   Node d_templ_solution;
@@ -76,11 +78,11 @@ public:
   //initialize
   void initialize();
   //check
-  void check( QuantifiersEngine * qe, std::vector< Node >& lems );
+  void check( std::vector< Node >& lems );
   //get solution
-  Node getSolution( QuantifiersEngine * qe, unsigned i, TypeNode stn, int& reconstructed );
-  
-  
+  Node getSolution( unsigned i, TypeNode stn, int& reconstructed );
+
+
 //solution simplification
 private:
   bool debugSolution( Node sol );
@@ -88,11 +90,11 @@ private:
   Node pullITEs( Node n );
   bool pullITECondition( Node root, Node n, std::vector< Node >& conj, Node& t, Node& rem, int depth );
   Node flattenITEs( Node n, bool rec = true );
-  Node simplifySolution( QuantifiersEngine * qe, Node sol, std::map< Node, bool >& assign,
+  Node simplifySolution( Node sol, std::map< Node, bool >& assign,
                          std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& args, int status );
-  bool getAssign( QuantifiersEngine * qe, bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
+  bool getAssign( bool pol, Node n, std::map< Node, bool >& assign, std::vector< Node >& new_assign,
                   std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
-  bool getAssignEquality( QuantifiersEngine * qe, Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
+  bool getAssignEquality( Node eq, std::vector< Node >& vars, std::vector< Node >& new_vars, std::vector< Node >& new_subs, std::vector< Node >& args );
 //solution reconstruction
 private:
   std::map< Node, std::map< TypeNode, Node > > d_rcons_processed;
@@ -105,7 +107,7 @@ private:
   std::map< Node, Node > d_rcons_to_rewrite;
   // term t with sygus type st, returns inducted templated form of t
   Node collectReconstructNodes( TermDbSygus * tds, Node t, TypeNode stn, int& status );
-  // set reconstructed 
+  // set reconstructed
   void setNeedsReconstruction( Node t, TypeNode stn, Node parent, TypeNode pstn );
   void setReconstructed( Node tr, TypeNode stn );
   // get solution

diff --git a/src/theory/quantifiers/quant_util.cpp b/src/theory/quantifiers/quant_util.cpp
index 8d24c2cefe1ea63c397ee56affae7a641e22f2cf..ccc4cfd150a35ae131e46a94ab17f1b1eace41ff 100644 (file)
--- a/src/theory/quantifiers/quant_util.cpp
+++ b/src/theory/quantifiers/quant_util.cpp
@@ -23,7 +23,15 @@ using namespace CVC4::kind;
 using namespace CVC4::context;
 using namespace CVC4::theory;
 
-
+bool QuantArith::getMonomial( Node n, Node& c, Node& v ){
+  if( n.getKind()==MULT && n.getNumChildren()==2 && n[0].isConst() ){
+    c = n[0];
+    v = n[1];
+    return true;
+  }else{
+    return false;
+  }
+}
 bool QuantArith::getMonomial( Node n, std::map< Node, Node >& msum ) {
   if ( n.getKind()==MULT ){
     if( n.getNumChildren()==2 && msum.find(n[1])==msum.end() && n[0].isConst() ){

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 7c1ca24449ddd38fdae6039c0914c054636ee518..f0dfb1ed6e91d8378eec9333588f7a35ed393c7e 100644 (file)
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -32,6 +32,7 @@ class QuantifiersEngine;
 class QuantArith
 {
 public:
+  static bool getMonomial( Node n, Node& c, Node& v );
   static bool getMonomial( Node n, std::map< Node, Node >& msum );
   static bool getMonomialSum( Node n, std::map< Node, Node >& msum );
   static bool getMonomialSumLit( Node lit, std::map< Node, Node >& msum );

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index a7385f027d711d563bf4d4575c5f7df2b66bf3d7..cca2cb5e2b23220e527369bdc6a6a4e467b8b60d 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1362,7 +1362,7 @@ TypeNode TermDbSygus::getSygusType( Node v ) {
   return d_fv_stype[v];
 }
 
-bool TermDbSygus::getMatch( Node p, Node n, std::map< int, Node >& s ) { 
+bool TermDbSygus::getMatch( Node p, Node n, std::map< int, Node >& s ) {
   std::vector< int > new_s;
   return getMatch2( p, n, s, new_s );
 }
@@ -1397,7 +1397,7 @@ bool TermDbSygus::getMatch2( Node p, Node n, std::map< int, Node >& s, std::vect
       }
       if( success ){
         new_s.insert( new_s.end(), new_tmp.begin(), new_tmp.end() );
-        return true; 
+        return true;
       }
     }
   }
@@ -1866,3 +1866,54 @@ TypeNode TermDbSygus::getArgType( const DatatypeConstructor& c, int i ) {
   Assert( i>=0 && i<(int)c.getNumArgs() );
   return TypeNode::fromType( ((SelectorType)c[i].getType()).getRangeType() );
 }
+
+Node TermDbSygus::minimizeBuiltinTerm( Node n ) {
+  if( ( n.getKind()==EQUAL || n.getKind()==LEQ ) && ( n[0].getType().isInteger() || n[0].getType().isReal() ) ){
+    bool changed = false;
+    std::vector< Node > mon[2];
+    for( unsigned r=0; r<2; r++ ){
+      unsigned ro = r==0 ? 1 : 0;
+      Node c;
+      Node nc;
+      if( n[r].getKind()==PLUS ){
+        for( unsigned i=0; i<n[r].getNumChildren(); i++ ){
+          if( QuantArith::getMonomial( n[r][i], c, nc ) && c.getConst<Rational>().isNegativeOne() ){
+            mon[ro].push_back( nc );
+            changed = true;
+          }else{
+            mon[r].push_back( n[r][i] );
+          }
+        }
+      }else{
+        if( QuantArith::getMonomial( n[r], c, nc ) && c.getConst<Rational>().isNegativeOne() ){
+          mon[ro].push_back( nc );
+          changed = true;
+        }else{
+          mon[r].push_back( n[r] );
+        }
+      }
+    }
+    if( changed ){
+      Node nn[2];
+      for( unsigned r=0; r<2; r++ ){
+        nn[r] = mon[r].size()==0 ? NodeManager::currentNM()->mkConst( Rational(0) ) : ( mon[r].size()==1 ? mon[r][0] : NodeManager::currentNM()->mkNode( PLUS, mon[r] ) );
+      }
+      return NodeManager::currentNM()->mkNode( n.getKind(), nn[0], nn[1] );
+    }
+  }
+  return n;
+}
+
+Node TermDbSygus::expandBuiltinTerm( Node t ){
+  if( t.getKind()==EQUAL && ( t[0].getType().isInteger() || t[0].getType().isReal() ) ){
+    return NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( LEQ, t[0], t[1] ),
+                                                  NodeManager::currentNM()->mkNode( LEQ, t[1], t[0] ) );
+  }else if( t.getKind()==ITE ){
+    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
+                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[2] ) );
+  }else if( t.getKind()==IFF ){
+    return NodeManager::currentNM()->mkNode( OR, NodeManager::currentNM()->mkNode( AND, t[0], t[1] ),
+                                                  NodeManager::currentNM()->mkNode( AND, t[0].negate(), t[1].negate() ) );
+  }
+  return Node::null();
+}
\ No newline at end of file

diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h
index 5a3419ceed99d5c98e282855b661f9cbc7933cdb..1e457f8ec3487196ed8aa7fd152150e526f87bb7 100644 (file)
--- a/src/theory/quantifiers/term_database.h
+++ b/src/theory/quantifiers/term_database.h
@@ -325,7 +325,7 @@ private:
   TermDbSygus * d_sygus_tdb;
 public:
   TermDbSygus * getTermDatabaseSygus() { return d_sygus_tdb; }
-  
+
 private:
   std::map< Node, bool > d_fun_defs;
 public: //general queries concerning quantified formulas wrt modules
@@ -438,6 +438,10 @@ public:
   Node getSygusNormalized( Node n, std::map< TypeNode, int >& var_count, std::map< Node, Node >& subs );
   Node getNormalized( TypeNode t, Node prog, bool do_pre_norm = false, bool do_post_norm = true );
   int getTermSize( Node n );
+  /** given a term, construct an equivalent smaller one that respects syntax */
+  Node minimizeBuiltinTerm( Node n );
+  /** given a term, expand it into more basic components */
+  Node expandBuiltinTerm( Node n );
 };
 
 }/* CVC4::theory::quantifiers namespace */