Improve defaults for sygus default grammars (#7553)

We now add constants from the conjecture to default grammars by default. We also ensure that integer constants are used as real constants when applicable.

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index b15ed49a68dee32fb93b226cfc135e0ab7719569..e53d3f5ba291e419391824c79735f25da8b60f14 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1112,7 +1112,7 @@ name   = "Quantifiers"
   category   = "regular"
   long       = "sygus-add-const-grammar"
   type       = "bool"
-  default    = "false"
+  default    = "true"
   help       = "statically add constants appearing in conjecture to grammars"
 
 [[option]]

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index 9b4cfb9e109d9237c9f36169ed007eb3666b482c..fce0b9f386dd3564ce59a5748f08064a523a9fc0 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -64,6 +64,7 @@ bool CegGrammarConstructor::hasSyntaxRestrictions(Node q)
 void CegGrammarConstructor::collectTerms(
     Node n, std::map<TypeNode, std::unordered_set<Node>>& consts)
 {
+  NodeManager * nm = NodeManager::currentNM();
   std::unordered_map<TNode, bool> visited;
   std::unordered_map<TNode, bool>::iterator it;
   std::stack<TNode> visit;
@@ -80,11 +81,13 @@ void CegGrammarConstructor::collectTerms(
         TypeNode tn = cur.getType();
         Node c = cur;
         if( tn.isReal() ){
-          c = NodeManager::currentNM()->mkConst( c.getConst<Rational>().abs() );
+          c = nm->mkConst( c.getConst<Rational>().abs() );
         }
-        if( std::find( consts[tn].begin(), consts[tn].end(), c )==consts[tn].end() ){
-          Trace("cegqi-debug") << "...consider const : " << c << std::endl;
-          consts[tn].insert(c);
+        consts[tn].insert(c);
+        if (tn.isInteger())
+        {
+          TypeNode rtype = nm->realType();
+          consts[rtype].insert(c);
         }
       }
       // recurse

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 99c65e973a1f5e0fcd9fa1496b007c82196df8ca..3bd5e33f0d05d51ea9effae2ee2a76d5456e7431 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1508,6 +1508,7 @@ set(regress_0_tests
 # Regression level 1 tests
 
 set(regress_1_tests
+  regress1/abduction/abd-real-const.smt2
   regress1/abduction/sygus-abduct-test-user.smt2
   regress1/abduction/issue5848-4.smt2
   regress1/abduction/issue5848-2.smt2

diff --git a/test/regress/regress1/abduction/abd-real-const.smt2 b/test/regress/regress1/abduction/abd-real-const.smt2
new file mode 100644 (file)
index 0000000..258d80a
--- /dev/null
+++ b/test/regress/regress1/abduction/abd-real-const.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --produce-abducts
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+(set-logic QF_LRA)
+(declare-const x Real)
+(declare-const y Real)
+(declare-const z Real)
+(assert (and (>= x 0) (< y 7)))
+(get-abduct A (>= y 5))