Improvements to sygus, register equivalent terms based on rewrites of original conjec...

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 498b2ee12d00e8a72be4aa7f19d5aeb8c7136b78..1a9887e93d53f08f99dc4f9a28c4f16a4c67bb51 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -85,6 +85,7 @@
 #include "theory/quantifiers/macros.h"
 #include "theory/quantifiers/fun_def_process.h"
 #include "theory/quantifiers/quantifiers_rewriter.h"
+#include "theory/quantifiers/ce_guided_instantiation.h"
 #include "theory/quantifiers/options.h"
 #include "theory/datatypes/options.h"
 #include "theory/strings/theory_strings_preprocess.h"
@@ -3170,6 +3171,13 @@ void SmtEnginePrivate::processAssertions() {
 
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+  if( options::ceGuidedInst() ){
+    //register sygus conjecture pre-rewrite (motivated by solution reconstruction)
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_smt.d_theoryEngine->getQuantifiersEngine()->getCegInstantiation()->preregisterAssertion( d_assertions[i] );
+    }
+  }
+  
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
       !d_smt.d_logic.isPure(THEORY_BV)) {
     throw ModalException("Eager bit-blasting does not currently support theory combination. "

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f01efb5c4b2085319b8f2353b1f1bdf46456ea70..0bc5bb0087bdd0b3a29fed993447e3429e037d0b 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.cpp
+++ b/src/theory/quantifiers/ce_guided_instantiation.cpp
@@ -150,6 +150,10 @@ bool CegConjecture::needsCheck() {
   return d_active && !d_infeasible && ( !isSingleInvocation() || d_ceg_si->needsCheck() );
 }
 
+void CegConjecture::preregisterConjecture( Node q ) {
+  d_ceg_si->preregisterConjecture( q );
+}
+
 CegInstantiation::CegInstantiation( QuantifiersEngine * qe, context::Context* c ) : QuantifiersModule( qe ){
   d_conj = new CegConjecture( qe, qe->getSatContext() );
   d_last_inst_si = false;
@@ -592,6 +596,24 @@ void CegInstantiation::collectDisjuncts( Node n, std::vector< Node >& d ) {
   }
 }
 
+void CegInstantiation::preregisterAssertion( Node n ) {
+  //check if it sygus conjecture
+  if( n.getKind()==FORALL ){
+    if( n.getNumChildren()==3 ){
+      for( unsigned i=0; i<n[2].getNumChildren(); i++ ){
+        if( n[2][i].getKind()==INST_ATTRIBUTE ){
+          Node avar = n[2][i][0];
+          if( avar.getAttribute(SygusAttribute()) ){
+            //this is a sygus conjecture 
+            Trace("cegqi") << "Preregister sygus conjecture : " << n << std::endl;
+            d_conj->preregisterConjecture( n );
+          }
+        }
+      }
+    }
+  }
+}
+
 CegInstantiation::Statistics::Statistics():
   d_cegqi_lemmas_ce("CegInstantiation::cegqi_lemmas_ce", 0),
   d_cegqi_lemmas_refine("CegInstantiation::cegqi_lemmas_refine", 0),

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 9228f11b612113e79bd9b7110030c9b4c3255d99..8aa2e2c267c4414e404e6d4e25c8c4e26eb6bc49 100644 (file)
--- a/src/theory/quantifiers/ce_guided_instantiation.h
+++ b/src/theory/quantifiers/ce_guided_instantiation.h
@@ -89,6 +89,8 @@ public:  //for fairness
   bool isSingleInvocation();
   /** needs check */
   bool needsCheck();
+  /** preregister conjecture */
+  void preregisterConjecture( Node q );
 };
 
 
@@ -139,6 +141,8 @@ public:
   void printSynthSolution( std::ostream& out );
   /** collect disjuncts */
   static void collectDisjuncts( Node n, std::vector< Node >& ex );
+  /** preregister assertion (before rewrite) */
+  void preregisterAssertion( Node n );
 public:
   class Statistics {
   public:

diff --git a/src/theory/quantifiers/ce_guided_single_inv.cpp b/src/theory/quantifiers/ce_guided_single_inv.cpp
index c31ebd9aba746254885d6e09efd96713225cf3f9..19cf9b008dd4d7078f0d1ca08030156ffff77ac4 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv.cpp
@@ -806,6 +806,7 @@ Node CegConjectureSingleInv::reconstructToSyntax( Node s, TypeNode stn, int& rec
   //reconstruct the solution into sygus if necessary
   reconstructed = 0;
   if( options::cegqiSingleInvReconstruct() && !dt.getSygusAllowAll() && !stn.isNull() ){
+    d_sol->preregisterConjecture( d_orig_conjecture );
     d_sygus_solution = d_sol->reconstructSolution( s, stn, reconstructed );
     if( reconstructed==1 ){
       Trace("csi-sol") << "Solution (post-reconstruction into Sygus): " << d_sygus_solution << std::endl;
@@ -859,5 +860,8 @@ bool CegConjectureSingleInv::needsCheck() {
   return true;
 }
 
+void CegConjectureSingleInv::preregisterConjecture( Node q ) {
+  d_orig_conjecture = q;
+}
 
 }
\ No newline at end of file

diff --git a/src/theory/quantifiers/ce_guided_single_inv.h b/src/theory/quantifiers/ce_guided_single_inv.h
index 8950b2642fcd83b4e4ea8a9dd21d8f6bd32c7219..e814df11075f95bd40b9fa478c2537c1e158c86a 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv.h
+++ b/src/theory/quantifiers/ce_guided_single_inv.h
@@ -84,6 +84,8 @@ private:
   //lemmas produced
   inst::InstMatchTrie d_inst_match_trie;
   inst::CDInstMatchTrie * d_c_inst_match_trie;
+  //original conjecture 
+  Node d_orig_conjecture;
   // solution
   std::vector< Node > d_varList;
   Node d_orig_solution;
@@ -129,6 +131,8 @@ public:
   bool isSingleInvocation() { return !d_single_inv.isNull(); }
   //needs check
   bool needsCheck();
+  /** preregister conjecture */
+  void preregisterConjecture( Node q );
 };
 
 }

diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
index 413fd9ba248d8e6f30d3ea7fd0abd3e8c7f7f748..bac39f22cbd857ac4369c02d94c1465e33100574 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.cpp
@@ -618,9 +618,27 @@ Node CegConjectureSingleInvSol::simplifySolutionNode( Node sol, TypeNode stn, st
 }
 
 
-
-
-
+void CegConjectureSingleInvSol::preregisterConjecture( Node q ) {
+  Trace("csi-sol") << "Preregister conjecture : " << q << std::endl;
+  Node n = q;
+  if( n.getKind()==FORALL ){
+    n = n[1];
+  }
+  if( n.getKind()==EXISTS ){
+    if( n[0].getNumChildren()==d_varList.size() ){
+      std::vector< Node > evars;
+      for( unsigned i=0; i<n[0].getNumChildren(); i++ ){
+        evars.push_back( n[0][i] );
+      }
+      n = n[1].substitute( evars.begin(), evars.end(), d_varList.begin(), d_varList.end() );
+    }else{
+      Trace("csi-sol") << "Not the same number of variables, return." << std::endl;
+      return;
+    }
+  }
+  Trace("csi-sol") << "Preregister node for solution reconstruction : " << n << std::endl;
+  registerEquivalentTerms( n );
+}
 
 Node CegConjectureSingleInvSol::reconstructSolution( Node sol, TypeNode stn, int& reconstructed ) {
   Trace("csi-rcons") << "Solution (pre-reconstruction) is : " << sol << std::endl;
@@ -1108,7 +1126,38 @@ void CegConjectureSingleInvSol::getEquivalentTerms( Kind k, Node n, std::vector<
       nn = Rewriter::rewrite( nn );
       equiv.push_back( NodeManager::currentNM()->mkNode( MINUS, NodeManager::currentNM()->mkConst( Rational(0) ), nn ) );
     }
-  }  
-}
+  }
   
+  //based on eqt cache
+  std::map< Node, Node >::iterator itet = d_eqt_rep.find( n );
+  if( itet!=d_eqt_rep.end() ){
+    Node rn = itet->second;
+    for( unsigned i=0; i<d_eqt_eqc[rn].size(); i++ ){
+      if( d_eqt_eqc[rn][i]!=n ){
+        if( std::find( equiv.begin(), equiv.end(), d_eqt_eqc[rn][i] )==equiv.end() ){
+          equiv.push_back( d_eqt_eqc[rn][i] );
+        }
+      }
+    }
+  }
+}
+
+void CegConjectureSingleInvSol::registerEquivalentTerms( Node n ) {
+  for( unsigned i=0; i<n.getNumChildren(); i++ ){
+    registerEquivalentTerms( n[i] );
+  }
+  Node rn = Rewriter::rewrite( n );
+  if( rn!=n ){
+    Trace("csi-equiv") << "  eq terms : " << n << " " << rn << std::endl;
+    d_eqt_rep[n] = rn;
+    d_eqt_rep[rn] = rn;
+    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), rn )==d_eqt_eqc[rn].end() ){
+      d_eqt_eqc[rn].push_back( rn );
+    }
+    if( std::find( d_eqt_eqc[rn].begin(), d_eqt_eqc[rn].end(), n )==d_eqt_eqc[rn].end() ){
+      d_eqt_eqc[rn].push_back( n );
+    }
+  }
+}
+
 }

diff --git a/src/theory/quantifiers/ce_guided_single_inv_sol.h b/src/theory/quantifiers/ce_guided_single_inv_sol.h
index 1d84986b4b3b8de7f7677e9b25d1ba3c4ac8c309..adcc7bf85d38d43d93c265b64bb3dad0a0c481e0 100644 (file)
--- a/src/theory/quantifiers/ce_guided_single_inv_sol.h
+++ b/src/theory/quantifiers/ce_guided_single_inv_sol.h
@@ -65,6 +65,10 @@ private:
 
   std::map< int, std::vector< int > > d_eqc;
   std::map< int, int > d_rep;
+  
+  //equivalent terms
+  std::map< Node, Node > d_eqt_rep;
+  std::map< Node, std::vector< Node > > d_eqt_eqc;
 
   //cache when reconstructing solutions
   std::vector< int > d_tmp_fail;
@@ -80,8 +84,11 @@ private:
   void setReconstructed( int id, Node n );
   //get equivalent terms to n with top symbol k
   void getEquivalentTerms( Kind k, Node n, std::vector< Node >& equiv );
+  //register equivalent terms
+  void registerEquivalentTerms( Node n );
 public:
   Node reconstructSolution( Node sol, TypeNode stn, int& reconstructed );
+  void preregisterConjecture( Node q );
 public:
   CegConjectureSingleInvSol( QuantifiersEngine * qe );
 };

diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index ec71e5348196c81eefad3189ff824221c41b5542..753f3f170c66e9a73d9d8e1b89b7f8ecb20b45d2 100644 (file)
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -226,7 +226,7 @@ option sygusNormalFormGlobalArg --sygus-nf-sym-arg bool :default true
 option sygusNormalFormGlobalContent --sygus-nf-sym-content bool :default true
   generalize based on content in global search space narrowing
   
-option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_NONE :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
+option sygusInvTemplMode --sygus-inv-templ=MODE CVC4::theory::quantifiers::SygusInvTemplMode :default CVC4::theory::quantifiers::SYGUS_INV_TEMPL_MODE_POST :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToSygusInvTemplMode :handler-include "theory/quantifiers/options_handlers.h"
   template mode for sygus invariant synthesis
 
 # approach applied to general quantified formulas