From f4d031742d969c689d38c0756a5026a434ef89b3 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Sun, 29 Jun 2014 18:44:40 -0400 Subject: [PATCH] sets: "insert" operator MIME-Version: 1.0 Content-Type: text/plain; charset=utf8 Content-Transfer-Encoding: 8bit new™! support for (insert (X (Set X)) (Set X) :right-associative) from the finte sets theory prosoal. e.g., (insert 1 2 3 4 (singleton 5)) --- src/parser/smt2/smt2.cpp | 1 + src/printer/smt2/smt2_printer.cpp | 1 + src/theory/sets/kinds | 3 +++ src/theory/sets/theory_sets_rewriter.cpp | 9 ++++++++ src/theory/sets/theory_sets_type_rules.h | 28 ++++++++++++++++++++++++ test/regress/regress0/sets/Makefile.am | 1 + test/regress/regress0/sets/insert.smt2 | 7 ++++++ 7 files changed, 50 insertions(+) create mode 100644 test/regress/regress0/sets/insert.smt2 diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 3f1e59e6d..0c4b1258f 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -152,6 +152,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SUBSET, "subset"); addOperator(kind::MEMBER, "member"); addOperator(kind::SINGLETON, "singleton"); + addOperator(kind::INSERT, "insert"); break; case THEORY_DATATYPES: diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 3c0f4ebc5..bc2cb1ec9 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -613,6 +613,7 @@ static string smtKindString(Kind k) throw() { case kind::MEMBER: return "member"; case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; + case kind::INSERT: return "insert"; default: ; /* fall through */ } diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index 06d3be5a0..39e7883c6 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -41,6 +41,7 @@ operator SETMINUS 2 "set subtraction" operator SUBSET 2 "subset predicate; first parameter a subset of second" operator MEMBER 2 "set membership predicate; first parameter a member of second" operator SINGLETON 1 "the set of the single element given as a parameter" +operator INSERT 2: "set obtained by inserting elements (first N-1 parameters) into a set (the last parameter)" typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -49,10 +50,12 @@ typerule SUBSET ::CVC4::theory::sets::SubsetTypeRule typerule MEMBER ::CVC4::theory::sets::MemberTypeRule typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule +typerule INSERT ::CVC4::theory::sets::InsertTypeRule construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule +construle INSERT ::CVC4::theory::sets::InsertTypeRule endtheory diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index ce469cc0c..8716d1065 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -239,6 +239,15 @@ RewriteResponse TheorySetsRewriter::preRewrite(TNode node) { return RewriteResponse(REWRITE_DONE, nm->mkConst(true)); // Further optimization, if constants but differing ones + if(node.getKind() == kind::INSERT) { + Node insertedElements = nm->mkNode(kind::SINGLETON, node[0]); + size_t setNodeIndex = node.getNumChildren()-1; + for(size_t i = 1; i < setNodeIndex; ++i) { + insertedElements = nm->mkNode(kind::UNION, insertedElements, nm->mkNode(kind::SINGLETON, node[i])); + } + return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::UNION, insertedElements, node[setNodeIndex])); + }//kind::INSERT + if(node.getType().isSet() && node.isConst()) { //rewrite set to normal form SettermElementsMap setTermElementsMap; // cache diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 2267ee22a..fa1183e07 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -130,6 +130,34 @@ struct EmptySetTypeRule { } };/* struct EmptySetTypeRule */ +struct InsertTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::INSERT); + size_t numChildren = n.getNumChildren(); + Assert( numChildren >= 2 ); + TypeNode setType = n[numChildren-1].getType(check); + if( check ) { + if(!setType.isSet()) { + throw TypeCheckingExceptionPrivate(n, "inserting into a non-set"); + } + for(size_t i = 0; i < numChildren-1; ++i) { + TypeNode elementType = n[i].getType(check); + if(elementType != setType.getSetElementType()) { + throw TypeCheckingExceptionPrivate + (n, "type of element should be same as element type of set being inserted into"); + } + } + } + return setType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::INSERT); + return n[0].isConst() && n[1].isConst(); + } +};/* struct InsertTypeRule */ + struct SetsProperties { inline static Cardinality computeCardinality(TypeNode type) { diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index ccedc7596..9536dfac1 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -44,6 +44,7 @@ TESTS = \ error1.smt2 \ error2.smt2 \ eqtest.smt2 \ + insert.smt2 \ fuzz14418.smt2 \ fuzz15201.smt2 \ fuzz31811.smt2 \ diff --git a/test/regress/regress0/sets/insert.smt2 b/test/regress/regress0/sets/insert.smt2 new file mode 100644 index 000000000..3a7b18179 --- /dev/null +++ b/test/regress/regress0/sets/insert.smt2 @@ -0,0 +1,7 @@ +(set-option :produce-models true) +(set-logic QF_UFLIA_SETS) +(set-info :status sat) +(declare-fun X () (Set Int)) +(assert (= X (insert 1 2 (singleton 3)))) +(check-sat) +;(get-model) -- 2.30.2