From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 10 Jan 2020 18:08:16 +0000 (-0600)
Subject: Track trivial cases in transition inference (#3598)
X-Git-Tag: cvc5-1.0.0~3741
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3848242e33130ba507cbfcd5d8296cdeaa3dfa35;p=cvc5.git

Track trivial cases in transition inference (#3598)
---

diff --git a/src/theory/quantifiers/sygus/cegis_core_connective.cpp b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
index 573e11426..a8c4cb0d1 100644
--- a/src/theory/quantifiers/sygus/cegis_core_connective.cpp
+++ b/src/theory/quantifiers/sygus/cegis_core_connective.cpp
@@ -111,6 +111,13 @@ bool CegisCoreConnective::processInitialize(Node conj,
     Trace("sygus-ccore-init") << "...could not infer predicate." << std::endl;
     return false;
   }
+  if (ti.isTrivial())
+  {
+    // not necessary to use this class if the conjecture is trivial (does
+    // not contain the function-to-synthesize).
+    Trace("sygus-ccore-init") << "...conjecture is trivial." << std::endl;
+    return false;
+  }
   Node trans = ti.getTransitionRelation();
   Trace("sygus-ccore-init") << "  transition relation: " << trans << std::endl;
   if (!trans.isConst() || trans.getConst<bool>())
diff --git a/src/theory/quantifiers/sygus/transition_inference.cpp b/src/theory/quantifiers/sygus/transition_inference.cpp
index 7db3f50f8..97dd18492 100644
--- a/src/theory/quantifiers/sygus/transition_inference.cpp
+++ b/src/theory/quantifiers/sygus/transition_inference.cpp
@@ -197,6 +197,7 @@ void TransitionInference::process(Node n)
 {
   NodeManager* nm = NodeManager::currentNM();
   d_complete = true;
+  d_trivial = true;
   std::vector<Node> n_check;
   if (n.getKind() == AND)
   {
@@ -418,8 +419,9 @@ bool TransitionInference::processDisjunct(
   {
     Node op = lit.getOperator();
     // initialize the variables
-    if (d_vars.empty())
+    if (d_trivial)
     {
+      d_trivial = false;
       d_func = op;
       Trace("cegqi-inv-debug") << "Use " << op << " with args ";
       NodeManager* nm = NodeManager::currentNM();
diff --git a/src/theory/quantifiers/sygus/transition_inference.h b/src/theory/quantifiers/sygus/transition_inference.h
index 8939cf6da..a6276e70d 100644
--- a/src/theory/quantifiers/sygus/transition_inference.h
+++ b/src/theory/quantifiers/sygus/transition_inference.h
@@ -158,6 +158,11 @@ class TransitionInference
    * was called on formula that does not have the shape of a transition system.
    */
   bool isComplete() const { return d_complete; }
+  /**
+   * Was the analysis of the conjecture trivial? This is true if the function
+   * did not occur in the conjecture.
+   */
+  bool isTrivial() const { return d_trivial; }
 
   /**
    * The following two functions are used for computing whether this transition
@@ -212,6 +217,8 @@ class TransitionInference
    * of this class complete?
    */
   bool d_complete;
+  /** Was the analyis trivial? */
+  bool d_trivial;
 
   /** process disjunct
    *
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f8608a34d..823bbb0bd 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1727,6 +1727,7 @@ set(regress_1_tests
   regress1/sygus-abduct-test-user.smt2
   regress1/sygus/VC22_a.sy
   regress1/sygus/abd-simple-conj-4.smt2
+  regress1/sygus/abduction_streq.readable.smt2
   regress1/sygus/abv.sy
   regress1/sygus/array_search_5-Q-easy.sy
   regress1/sygus/bvudiv-by-2.sy
diff --git a/test/regress/regress1/sygus/abduction_streq.readable.smt2 b/test/regress/regress1/sygus/abduction_streq.readable.smt2
new file mode 100644
index 000000000..b6a422035
--- /dev/null
+++ b/test/regress/regress1/sygus/abduction_streq.readable.smt2
@@ -0,0 +1,44 @@
+; REQUIRES: proof
+; COMMAND-LINE: --produce-abducts --sygus-core-connective
+; SCRUBBER: grep -v -E '(\(define-fun)'
+; EXIT: 0
+
+(set-info :smt-lib-version |2.6|)
+(set-logic QF_SLIA)
+(set-info :source |
+Generated by: Andrew Reynolds
+Generated on: 2018-04-25
+Generator: Kudzu, converted to v2.6 by CVC4
+Application: Symbolic Execution of Javascript
+Target solver: Kaluza
+Publications: "A symbolic execution framework for JavaScript" by P. Saxena, D. Akhawe, S. Hanna, F. Mao, S. McCamant, and D. Song, 2010.
+|)
+(set-info :license |"https://creativecommons.org/licenses/by/4.0/"|)
+(set-info :category |"industrial"|)
+(set-info :status unknown)
+(declare-fun I0_2 () Int)
+(declare-fun I1_2 () Int)
+(declare-fun I2_2 () Int)
+(declare-fun PCTEMP_LHS_1 () String)
+(declare-fun T1_2 () String)
+(declare-fun T2_2 () String)
+(declare-fun T3_2 () String)
+(declare-fun T_2 () Bool)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun var_0xINPUT_19 () String)
+(assert (= I0_2 (- 5 0)))
+(assert (<= 0 0))
+(assert (<= 0 5))
+(assert (<= 5 I1_2))
+(assert (= I2_2 I1_2))
+(assert (= I0_2 (str.len PCTEMP_LHS_1)))
+(assert (= var_0xINPUT_19 ( str.++ T1_2 T2_2 )))
+(assert (= T2_2 ( str.++ PCTEMP_LHS_1 T3_2 )))
+(assert (= 0 (str.len T1_2)))
+(assert (= I1_2 (str.len var_0xINPUT_19)))
+(assert (= T_2 (= PCTEMP_LHS_1 "Hello")))
+(assert T_2)
+(assert (= T_4 (= PCTEMP_LHS_1 "hello")))
+(assert (= T_5 (not T_4)))
+(get-abduct A T_5)