From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Mon, 26 Mar 2018 16:53:51 +0000 (-0500)
Subject: Abort when sygus-verify finds unsoundness. (#1717)
X-Git-Tag: cvc5-1.0.0~5210
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5a669e6ed1c51cc80cc1dd313906ca47345abccd;p=cvc5.git

Abort when sygus-verify finds unsoundness. (#1717)
---

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 1437e9992..c40491a40 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1122,6 +1122,14 @@ header = "options/quantifiers_options.h"
   default    = "false"
   help       = "use sygus to verify the correctness of rewrite rules via sampling"
 
+[[option]]
+  name       = "sygusRewVerifyAbort"
+  category   = "regular"
+  long       = "sygus-rr-verify-abort"
+  type       = "bool"
+  default    = "true"
+  help       = "abort when sygus-rr-verify finds an instance of unsoundness"
+
 [[option]]
   name       = "sygusSamples"
   category   = "regular"
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp
index 7fe403526..4d3584596 100644
--- a/src/theory/datatypes/datatypes_sygus.cpp
+++ b/src/theory/datatypes/datatypes_sygus.cpp
@@ -827,9 +827,16 @@ bool SygusSymBreakNew::registerSearchValue( Node a, Node n, Node nv, unsigned d,
             }
             else
             {
+              // no witness point found?
               Assert(false);
             }
           }
+          if (options::sygusRewVerifyAbort())
+          {
+            AlwaysAssert(
+                false,
+                "--sygus-rr-verify detected unsoundness in the rewriter!");
+          }
         }
       }