CBQI BV choice expressions (#1296)

[cvc5.git] / src / theory / quantifiers / ceg_t_instantiator.h

diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h
index 9f47e72111db8148cdcbf2dfae789c6bb9ce04a2..30dd1bffad9630c2ba416dda0aa0b8736d0cf933 100644 (file)
--- a/src/theory/quantifiers/ceg_t_instantiator.h
+++ b/src/theory/quantifiers/ceg_t_instantiator.h
@@ -101,7 +101,23 @@ private:
   /** rewrite assertion for solve pv
   * returns a literal that is equivalent to lit that leads to best solved form for pv
   */
-  Node rewriteAssertionForSolvePv( Node pv, Node lit );
+  Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit);
+  /** rewrite term for solve pv
+   * This is a helper function for rewriteAssertionForSolvePv.
+   * If this returns non-null value ret, then this indicates
+   * that n should be rewritten to ret. It is called as
+   * a "post-rewrite", that is, after the children of n
+   * have been rewritten and stored in the vector children.
+   *
+   * contains_pv stores whether certain nodes contain pv.
+   * where we guarantee that all subterms of terms in children
+   * appear in the domain of contains_pv.
+   */
+  Node rewriteTermForSolvePv(
+      Node pv,
+      Node n,
+      std::vector<Node>& children,
+      std::unordered_map<TNode, bool, TNodeHashFunction>& contains_pv);
   /** process literal, called from processAssertion
   * lit is the literal to solve for pv that has been rewritten according to
   * internal rules here.
@@ -121,8 +137,6 @@ private:
                         Node alit, unsigned effort);
   bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv,
                          unsigned effort);
-  bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort );
-  bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas );
   bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; }
   std::string identify() const { return "Bv"; }
 };