From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 18 Feb 2022 23:13:14 +0000 (-0600)
Subject: Throw option exceptions when combining input conversion preprocessing with sygus... 
X-Git-Tag: cvc5-1.0.0~412
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9fc39569250d3f503401e003d5cfacd0dd352691;p=cvc5.git

Throw option exceptions when combining input conversion preprocessing with sygus (#8059)

Fixes cvc5/cvc5-projects#436.
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index 9f51dcc24..5a7181f7b 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -889,6 +889,27 @@ bool SetDefaults::usesSygus(const Options& opts) const
   return false;
 }
 
+bool SetDefaults::usesInputConversion(const Options& opts,
+                                      std::ostream& reason) const
+{
+  if (opts.smt.solveBVAsInt != options::SolveBVAsIntMode::OFF)
+  {
+    reason << "solveBVAsInt";
+    return true;
+  }
+  if (opts.smt.solveIntAsBV > 0)
+  {
+    reason << "solveIntAsBV";
+    return true;
+  }
+  if (opts.smt.solveRealAsInt)
+  {
+    reason << "solveRealAsInt";
+    return true;
+  }
+  return false;
+}
+
 bool SetDefaults::incompatibleWithProofs(Options& opts,
                                          std::ostream& reason) const
 {
@@ -1156,6 +1177,18 @@ bool SetDefaults::safeUnsatCores(const Options& opts) const
   return opts.smt.unsatCoresMode == options::UnsatCoresMode::ASSUMPTIONS;
 }
 
+bool SetDefaults::incompatibleWithSygus(Options& opts,
+                                        std::ostream& reason) const
+{
+  // sygus should not be combined with preprocessing passes that convert the
+  // input
+  if (usesInputConversion(opts, reason))
+  {
+    return true;
+  }
+  return false;
+}
+
 bool SetDefaults::incompatibleWithQuantifiers(Options& opts,
                                               std::ostream& reason) const
 {
@@ -1375,6 +1408,14 @@ void SetDefaults::setDefaultsQuantifiers(const LogicInfo& logic,
   // if we are attempting to rewrite everything to SyGuS, use sygus()
   if (usesSygus(opts))
   {
+    std::stringstream reasonNoSygus;
+    if (incompatibleWithSygus(opts, reasonNoSygus))
+    {
+      std::stringstream ss;
+      ss << reasonNoSygus.str() << " not supported in sygus.";
+      throw OptionException(ss.str());
+    }
+    // now, set defaults based on sygus
     setDefaultsSygus(opts);
   }
   // counterexample-guided instantiation for non-sygus
diff --git a/src/smt/set_defaults.h b/src/smt/set_defaults.h
index 238e03b05..2603214fd 100644
--- a/src/smt/set_defaults.h
+++ b/src/smt/set_defaults.h
@@ -56,6 +56,12 @@ class SetDefaults : protected EnvObj
    * Determine whether we will be using SyGuS.
    */
   bool usesSygus(const Options& opts) const;
+  /**
+   * Does options enable an input conversion, e.g. solve-bv-as-int?
+   * If this method returns true, then reason is updated with the name of the
+   * option.
+   */
+  bool usesInputConversion(const Options& opts, std::ostream& reason) const;
   /**
    * Check if incompatible with incremental mode. Notice this method may modify
    * the options to ensure that we are compatible with incremental mode.
@@ -93,6 +99,12 @@ class SetDefaults : protected EnvObj
    * techniques that may interfere with producing correct unsat cores.
    */
   bool safeUnsatCores(const Options& opts) const;
+  /**
+   * Check if incompatible with sygus. Notice this method may
+   * modify the options to ensure that we are compatible with sygus.
+   * The output stream reason is similar to above.
+   */
+  bool incompatibleWithSygus(Options& opts, std::ostream& reason) const;
   /**
    * Check if incompatible with quantified formulas. Notice this method may
    * modify the options to ensure that we are compatible with quantified logics.
diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp
index f8ace3570..e89906933 100644
--- a/test/unit/api/cpp/solver_black.cpp
+++ b/test/unit/api/cpp/solver_black.cpp
@@ -3003,6 +3003,24 @@ TEST_F(TestApiBlackSolver, proj_issue414)
   ASSERT_NO_THROW(slv.simplify(t54));
 }
 
+TEST_F(TestApiBlackSolver, proj_issue436)
+{
+  Solver slv;
+  slv.setOption("produce-abducts", "true");
+  slv.setOption("solve-bv-as-int", "sum");
+  Sort s8 = slv.mkBitVectorSort(68);
+  Term t17 = slv.mkConst(s8, "_x6");
+  Term t23;
+  {
+    uint32_t bw = s8.getBitVectorSize();
+    t23 = slv.mkBitVector(bw, 1);
+  }
+  Term t33 = slv.mkTerm(Kind::BITVECTOR_ULT, {t17, t23});
+  Term abduct;
+  // solve-bv-as-int is incompatible with get-abduct
+  ASSERT_THROW(slv.getAbduct(t33, abduct), CVC5ApiException);
+}
+  
 TEST_F(TestApiBlackSolver, proj_issue431)
 {
   Solver slv;