Make sygus inference a preprocessing pass (#2334)

1 files changed, 71 insertions, 0 deletions

diff --git a/src/preprocessing/passes/sygus_inference.h b/src/preprocessing/passes/sygus_inference.h
new file mode 100644
index 000000000..5e7c6f7d0
--- /dev/null
+++ b/src/preprocessing/passes/sygus_inference.h
@@ -0,0 +1,71 @@
+/*********************                                                        */
+/*! \file sygus_inference.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief SygusInference
+ **/
+
+#ifndef __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
+#define __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_
+
+#include <map>
+#include <string>
+#include <vector>
+#include "expr/node.h"
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+/** SygusInference
+ *
+ * A preprocessing utility that turns a set of (quantified) assertions into a
+ * single SyGuS conjecture. If this is possible, we solve for this single Sygus
+ * conjecture using a separate copy of the SMT engine. If sygus successfully
+ * solves the conjecture, we plug the synthesis solutions back into the original
+ * problem, thus obtaining a set of model substitutions under which the
+ * assertions should simplify to true.
+ */
+class SygusInference : public PreprocessingPass
+{
+ public:
+  SygusInference(PreprocessingPassContext* preprocContext);
+
+ protected:
+  /**
+   * Either replaces all uninterpreted functions in assertions by their
+   * interpretation in a sygus solution, or leaves the assertions unmodified.
+   */
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
+  /** solve sygus
+   *
+   * Returns true if we can recast the input problem assertions as a sygus
+   * problem and successfully solve it using a separate call to an SMT engine.
+   *
+   * We fail if either a sygus conjecture that corresponds to assertions cannot
+   * be inferred, or the sygus conjecture we infer is infeasible.
+   *
+   * If this function returns true, then we add all uninterpreted symbols s in
+   * assertions to funs and their corresponding solution to sols.
+   */
+  bool solveSygus(std::vector<Node>& assertions,
+                  std::vector<Node>& funs,
+                  std::vector<Node>& sols);
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif /* __CVC4__PREPROCESSING__PASSES__SYGUS_INFERENCE_H_ */