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;
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
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";
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);
#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
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);
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);
+ }
+}
+}
+}
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
+#include "context/cdhashset.h"
namespace CVC4 {
namespace theory {
class TheorySetsRels {
public:
- TheorySetsRels(eq::EqualityEngine*);
+ TheorySetsRels(context::Context* c,
+ context::UserContext* u,
+ eq::EqualityEngine*);
~TheorySetsRels();
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 */
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");
}
}
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) {
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) {
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 \
--- /dev/null
+% 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;
projects / cvc5.git / commitdiff