diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-02-15 17:36:07 -0600 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-02-15 17:36:07 -0600 |
commit | 51fbe09f8b16ad0a49b2add0801b2963de08427e (patch) | |
tree | 4dbdd7df1a5b2181b7ac1f32725595b5be998d86 /src | |
parent | 371c0799fa38452c2186efd268c73a42c282c96e (diff) |
extended smt parser for the finite relations
fixed typing rules for relational terms
added a benchmark example for the theory of finite relations
Diffstat (limited to 'src')
-rw-r--r-- | src/parser/smt2/smt2.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 8 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 88 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rels.h | 16 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 45 |
6 files changed, 129 insertions, 34 deletions
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<bool>(true)), + d_falseNode(NodeManager::currentNM()->mkConst<bool>(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 <<std::endl; } } ++eqc_i; } - if( !firstTime ){ Debug("rels") << " "; } - Debug("rels") << "}" << std::endl; + if( !firstTime ){ Debug("rels-eqc") << " "; } + Debug("rels-eqc") << "}" << std::endl; ++eqcs_i; } } -} -} -} - - - + Node TheorySetsRels::reverseTuple(TNode tuple) { + // need to register the newly created tuple? + Assert(tuple.getType().isDatatype()); + std::vector<Node> 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 <Node, NodeHashFunction> 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<TypeNode> newTupleTypes; + std::vector<TypeNode> firstTupleTypes = firstRelType[0].getTupleTypes(); + std::vector<TypeNode> 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<TypeNode> tupleTypes; + std::vector<TypeNode> originalTupleTypes = setType[0].getTupleTypes(); + for(std::vector<TypeNode>::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) { |