Improvements to sygus, register equivalent terms based on rewrites of original conjecture, set default invariant template mode to post-condition.

1 files changed, 22 insertions, 0 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.cpp b/src/theory/quantifiers/ce_guided_instantiation.cpp
index f01efb5c4..0bc5bb008 100644
--- 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),