diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/sets/theory_sets.cpp | 3 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 6 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 11 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 32 |
4 files changed, 21 insertions, 31 deletions
diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp index e4f281de8..e06a8cb52 100644 --- a/src/theory/sets/theory_sets.cpp +++ b/src/theory/sets/theory_sets.cpp @@ -158,8 +158,7 @@ TrustNode TheorySets::ppRewrite(TNode n) throw LogicException(ss.str()); } } - // just expand definitions - return expandDefinition(n); + return d_internal->ppRewrite(n); } Theory::PPAssertStatus TheorySets::ppAssert( diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index 3b95c7e00..a22e75d91 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -76,7 +76,13 @@ class TheorySets : public Theory Node getModelValue(TNode) override; std::string identify() const override { return "THEORY_SETS"; } void preRegisterTerm(TNode node) override; + /** Expand partial operators (choose) from n. */ TrustNode expandDefinition(Node n) override; + /** + * If the sets-ext option is not set and we have an extended operator, + * we throw an exception. Additionally, we expand operators like choose + * and is_singleton. + */ TrustNode ppRewrite(TNode n) override; PPAssertStatus ppAssert(TrustNode tin, TrustSubstitutionMap& outSubstitutions) override; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 4390b3e6e..5558b95d4 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1269,6 +1269,17 @@ TrustNode TheorySetsPrivate::expandDefinition(Node node) { Debug("sets-proc") << "expandDefinition : " << node << std::endl; + if (node.getKind()==kind::CHOOSE) + { + return expandChooseOperator(node); + } + return TrustNode::null(); +} + +TrustNode TheorySetsPrivate::ppRewrite(Node node) +{ + Debug("sets-proc") << "ppRewrite : " << node << std::endl; + switch (node.getKind()) { case kind::CHOOSE: return expandChooseOperator(node); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 8247d4940..ee42a7989 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -167,36 +167,10 @@ class TheorySetsPrivate { void preRegisterTerm(TNode node); - /** expandDefinition - * If the sets-ext option is not set and we have an extended operator, - * we throw an exception. This function is a no-op otherwise. - * - * TheorySets uses expandDefinition as an entry point to see if the input - * contains extended operators. - * - * We need to be notified when a universe set occurs in our input, - * before preprocessing and simplification takes place. Otherwise the models - * may be inaccurate when setsExt is false, here is an example: - * - * x,y : (Set Int) - * x = (as univset (Set Int)); - * 0 in y; - * check-sat; - * - * If setsExt is enabled, the model value of (as univset (Set Int)) is always accurate. - * - * If setsExt is not enabled, the following can happen for the above example: - * x = (as univset (Set Int)) is made into a model substitution during - * simplification. This means (as univset (Set Int)) is not a term in any assertion, - * and hence we do not throw an exception, nor do we infer that 0 is a member of - * (as univset (Set Int)). We instead report a model where x = {}. The correct behavior - * is to throw an exception that says universe set is not supported when setsExt disabled. - * Hence we check for the existence of universe set before simplification here. - * - * Another option to fix this is to make TheoryModel::getValue more general - * so that it makes theory-specific calls to evaluate interpreted symbols. - */ + /** ppRewrite, which expands choose. */ TrustNode expandDefinition(Node n); + /** ppRewrite, which expands choose and is_singleton. */ + TrustNode ppRewrite(Node n); void presolve(); |