diff options
5 files changed, 62 insertions, 1 deletions
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 e4d0d1fd9..9e3e04f06 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -1728,6 +1728,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) |