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

1 files changed, 4 insertions, 0 deletions

diff --git a/src/theory/quantifiers/ce_guided_instantiation.h b/src/theory/quantifiers/ce_guided_instantiation.h
index 9228f11b6..8aa2e2c26 100644
--- 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: