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 edc0f88f4d9c26d865fb899ef4349adf90ac448f..a861b06ebe157dacc5da19bc3bfddfd2863c783a 100644 (file)
--- 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 ad74e4ab9510fc02aa2dc5100c095545bde192f6..1bd29684a3975e9de13a19199d6a97901064a109 100644 (file)
--- 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 d9bec820ce6285c81b1e86d977b4026b5221069d..99949e223f8985b70ebe8afdd95342fd3d6d221d 100644 (file)
--- 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 4b5af67105a408bd4b9f197e1fcd4b102b49ec37..45908e3ddcc6d4155ceed83a295fff778891754d 100644 (file)
--- 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)