diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-01-10 12:08:16 -0600 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-01-10 12:08:16 -0600 |
commit | 3848242e33130ba507cbfcd5d8296cdeaa3dfa35 (patch) | |
tree | 2c7d4de150eb4c09d7aaf112fd8772a53b7565f8 /src | |
parent | 2ac7e8c916bfb33eb73cd90b20a92bef7036ac6b (diff) |
Track trivial cases in transition inference (#3598)
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/sygus/cegis_core_connective.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/transition_inference.cpp | 4 | ||||
-rw-r--r-- | src/theory/quantifiers/sygus/transition_inference.h | 7 |
3 files changed, 17 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 * |