Make getSynthSolution return a Bool (#3306)

1 files changed, 9 insertions, 6 deletions

diff --git a/src/theory/quantifiers/sygus/synth_conjecture.h b/src/theory/quantifiers/sygus/synth_conjecture.h
index 8ae30f636..a86ff6f75 100644
--- a/src/theory/quantifiers/sygus/synth_conjecture.h
+++ b/src/theory/quantifiers/sygus/synth_conjecture.h
@@ -113,13 +113,16 @@ class SynthConjecture
   void printSynthSolution(std::ostream& out);
   /** get synth solutions
    *
-   * This returns a map from function-to-synthesize variables to their
-   * builtin solution, which has the same type. For example, for synthesis
+   * This method returns true if this class has a solution available to the
+   * conjecture that it was assigned.
+   *
+   * This method adds entries to sol_map that map functions-to-synthesize to
+   * their builtin solution, which has the same type. For example, for synthesis
    * conjecture exists f. forall x. f( x )>x, this function may return the map
    * containing the entry:
    *   f -> (lambda x. x+1)
    */
-  void getSynthSolutions(std::map<Node, Node>& sol_map);
+  bool getSynthSolutions(std::map<Node, Node>& sol_map);
   /**
    * The feasible guard whose semantics are "this conjecture is feasiable".
    * This is "G" in Figure 3 of Reynolds et al CAV 2015.
@@ -174,10 +177,10 @@ class SynthConjecture
   /** The feasible guard. */
   Node d_feasible_guard;
   /**
-   * Do we have a solution in this user context? This is user-context dependent
-   * to enable use cases of sygus in incremental mode.
+   * Do we have a solution in this solve context? This flag is reset to false
+   * on every call to presolve.
    */
-  context::CDO<bool> d_hasSolution;
+  bool d_hasSolution;
   /** the decision strategy for the feasible guard */
   std::unique_ptr<DecisionStrategy> d_feasible_strategy;
   /** single invocation utility */