Sygus abduction feature (#2744)

1 files changed, 12 insertions, 0 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index e53d1eb55..5c41feaba 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -209,6 +209,9 @@ class CVC4_PUBLIC SmtEngine {
    */
   Options d_originalOptions;
 
+  /** whether this is an internal subsolver */
+  bool d_isInternalSubsolver;
+
   /**
    * Number of internal pops that have been deferred.
    */
@@ -502,6 +505,15 @@ class CVC4_PUBLIC SmtEngine {
   void setOption(const std::string& key, const CVC4::SExpr& value)
       /* throw(OptionException, ModalException) */;
 
+  /** Set is internal subsolver.
+   *
+   * This function is called on SmtEngine objects that are created internally.
+   * It is used to mark that this SmtEngine should not perform preprocessing
+   * passes that rephrase the input, such as --sygus-rr-synth-input or
+   * --sygus-abduct.
+   */
+  void setIsInternalSubsolver();
+
   /** sets the input name */
   void setFilename(std::string filename);
   /** return the input name (if any) */