Fix match trie for polymorphic operators (#3125)

[cvc5.git] / src / preprocessing / passes / sygus_abduct.h

diff --git a/src/preprocessing/passes/sygus_abduct.h b/src/preprocessing/passes/sygus_abduct.h
index 8e83bf1d7955bb53dda2e83946c45a703bf909b1..db40b9688f9561093b2fbd9dbcf53b101e5d9f69 100644 (file)
--- a/src/preprocessing/passes/sygus_abduct.h
+++ b/src/preprocessing/passes/sygus_abduct.h
@@ -13,8 +13,8 @@
  ** input into an abduction problem.
  **/
 
-#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
-#define __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+#ifndef CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
+#define CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H
 
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
@@ -56,6 +56,18 @@ class SygusAbduct : public PreprocessingPass
  public:
   SygusAbduct(PreprocessingPassContext* preprocContext);
 
+  /**
+   * Returns the sygus conjecture corresponding to the abduction problem for
+   * input problem (F above) given by asserts, and axioms (Fa above) given by
+   * axioms. Note that axioms is expected to be a subset of asserts.
+   *
+   * The type abdGType (if non-null) is a sygus datatype type that encodes the
+   * grammar that should be used for solutions of the abduction conjecture.
+   */
+  static Node mkAbductionConjecture(const std::vector<Node>& asserts,
+                                    const std::vector<Node>& axioms,
+                                    TypeNode abdGType);
+
  protected:
   /**
    * Replaces the set of assertions by an abduction sygus problem described
@@ -69,4 +81,4 @@ class SygusAbduct : public PreprocessingPass
 }  // namespace preprocessing
 }  // namespace CVC4
 
-#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */
+#endif /* CVC4__PREPROCESSING__PASSES__SYGUS_ABDUCT_H_ */