From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Thu, 4 Nov 2021 21:01:41 +0000 (-0500)
Subject: Improve defaults for sygus default grammars (#7553)
X-Git-Tag: cvc5-1.0.0~888
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=be6f9c2ee9201cc5181ce7ba27b6fe992ab3fff6;p=cvc5.git

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 b15ed49a6..e53d3f5ba 100644
--- 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 9b4cfb9e1..fce0b9f38 100644
--- 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 99c65e973..3bd5e33f0 100644
--- 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
index 000000000..258d80a88
--- /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))