From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 18 Aug 2021 21:06:52 +0000 (-0700)
Subject: Minor fixes of policy for eliminating quantifiers (#7033)
X-Git-Tag: cvc5-1.0.0~1372
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7ef9f24a1a879d278d8ac5a3fef28c7ca8489d2c;p=cvc5.git

Minor fixes of policy for eliminating quantifiers (#7033)

PR #7017 fixed the policy for eliminating quantifiers but introduced
some minor issues, which this commit fixes:

the InstantiationEngine::checkOwnership() method was changed to look
for patterns in the wrong node.
the PR changed the modes of the --user-pat=MODE method but reused
one of the names. This commit fixes the name and adds a check in the
options script.
fixing the policy caused cvc5 to answer unsat instead of the
expected unknown for regress0/use_approx/bug812_approx.smt2. The
commit updates the expected result.
---

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index edc0f88f4..a861b06eb 100644
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -610,12 +610,20 @@ def codegen_module(module, dst_dir, tpls):
                     cases=''.join(cases)))
 
             # Generate str-to-enum handler
+            names = set()
             cases = []
             for value, attrib in option.mode.items():
                 assert len(attrib) == 1
+                name = attrib[0]['name']
+                if name in names:
+                    die("multiple modes with the name '{}' for option '{}'".
+                        format(name, option.long))
+                else:
+                    names.add(name)
+
                 cases.append(
                     TPL_MODE_HANDLER_CASE.format(
-                        name=attrib[0]['name'],
+                        name=name,
                         type=option.type,
                         enum=value))
             assert option.long
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ad74e4ab9..1bd29684a 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -381,7 +381,7 @@ name   = "Quantifiers"
   name = "trust"
   help = "When provided, use only user-provided patterns for a quantified formula."
 [[option.mode.STRICT]]
-  name = "trust"
+  name = "strict"
   help = "When provided, use only user-provided patterns for a quantified formula, and do not use any other instantiation techniques."
 [[option.mode.RESORT]]
   name = "resort"
diff --git a/src/theory/quantifiers/ematching/instantiation_engine.cpp b/src/theory/quantifiers/ematching/instantiation_engine.cpp
index d9bec820c..99949e223 100644
--- a/src/theory/quantifiers/ematching/instantiation_engine.cpp
+++ b/src/theory/quantifiers/ematching/instantiation_engine.cpp
@@ -205,7 +205,7 @@ void InstantiationEngine::checkOwnership(Node q)
   {
     //if strict triggers, take ownership of this quantified formula
     bool hasPat = false;
-    for (const Node& qc : q)
+    for (const Node& qc : q[2])
     {
       if (qc.getKind() == INST_PATTERN || qc.getKind() == INST_NO_PATTERN)
       {
diff --git a/test/regress/regress0/use_approx/bug812_approx.smt2 b/test/regress/regress0/use_approx/bug812_approx.smt2
index 4b5af6710..45908e3dd 100644
--- a/test/regress/regress0/use_approx/bug812_approx.smt2
+++ b/test/regress/regress0/use_approx/bug812_approx.smt2
@@ -1,11 +1,10 @@
 ; REQUIRES: glpk
 ; COMMAND-LINE: --use-approx
-; EXPECT: unknown
 (set-logic UFNIA)
 (set-info :source "Reduced from regression 'bug812.smt2' using ddSMT to exercise GLPK")
 (set-info :smt-lib-version 2.6)
 (set-info :category "crafted")
-(set-info :status unknown)
+(set-info :status unsat)
 (declare-fun s (Int Int) Int)
 (declare-fun P (Int Int Int) Int)
 (declare-fun p (Int) Int)