diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/transition_inference.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/transition_inference.h | 7 |
1 files changed, 7 insertions, 0 deletions
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 * |