From 13cf41801f8f2bac538cb45d53ae7427916041a7 Mon Sep 17 00:00:00 2001 From: mudathirmahgoub Date: Sun, 4 Oct 2020 15:10:24 -0500 Subject: Remove subtyping for sets theory (#5179) This PR removes subtyping for sets theory due to issues like #4502, #4507 and #4631. Changes: Add SingletonOp for singletons to specify the type of the single element in the set. Add mkSingleton to the solver to enable the user to pass the sort of the single element. Update smt and cvc parsers to use mkSingleton when the kind is SINGLETON --- src/theory/quantifiers/fmf/bounded_integers.cpp | 2 +- src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 8 +++++++- 2 files changed, 8 insertions(+), 2 deletions(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index 28731b371..2d6af9a63 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -676,7 +676,7 @@ Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { Assert(i < d_setm_choice[sro].size()); choice_i = d_setm_choice[sro][i]; choices.push_back(choice_i); - Node sChoiceI = nm->mkNode(SINGLETON, choice_i); + Node sChoiceI = nm->mkSingleton(choice_i.getType(), choice_i); if (nsr.isNull()) { nsr = sChoiceI; diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index 1b86afb85..ba9962bd9 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -965,7 +965,13 @@ void CegGrammarConstructor::mkSygusDefaultGrammar( Trace("sygus-grammar-def") << "...add for singleton" << std::endl; std::vector cargsSingleton; cargsSingleton.push_back(unresElemType); - sdts[i].addConstructor(SINGLETON, cargsSingleton); + + // lambda x . (singleton (singleton_op T) x) where T = x.getType() + Node x = nm->mkBoundVar(etype); + Node vars = nm->mkNode(BOUND_VAR_LIST, x); + Node singleton = nm->mkSingleton(etype, x); + Node lambda = nm->mkNode(LAMBDA,vars, singleton); + sdts[i].addConstructor(lambda, "singleton", cargsSingleton); // add for union, difference, intersection std::vector bin_kinds = {UNION, INTERSECTION, SETMINUS}; -- cgit v1.2.3