From 51fbe09f8b16ad0a49b2add0801b2963de08427e Mon Sep 17 00:00:00 2001 From: PaulMeng Date: Mon, 15 Feb 2016 17:36:07 -0600 Subject: [PATCH] extended smt parser for the finite relations fixed typing rules for relational terms added a benchmark example for the theory of finite relations --- src/parser/smt2/smt2.cpp | 4 ++ src/printer/smt2/smt2_printer.cpp | 8 +++ src/theory/sets/theory_sets_private.cpp | 2 +- src/theory/sets/theory_sets_rels.cpp | 88 +++++++++++++++++------- src/theory/sets/theory_sets_rels.h | 16 ++++- src/theory/sets/theory_sets_type_rules.h | 45 +++++++++--- test/regress/regress0/sets/Makefile.am | 1 + test/regress/regress0/sets/rels/rel.cvc | 20 ++++++ 8 files changed, 150 insertions(+), 34 deletions(-) create mode 100644 test/regress/regress0/sets/rels/rel.cvc diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e3fbe36f2..530e9da8b 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -224,6 +224,10 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SETMINUS, "setminus"); addOperator(kind::SUBSET, "subset"); addOperator(kind::MEMBER, "member"); + addOperator(kind::TRANSPOSE, "transpose"); + addOperator(kind::TRANSCLOSURE, "transclosure"); + addOperator(kind::JOIN, "join"); + addOperator(kind::PRODUCT, "product"); addOperator(kind::SINGLETON, "singleton"); addOperator(kind::INSERT, "insert"); break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index ece4e9177..7afbf4e40 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -506,6 +506,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SUBSET: case kind::MEMBER: case kind::SET_TYPE: + case kind::TRANSCLOSURE: + case kind::TRANSPOSE: + case kind::JOIN: + case kind::PRODUCT: case kind::SINGLETON: out << smtKindString(k) << " "; break; // fp theory @@ -784,6 +788,10 @@ static string smtKindString(Kind k) throw() { case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; case kind::INSERT: return "insert"; + case kind::TRANSCLOSURE: return "transclosure"; + case kind::TRANSPOSE: return "transpose"; + case kind::PRODUCT: return "product"; + case kind::JOIN: return "join"; // fp theory case kind::FLOATINGPOINT_FP: return "fp"; diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index c7f34bb52..9d3f7e08e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1111,7 +1111,7 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_rels(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); - d_rels = new TheorySetsRels(&d_equalityEngine); + d_rels = new TheorySetsRels(c, u, &d_equalityEngine); d_equalityEngine.addFunctionKind(kind::UNION); d_equalityEngine.addFunctionKind(kind::INTERSECTION); diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp index 7ed0ada32..24a69bfdb 100644 --- a/src/theory/sets/theory_sets_rels.cpp +++ b/src/theory/sets/theory_sets_rels.cpp @@ -16,7 +16,7 @@ #include "theory/sets/theory_sets_rels.h" -//#include "expr/emptyset.h" +#include "expr/datatype.h" //#include "options/sets_options.h" //#include "smt/smt_statistics_registry.h" //#include "theory/sets/expr_patterns.h" // ONLY included here @@ -33,8 +33,13 @@ namespace CVC4 { namespace theory { namespace sets { - TheorySetsRels::TheorySetsRels(eq::EqualityEngine* eq): - d_eqEngine(eq) + TheorySetsRels::TheorySetsRels(context::Context* c, + context::UserContext* u, + eq::EqualityEngine* eq): + d_trueNode(NodeManager::currentNM()->mkConst(true)), + d_falseNode(NodeManager::currentNM()->mkConst(false)), + d_eqEngine(eq), + d_relsSaver(c) { d_eqEngine->addFunctionKind(kind::PRODUCT); d_eqEngine->addFunctionKind(kind::JOIN); @@ -42,59 +47,94 @@ namespace sets { d_eqEngine->addFunctionKind(kind::TRANSCLOSURE); } - TheorySetsRels::TheorySetsRels::~TheorySetsRels() {} + TheorySetsRels::~TheorySetsRels() {} - void TheorySetsRels::TheorySetsRels::check(Theory::Effort level) { + void TheorySetsRels::check(Theory::Effort level) { - Debug("rels") << "\nStart iterating equivalence class......\n" << std::endl; + Debug("rels-eqc") << "\nStart iterating equivalence classes......\n" << std::endl; if (!d_eqEngine->consistent()) return; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( d_eqEngine ); - std::map< TypeNode, int > typ_num; while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); - TypeNode tr = r.getType(); - if( typ_num.find( tr )==typ_num.end() ){ - typ_num[tr] = 0; - } - typ_num[tr]++; bool firstTime = true; - Debug("rels") << " " << r; - Debug("rels") << " : { "; + Debug("rels-eqc") << " " << r; + Debug("rels-eqc") << " : { "; eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine ); while( !eqc_i.isFinished() ){ TNode n = (*eqc_i); + + // only consider membership constraints that involving relatioinal operators + if((d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_trueNode) + || d_eqEngine->getRepresentative(r) == d_eqEngine->getRepresentative(d_falseNode)) + && !d_relsSaver.contains(n)) { + d_relsSaver.insert(n); + + // case: (b, a) IS_IN (TRANSPOSE X) + // => (a, b) IS_IN X + if(n.getKind() == kind::MEMBER) { + if(kind::TRANSPOSE == n[1].getKind()) { + Node reversedTuple = reverseTuple(n[0]); + Node fact = NodeManager::currentNM()->mkNode(kind::MEMBER, reversedTuple, n[1][0]); +// assertMembership(fact, n, r == d_trueNode); + } else if(kind::JOIN == n[1].getKind()) { + + }else if(kind::PRODUCT == n[1].getKind()) { + + } + } + } + if( r!=n ){ if( firstTime ){ - Debug("rels") << std::endl; + Debug("rels-eqc") << std::endl; firstTime = false; } if (n.getKind() == kind::PRODUCT || n.getKind() == kind::JOIN || n.getKind() == kind::TRANSCLOSURE || n.getKind() == kind::TRANSPOSE) { - Debug("rels") << " " << n << std::endl; + Debug("rels-eqc") << " *** " << n << std::endl; + }else{ + Debug("rels-eqc") << " " << n < elements; + Datatype dt = (Datatype)((tuple.getType()).getDatatype()); + elements.push_back(tuple.getOperator()); + for(Node::iterator child_it = tuple.end()-1; + child_it != tuple.begin()-1; --child_it) { + elements.push_back(*child_it); + } + return NodeManager::currentNM()->mkNode(kind::APPLY_CONSTRUCTOR, elements); + } + void TheorySetsRels::assertMembership(TNode fact, TNode reason, bool polarity) { + TNode explain = reason; + if(!polarity) { + explain = reason.negate(); + } + Debug("rels") << " polarity : " << polarity << " reason: " << explain << std::endl; + d_eqEngine->assertPredicate(fact, polarity, explain); + } +} +} +} diff --git a/src/theory/sets/theory_sets_rels.h b/src/theory/sets/theory_sets_rels.h index d83fd59c2..c48217275 100644 --- a/src/theory/sets/theory_sets_rels.h +++ b/src/theory/sets/theory_sets_rels.h @@ -19,6 +19,7 @@ #include "theory/theory.h" #include "theory/uf/equality_engine.h" +#include "context/cdhashset.h" namespace CVC4 { namespace theory { @@ -27,7 +28,9 @@ namespace sets { class TheorySetsRels { public: - TheorySetsRels(eq::EqualityEngine*); + TheorySetsRels(context::Context* c, + context::UserContext* u, + eq::EqualityEngine*); ~TheorySetsRels(); @@ -35,7 +38,18 @@ public: private: + /** True and false constant nodes */ + Node d_trueNode; + Node d_falseNode; + eq::EqualityEngine *d_eqEngine; + + // save all the relational terms seen so far + context::CDHashSet d_relsSaver; + + void assertMembership(TNode fact, TNode reason, bool polarity); + + Node reverseTuple(TNode tuple); }; }/* CVC4::theory::sets namespace */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 3b0fabf59..8d294ceeb 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -105,7 +105,7 @@ struct MemberTypeRule { throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set"); } TypeNode elementType = n[0].getType(check); - if(elementType != setType.getSetElementType()) { + if(!setType.getSetElementType().isSubtypeOf(elementType)) { throw TypeCheckingExceptionPrivate(n, "member operating on sets of different types"); } } @@ -172,24 +172,46 @@ struct RelBinaryOperatorTypeRule { TypeNode firstRelType = n[0].getType(check); TypeNode secondRelType = n[1].getType(check); + TypeNode resultType = firstRelType; if(check) { + if(!firstRelType.isSet() || !secondRelType.isSet()) { throw TypeCheckingExceptionPrivate(n, " set operator operates on non-sets"); } if(!firstRelType[0].isTuple() || !secondRelType[0].isTuple()) { throw TypeCheckingExceptionPrivate(n, " set operator operates on non-relations (sets of tuples)"); } - // JOIN is applied on two sets of tuples that are not both unary + + std::vector newTupleTypes; + std::vector firstTupleTypes = firstRelType[0].getTupleTypes(); + std::vector secondTupleTypes = secondRelType[0].getTupleTypes(); + // JOIN is not allowed to apply on two unary sets if(n.getKind() == kind::JOIN) { - if((firstRelType[0].getNumChildren() == 1) && (secondRelType[0].getNumChildren() == 1)) { + if((firstTupleTypes.size() == 1) && (secondTupleTypes.size() == 1)) { throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations"); } + if(firstTupleTypes.back() != secondTupleTypes.front()) { + throw TypeCheckingExceptionPrivate(n, " Join operates on two non-joinable relations"); + } + + if(firstTupleTypes.size() == 1) { + newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end()); + } else if (secondTupleTypes.size() == 1) { + newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1); + } else { + newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()-1); + newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin()+1, secondTupleTypes.end()); + } + }else if(n.getKind() == kind::PRODUCT) { + newTupleTypes.insert(newTupleTypes.end(), firstTupleTypes.begin(), firstTupleTypes.end()); + newTupleTypes.insert(newTupleTypes.end(), secondTupleTypes.begin(), secondTupleTypes.end()); } + resultType = nodeManager->mkSetType(nodeManager->mkTupleType(newTupleTypes)); } - Assert(firstRelType == secondRelType); - return firstRelType; + Debug("rels") << "The resulting Type is " << resultType << std::endl; + return resultType; } inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { @@ -204,10 +226,17 @@ struct RelTransposeTypeRule { throw (TypeCheckingExceptionPrivate, AssertionException) { Assert(n.getKind() == kind::TRANSPOSE); TypeNode setType = n[0].getType(check); - if(check && !setType.isSet()) { - throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-rel"); + if(check && !setType.isSet() && !setType[0].isTuple()) { + throw TypeCheckingExceptionPrivate(n, "relation transpose operats on non-relation"); } - return setType; + + std::vector tupleTypes; + std::vector originalTupleTypes = setType[0].getTupleTypes(); + for(std::vector::reverse_iterator it = originalTupleTypes.rbegin(); it != originalTupleTypes.rend(); ++it) { + tupleTypes.push_back(*it); + } + + return nodeManager->mkSetType(nodeManager->mkTupleType(tupleTypes)); } inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am index 19f6313fb..d694d553b 100644 --- a/test/regress/regress0/sets/Makefile.am +++ b/test/regress/regress0/sets/Makefile.am @@ -39,6 +39,7 @@ TESTS = \ mar2014/smaller.smt2 \ mar2014/UniqueZipper.hs.1030minimized2.cvc4.smt2 \ mar2014/UniqueZipper.hs.1030minimized.cvc4.smt2 \ + rels/rel.cvc \ copy_check_heap_access_33_4.smt2 \ cvc-sample.cvc \ emptyset.smt2 \ diff --git a/test/regress/regress0/sets/rels/rel.cvc b/test/regress/regress0/sets/rels/rel.cvc new file mode 100644 index 000000000..27eb43b9f --- /dev/null +++ b/test/regress/regress0/sets/rels/rel.cvc @@ -0,0 +1,20 @@ +% EXPECT: sat +OPTION "logic" "ALL_SUPPORTED"; +IntPair: TYPE = [INT, INT]; +x : SET OF IntPair; +y : SET OF IntPair; +z : SET OF IntPair; +m: SET OF INT; +a: IntPair; +b: INT; + +ASSERT a IS_IN (y JOIN z); +ASSERT (y PRODUCT x) = (y PRODUCT z); +ASSERT x = ((y JOIN z) JOIN x); + +ASSERT x = y | z; +ASSERT x = y & z; +ASSERT y = y - z; +ASSERT z = (TRANSPOSE z); +ASSERT z = x | y; +CHECKSAT TRUE; -- 2.30.2