theory/sets/theory_sets.h \
theory/sets/theory_sets_private.cpp \
theory/sets/theory_sets_private.h \
+ theory/sets/theory_sets_rels.cpp \
+ theory/sets/theory_sets_rels.h \
theory/sets/theory_sets_rewriter.cpp \
theory/sets/theory_sets_rewriter.h \
theory/sets/theory_sets_type_enumerator.h \
BVSGT_TOK = 'BVSGT';
BVSLE_TOK = 'BVSLE';
BVSGE_TOK = 'BVSGE';
+
+ // Relations
+ JOIN_TOK = 'JOIN';
+ TRANSPOSE_TOK = 'TRANSPOSE';
+ PRODUCT_TOK = 'PRODUCT';
+ TRANSCLOSURE_TOK = 'TRANSCLOSURE';
// Strings
case DIV_TOK:
case MOD_TOK: return 23;
case PLUS_TOK:
- case MINUS_TOK: return 24;
+ case MINUS_TOK:
+ case JOIN_TOK:
+ case TRANSPOSE_TOK:
+ case PRODUCT_TOK:
+ case TRANSCLOSURE_TOK: return 24;
case LEQ_TOK:
case LT_TOK:
case GEQ_TOK:
case OR_TOK: return kind::OR;
case XOR_TOK: return kind::XOR;
case AND_TOK: return kind::AND;
+
+ case PRODUCT_TOK: return kind::PRODUCT;
+ case JOIN_TOK: return kind::JOIN;
// comparisonBinop
case EQUAL_TOK: return kind::EQUAL;
| OR_TOK
| XOR_TOK
| AND_TOK
+ | JOIN_TOK
+ | PRODUCT_TOK
;
comparison[CVC4::Expr& f]
/* BV neg */
: BVNEG_TOK bvNegTerm[f]
{ f = MK_EXPR(CVC4::kind::BITVECTOR_NOT, f); }
+ | TRANSPOSE_TOK bvNegTerm[f]
+ { f = MK_EXPR(CVC4::kind::TRANSPOSE, f); }
+ | TRANSCLOSURE_TOK bvNegTerm[f]
+ { f = MK_EXPR(CVC4::kind::TRANSCLOSURE, f); }
| postfixTerm[f]
;
op << "IS_IN";
opType = INFIX;
break;
+ case kind::PRODUCT:
+ op << "PRODUCT";
+ opType = INFIX;
+ break;
+ case kind::JOIN:
+ op << "JOIN";
+ opType = INFIX;
+ break;
+ case kind::TRANSPOSE:
+ op << "TRANSPOSE";
+ opType = PREFIX;
+ break;
+ case kind::TRANSCLOSURE:
+ op << "TRANSCLOSURE";
+ opType = PREFIX;
+ break;
case kind::SINGLETON:
out << "{";
toStream(out, n[0], depth, types, false);
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)"
+operator JOIN 2 "set join"
+operator PRODUCT 2 "set cartesian product"
+operator TRANSPOSE 1 "set transpose"
+operator TRANSCLOSURE 1 "set transitive closure"
+
typerule UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule
typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
typerule INSERT ::CVC4::theory::sets::InsertTypeRule
+typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
+typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
+typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule
+typerule TRANSCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule
+
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
+construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule
+construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule
+construle TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule
+construle TRANSCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule
+
endtheory
// and that leads to conflict (externally).
if(d_conflict) { return; }
Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
+
+ d_rels->check(level);
}
if( (level == Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
d_modelCache(c),
d_ccg_i(c),
d_ccg_j(c),
- d_scrutinize(NULL)
+ d_scrutinize(NULL),
+ d_rels(NULL)
{
d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
+ d_rels = new TheorySetsRels(&d_equalityEngine);
d_equalityEngine.addFunctionKind(kind::UNION);
d_equalityEngine.addFunctionKind(kind::INTERSECTION);
TheorySetsPrivate::~TheorySetsPrivate()
{
delete d_termInfoManager;
+ delete d_rels;
if( Debug.isOn("sets-scrutinize") ) {
Assert(d_scrutinize != NULL);
delete d_scrutinize;
#include "theory/theory.h"
#include "theory/uf/equality_engine.h"
#include "theory/sets/term_info.h"
+#include "theory/sets/theory_sets_rels.h"
namespace CVC4 {
namespace theory {
private:
TheorySets& d_external;
+ TheorySetsRels* d_rels;
class Statistics {
public:
--- /dev/null
+/********************* */
+/*! \file theory_sets_rels.cpp
+ ** \verbatim
+ ** Original author: Paul Meng
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Extension to Sets theory.
+ **/
+
+#include "theory/sets/theory_sets_rels.h"
+
+//#include "expr/emptyset.h"
+//#include "options/sets_options.h"
+//#include "smt/smt_statistics_registry.h"
+//#include "theory/sets/expr_patterns.h" // ONLY included here
+//#include "theory/sets/scrutinize.h"
+//#include "theory/sets/theory_sets.h"
+//#include "theory/theory_model.h"
+//#include "util/result.h"
+
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+ TheorySetsRels::TheorySetsRels(eq::EqualityEngine* eq):
+ d_eqEngine(eq)
+ {
+ d_eqEngine->addFunctionKind(kind::PRODUCT);
+ d_eqEngine->addFunctionKind(kind::JOIN);
+ d_eqEngine->addFunctionKind(kind::TRANSPOSE);
+ d_eqEngine->addFunctionKind(kind::TRANSCLOSURE);
+ }
+
+ TheorySetsRels::TheorySetsRels::~TheorySetsRels() {}
+
+ void TheorySetsRels::TheorySetsRels::check(Theory::Effort level) {
+
+ Debug("rels") << "\nStart iterating equivalence class......\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") << " : { ";
+ eq::EqClassIterator eqc_i = eq::EqClassIterator( r, d_eqEngine );
+ while( !eqc_i.isFinished() ){
+ TNode n = (*eqc_i);
+ if( r!=n ){
+ if( firstTime ){
+ Debug("rels") << 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;
+ }
+ }
+ ++eqc_i;
+ }
+ if( !firstTime ){ Debug("rels") << " "; }
+ Debug("rels") << "}" << std::endl;
+ ++eqcs_i;
+ }
+ }
+}
+}
+}
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null
+/********************* */
+/*! \file theory_sets_rels.h
+ ** \verbatim
+ ** Original author: Paul Meng
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Sets theory implementation.
+ **
+ ** Extension to Sets theory.
+ **/
+
+#ifndef SRC_THEORY_SETS_THEORY_SETS_RELS_H_
+#define SRC_THEORY_SETS_THEORY_SETS_RELS_H_
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsRels {
+
+public:
+ TheorySetsRels(eq::EqualityEngine*);
+
+ ~TheorySetsRels();
+
+ void check(Theory::Effort);
+
+private:
+
+ eq::EqualityEngine *d_eqEngine;
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+
+
+#endif /* SRC_THEORY_SETS_THEORY_SETS_RELS_H_ */
}
};/* struct InsertTypeRule */
+struct RelBinaryOperatorTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::PRODUCT ||
+ n.getKind() == kind::JOIN);
+
+ TypeNode firstRelType = n[0].getType(check);
+ TypeNode secondRelType = n[1].getType(check);
+
+ 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
+ if(n.getKind() == kind::JOIN) {
+ if((firstRelType[0].getNumChildren() == 1) && (secondRelType[0].getNumChildren() == 1)) {
+ throw TypeCheckingExceptionPrivate(n, " Join operates on two unary relations");
+ }
+ }
+ }
+
+ Assert(firstRelType == secondRelType);
+ return firstRelType;
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ Assert(n.getKind() == kind::JOIN ||
+ n.getKind() == kind::PRODUCT);
+ return false;
+ }
+};/* struct RelBinaryOperatorTypeRule */
+
+struct RelTransposeTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ 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");
+ }
+ return setType;
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ //Assert(n.getKind() == kind::TRANSCLOSURE);
+ return false;
+ }
+};/* struct RelTransposeTypeRule */
+
+struct RelTransClosureTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::TRANSCLOSURE);
+ TypeNode setType = n[0].getType(check);
+ if(check) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-rel");
+ }
+ if(setType[0].getNumChildren() != 2) {
+ throw TypeCheckingExceptionPrivate(n, " transitive closure operates on non-binary relations");
+ }
+ }
+ return setType;
+ }
+
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ Assert(n.getKind() == kind::TRANSCLOSURE);
+ return true;
+ }
+};/* struct RelTransClosureTypeRule */
+
struct SetsProperties {
inline static Cardinality computeCardinality(TypeNode type) {
projects / cvc5.git / commitdiff