diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:03 -0600 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-06 09:39:20 -0600 |
commit | d73fdfe7e1fe071670a7e5f843c7609db290b63e (patch) | |
tree | ff8ad52565f6a149689668f74957292486b2eeab /src | |
parent | 5f096cbd59afa98e8b3c7e7e7aa0b6df3c7e01b0 (diff) |
Support for set compliment and universe set. Simplify approach for sep.nil nodes.
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/Makefile.am | 2 | ||||
-rw-r--r-- | src/expr/sepconst.cpp | 29 | ||||
-rw-r--r-- | src/expr/sepconst.h | 72 | ||||
-rw-r--r-- | src/parser/cvc/Cvc.g | 8 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 12 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 1 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 4 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 7 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/sep/kinds | 8 | ||||
-rw-r--r-- | src/theory/sep/theory_sep_type_rules.h | 8 | ||||
-rw-r--r-- | src/theory/sets/kinds | 4 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 69 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.h | 3 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_rewriter.cpp | 30 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_type_rules.h | 21 |
17 files changed, 128 insertions, 154 deletions
diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 9dcbc3b4b..c04de4421 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -40,8 +40,6 @@ libexpr_la_SOURCES = \ pickle_data.h \ pickler.cpp \ pickler.h \ - sepconst.cpp \ - sepconst.h \ symbol_table.cpp \ symbol_table.h \ type.cpp \ diff --git a/src/expr/sepconst.cpp b/src/expr/sepconst.cpp deleted file mode 100644 index 7646b90d3..000000000 --- a/src/expr/sepconst.cpp +++ /dev/null @@ -1,29 +0,0 @@ -/********************* */ -/*! \file sepconst.cpp - ** \verbatim - ** Original author: Andrew Reynolds - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "expr/sepconst.h" -#include <iostream> - -using namespace std; - -namespace CVC4 { - -std::ostream& operator<<(std::ostream& out, const NilRef& asa) { - return out << "(nil " << asa.getType() << ")"; -} - -}/* CVC4 namespace */ diff --git a/src/expr/sepconst.h b/src/expr/sepconst.h deleted file mode 100644 index 9f86c7efc..000000000 --- a/src/expr/sepconst.h +++ /dev/null @@ -1,72 +0,0 @@ -/********************* */ -/*! \file sepconst.h - ** \verbatim - ** Original author: Andrew Reynolds - ** 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 [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "cvc4_public.h" - -#pragma once - -namespace CVC4 { - // messy; Expr needs NilRef (because it's the payload of a - // CONSTANT-kinded expression), and NilRef needs Expr. - class CVC4_PUBLIC NilRef; - //class CVC4_PUBLIC EmpStar; -}/* CVC4 namespace */ - -#include "expr/expr.h" -#include "expr/type.h" -#include <iostream> - -namespace CVC4 { - -class CVC4_PUBLIC NilRef { - const Type d_type; - NilRef() { } -public: - NilRef(Type refType):d_type(refType) { } - - ~NilRef() throw() { - } - Type getType() const { return d_type; } - bool operator==(const NilRef& es) const throw() { - return d_type == es.d_type; - } - bool operator!=(const NilRef& es) const throw() { - return !(*this == es); - } - bool operator<(const NilRef& es) const throw() { - return d_type < es.d_type; - } - bool operator<=(const NilRef& es) const throw() { - return d_type <= es.d_type; - } - bool operator>(const NilRef& es) const throw() { - return !(*this <= es); - } - bool operator>=(const NilRef& es) const throw() { - return !(*this < es); - } -};/* class NilRef */ - -std::ostream& operator<<(std::ostream& out, const NilRef& es) CVC4_PUBLIC; - -struct CVC4_PUBLIC NilRefHashFunction { - inline size_t operator()(const NilRef& es) const { - return TypeHashFunction()(es.getType()); - } -};/* struct NilRefHashFunction */ - -}/* CVC4 namespace */ diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g index 3a8f3a794..0655359a9 100644 --- a/src/parser/cvc/Cvc.g +++ b/src/parser/cvc/Cvc.g @@ -245,6 +245,7 @@ tokens { SETS_CARD_TOK = 'CARD'; FMF_CARD_TOK = 'HAS_CARD'; + UNIVSET_TOK = 'UNIVERSE'; // these are parsed by special NUMBER_OR_RANGEOP rule, below DECIMAL_LITERAL; @@ -440,6 +441,7 @@ Expr createPrecedenceTree(Parser* parser, ExprManager* em, Expr rhs = createPrecedenceTree(parser, em, expressions, operators, pivot + 1, stopIndex); switch(k) { + case kind::NOT : if(lhs.getType().isSet()) { k = kind::COMPLIMENT; } break; case kind::LEQ : if(lhs.getType().isSet()) { k = kind::SUBSET; } break; case kind::MINUS : if(lhs.getType().isSet()) { k = kind::SETMINUS; } break; case kind::BITVECTOR_AND: if(lhs.getType().isSet()) { k = kind::INTERSECTION; } break; @@ -1832,6 +1834,8 @@ postfixTerm[CVC4::Expr& f] f = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v); } else if(f.getKind() == CVC4::kind::EMPTYSET && t.isSet()) { f = MK_CONST(CVC4::EmptySet(t)); + } else if(f.getKind() == CVC4::kind::UNIVERSE_SET && t.isSet()) { + f = EXPR_MANAGER->mkUniqueVar(t, kind::UNIVERSE_SET); } else { if(f.getType() != t) { PARSER_STATE->parseError("Type ascription not satisfied."); @@ -2065,6 +2069,10 @@ simpleTerm[CVC4::Expr& f] /* empty set literal */ | LBRACE RBRACE { f = MK_CONST(EmptySet(Type())); } + | UNIVSET_TOK + { //booleanType is placeholder + f = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); + } /* finite set literal */ | LBRACE formula[f] { args.push_back(f); } diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 735c2b2f1..92becbc68 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1775,7 +1775,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] Debug("parser") << "Empty set encountered: " << f << " " << f2 << " " << type << std::endl; expr = MK_CONST( ::CVC4::EmptySet(type) ); - } else if(f.getKind() == CVC4::kind::SEP_NIL_REF) { + } else if(f.getKind() == CVC4::kind::UNIVERSE_SET) { + expr = EXPR_MANAGER->mkUniqueVar(type, kind::UNIVERSE_SET); + } else if(f.getKind() == CVC4::kind::SEP_NIL) { //We don't want the nil reference to be a constant: for instance, it //could be of type Int but is not a const rational. However, the //expression has 0 children. So we convert to a SEP_NIL variable. @@ -2095,8 +2097,13 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | EMPTYSET_TOK { expr = MK_CONST( ::CVC4::EmptySet(Type())); } + | UNIVSET_TOK + { //booleanType is placeholder here since we don't have type info without type annotation + expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::UNIVERSE_SET); } + | NILREF_TOK - { expr = MK_CONST( ::CVC4::NilRef(Type())); } + { //booleanType is placeholder here since we don't have type info without type annotation + expr = EXPR_MANAGER->mkUniqueVar(EXPR_MANAGER->booleanType(), kind::SEP_NIL); } // NOTE: Theory constants go here ; @@ -2874,6 +2881,7 @@ FMFCARDVAL_TOK : 'fmf.card.val'; INST_CLOSURE_TOK : 'inst-closure'; EMPTYSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'emptyset'; +UNIVSET_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SETS) }? 'univset'; NILREF_TOK: { PARSER_STATE->isTheoryEnabled(Smt2::THEORY_SEP) }? 'sep.nil'; // Other set theory operators are not // tokenized and handled directly when diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e1b824ba3..88b2479ea 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -236,6 +236,7 @@ void Smt2::addTheory(Theory theory) { addOperator(kind::SINGLETON, "singleton"); addOperator(kind::INSERT, "insert"); addOperator(kind::CARD, "card"); + addOperator(kind::COMPLIMENT, "compliment"); break; case THEORY_DATATYPES: diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 01978b2e5..e0c434d5a 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -780,6 +780,10 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo op << "IS_IN"; opType = INFIX; break; + case kind::COMPLIMENT: + op << "NOT"; + opType = PREFIX; + break; case kind::PRODUCT: op << "PRODUCT"; opType = INFIX; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index a7add27f8..b3fcaf24b 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -120,6 +120,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, if( n.getKind() == kind::SEP_NIL ){ out << "(as sep.nil " << n.getType() << ")"; return; + }else if( n.getKind() == kind::UNIVERSE_SET ){ + out << "(as univset " << n.getType() << ")"; + return; }else{ string s; if(n.getAttribute(expr::VarNameAttr(), s)) { @@ -514,7 +517,8 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::SUBSET: case kind::MEMBER: case kind::SET_TYPE: - case kind::SINGLETON: out << smtKindString(k) << " "; break; + case kind::SINGLETON: + case kind::COMPLIMENT:out << smtKindString(k) << " "; break; // fp theory case kind::FLOATINGPOINT_FP: @@ -803,6 +807,7 @@ static string smtKindString(Kind k) throw() { case kind::SET_TYPE: return "Set"; case kind::SINGLETON: return "singleton"; case kind::INSERT: return "insert"; + case kind::COMPLIMENT: return "compliment"; // fp theory case kind::FLOATINGPOINT_FP: return "fp"; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index d394c8fef..6b4b67a26 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -137,7 +137,7 @@ Node TermDb::getTypeGroundTerm( TypeNode tn, unsigned i ) { Node TermDb::getMatchOperator( Node n ) { Kind k = n.getKind(); //datatype operators may be parametric, always assume they are - if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || + if( k==SELECT || k==STORE || k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || k==SEP_PTO ){ //since it is parametric, use a particular one as op TypeNode tn = n[0].getType(); diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index cca6543b6..efd80a83c 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -353,7 +353,7 @@ bool Trigger::isAtomicTrigger( Node n ){ bool Trigger::isAtomicTriggerKind( Kind k ) { return k==APPLY_UF || k==SELECT || k==STORE || k==APPLY_CONSTRUCTOR || k==APPLY_SELECTOR_TOTAL || k==APPLY_TESTER || - k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || + k==UNION || k==INTERSECTION || k==SUBSET || k==SETMINUS || k==MEMBER || k==SINGLETON || k==COMPLIMENT || k==SEP_PTO || k==BITVECTOR_TO_NAT || k==INT_TO_BITVECTOR; } diff --git a/src/theory/sep/kinds b/src/theory/sep/kinds index 5cd9093f4..358c63f55 100644 --- a/src/theory/sep/kinds +++ b/src/theory/sep/kinds @@ -12,13 +12,6 @@ properties check propagate presolve getNextDecisionRequest rewriter ::CVC4::theory::sep::TheorySepRewriter "theory/sep/theory_sep_rewriter.h" -# constants -constant SEP_NIL_REF \ - ::CVC4::NilRef \ - ::CVC4::NilRefHashFunction \ - "expr/sepconst.h" \ - "the nil reference constant; payload is an instance of the CVC4::NilRef class" - variable SEP_NIL "separation nil" operator SEP_EMP 2 "separation empty heap" @@ -27,7 +20,6 @@ operator SEP_STAR 2: "separation star" operator SEP_WAND 2 "separation magic wand" operator SEP_LABEL 2 "separation label (internal use only)" -typerule SEP_NIL_REF ::CVC4::theory::sep::SepNilRefTypeRule typerule SEP_EMP ::CVC4::theory::sep::SepEmpTypeRule typerule SEP_PTO ::CVC4::theory::sep::SepPtoTypeRule typerule SEP_STAR ::CVC4::theory::sep::SepStarTypeRule diff --git a/src/theory/sep/theory_sep_type_rules.h b/src/theory/sep/theory_sep_type_rules.h index 7d4eb303e..23e725a25 100644 --- a/src/theory/sep/theory_sep_type_rules.h +++ b/src/theory/sep/theory_sep_type_rules.h @@ -25,14 +25,6 @@ namespace CVC4 { namespace theory { namespace sep { -class SepNilRefTypeRule { -public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) - throw (TypeCheckingExceptionPrivate, AssertionException) { - return TypeNode::fromType( n.getConst<NilRef>().getType() ); - } -}; - class SepEmpTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds index c92eab4bd..53905e47f 100644 --- a/src/theory/sets/kinds +++ b/src/theory/sets/kinds @@ -43,6 +43,7 @@ operator MEMBER 2 "set membership predicate; first parameter a member of 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 CARD 1 "set cardinality operator" +operator COMPLIMENT 1 "set compliment (with respect to finite universe)" operator JOIN 2 "set join" operator PRODUCT 2 "set cartesian product" @@ -58,12 +59,14 @@ typerule SINGLETON ::CVC4::theory::sets::SingletonTypeRule typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule typerule INSERT ::CVC4::theory::sets::InsertTypeRule typerule CARD ::CVC4::theory::sets::CardTypeRule +typerule COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule typerule JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule typerule TRANSPOSE ::CVC4::theory::sets::RelTransposeTypeRule typerule TCLOSURE ::CVC4::theory::sets::RelTransClosureTypeRule +variable UNIVERSE_SET "(finite) universe set, all set variables must be interpreted as subsets of it." construle UNION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle INTERSECTION ::CVC4::theory::sets::SetsBinaryOperatorTypeRule @@ -71,6 +74,7 @@ construle SETMINUS ::CVC4::theory::sets::SetsBinaryOperatorTypeRule construle SINGLETON ::CVC4::theory::sets::SingletonTypeRule construle INSERT ::CVC4::theory::sets::InsertTypeRule construle CARD ::CVC4::theory::sets::CardTypeRule +construle COMPLIMENT ::CVC4::theory::sets::ComplimentTypeRule construle JOIN ::CVC4::theory::sets::RelBinaryOperatorTypeRule construle PRODUCT ::CVC4::theory::sets::RelBinaryOperatorTypeRule diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index e78575791..e71333075 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -508,6 +508,7 @@ void TheorySetsPrivate::fullEffortCheck(){ d_set_eqc.clear(); d_set_eqc_list.clear(); d_eqc_emptyset.clear(); + d_eqc_univset.clear(); d_eqc_singleton.clear(); d_congruent.clear(); d_nvar_sets.clear(); @@ -557,7 +558,8 @@ void TheorySetsPrivate::fullEffortCheck(){ Assert( false ); } } - }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION || n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET ){ + }else if( n.getKind()==kind::SINGLETON || n.getKind()==kind::UNION || n.getKind()==kind::INTERSECTION || + n.getKind()==kind::SETMINUS || n.getKind()==kind::EMPTYSET || n.getKind()==kind::UNIVERSE_SET ){ if( n.getKind()==kind::SINGLETON ){ //singleton lemma getProxy( n ); @@ -571,6 +573,8 @@ void TheorySetsPrivate::fullEffortCheck(){ } }else if( n.getKind()==kind::EMPTYSET ){ d_eqc_emptyset[tn] = eqc; + }else if( n.getKind()==kind::UNIVERSE_SET ){ + d_eqc_univset[tn] = eqc; }else{ Node r1 = d_equalityEngine.getRepresentative( n[0] ); Node r2 = d_equalityEngine.getRepresentative( n[1] ); @@ -641,8 +645,9 @@ void TheorySetsPrivate::fullEffortCheck(){ checkUpwardsClosure( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ + std::vector< Node > intro_sets; + //for cardinality if( d_card_enabled ){ - //for cardinality checkCardBuildGraph( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ @@ -652,28 +657,27 @@ void TheorySetsPrivate::fullEffortCheck(){ checkCardCycles( lemmas ); flushLemmas( lemmas ); if( !hasProcessed() ){ - std::vector< Node > intro_sets; checkNormalForms( lemmas, intro_sets ); flushLemmas( lemmas ); - if( !hasProcessed() ){ - checkDisequalities( lemmas ); - flushLemmas( lemmas ); - if( !hasProcessed() && !intro_sets.empty() ){ - Assert( intro_sets.size()==1 ); - Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; - Trace("sets-intro") << " Actual Intro : "; - debugPrintSet( intro_sets[0], "sets-nf" ); - Trace("sets-nf") << std::endl; - Node k = getProxy( intro_sets[0] ); - d_sentLemma = true; - } - } } } } - }else{ + } + if( !hasProcessed() ){ checkDisequalities( lemmas ); flushLemmas( lemmas ); + if( !hasProcessed() ){ + //introduce splitting on venn regions (absolute last resort) + if( d_card_enabled && !hasProcessed() && !intro_sets.empty() ){ + Assert( intro_sets.size()==1 ); + Trace("sets-intro") << "Introduce term : " << intro_sets[0] << std::endl; + Trace("sets-intro") << " Actual Intro : "; + debugPrintSet( intro_sets[0], "sets-nf" ); + Trace("sets-nf") << std::endl; + Node k = getProxy( intro_sets[0] ); + d_sentLemma = true; + } + } } } } @@ -682,7 +686,6 @@ void TheorySetsPrivate::fullEffortCheck(){ Trace("sets") << "----- End full effort check, conflict=" << d_conflict << ", lemma=" << d_sentLemma << std::endl; } - void TheorySetsPrivate::checkDownwardsClosure( std::vector< Node >& lemmas ) { Trace("sets") << "Downwards closure..." << std::endl; //downwards closure @@ -837,6 +840,26 @@ void TheorySetsPrivate::checkUpwardsClosure( std::vector< Node >& lemmas ) { } } } + if( !hasProcessed() ){ + //universal sets + Trace("sets-debug") << "Check universe sets..." << std::endl; + //all elements must be in universal set + for( std::map< Node, std::map< Node, Node > >::iterator it = d_pol_mems[0].begin(); it != d_pol_mems[0].end(); ++it ){ + TypeNode tn = it->first.getType(); + std::map< TypeNode, Node >::iterator itu = d_eqc_univset.find( tn ); + if( itu==d_eqc_univset.end() || itu->second!=it->first ){ + Node u = getUnivSet( tn ); + for( std::map< Node, Node >::iterator it2 = it->second.begin(); it2 != it->second.end(); ++it2 ){ + Node mem = it2->second; + Node fact = NodeManager::currentNM()->mkNode( kind::MEMBER, mem[0], u ); + assertInference( fact, mem, lemmas, "upuniv" ); + if( d_conflict ){ + return; + } + } + } + } + } } void TheorySetsPrivate::checkDisequalities( std::vector< Node >& lemmas ) { @@ -1493,6 +1516,16 @@ Node TheorySetsPrivate::getEmptySet( TypeNode tn ) { return it->second; } } +Node TheorySetsPrivate::getUnivSet( TypeNode tn ) { + std::map< TypeNode, Node >::iterator it = d_univset.find( tn ); + if( it==d_univset.end() ){ + Node n = NodeManager::currentNM()->mkUniqueVar(tn, kind::UNIVERSE_SET); + d_univset[tn] = n; + return n; + }else{ + return it->second; + } +} bool TheorySetsPrivate::hasLemmaCached( Node lem ) { return d_lemmas_produced.find(lem)!=d_lemmas_produced.end(); diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 1c9a7e22a..6d7b57cc6 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -79,6 +79,7 @@ private: Node getProxy( Node n ); Node getCongruent( Node n ); Node getEmptySet( TypeNode tn ); + Node getUnivSet( TypeNode tn ); bool hasLemmaCached( Node lem ); bool hasProcessed(); @@ -119,8 +120,10 @@ private: std::map< Node, bool > d_set_eqc_relevant; std::map< Node, std::vector< Node > > d_set_eqc_list; std::map< TypeNode, Node > d_eqc_emptyset; + std::map< TypeNode, Node > d_eqc_univset; std::map< Node, Node > d_eqc_singleton; std::map< TypeNode, Node > d_emptyset; + std::map< TypeNode, Node > d_univset; std::map< Node, Node > d_congruent; std::map< Node, std::vector< Node > > d_nvar_sets; std::map< Node, std::map< Node, Node > > d_pol_mems[2]; diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp index aaf71e8fc..da4f8fb7a 100644 --- a/src/theory/sets/theory_sets_rewriter.cpp +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -219,7 +219,9 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::EMPTYSET) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; - return RewriteResponse(REWRITE_DONE, node[0]); + return RewriteResponse(REWRITE_AGAIN, node[0]); + }else if( node[1].getKind() == kind::UNIVERSE_SET ){ + return RewriteResponse(REWRITE_AGAIN, NodeManager::currentNM()->mkConst(EmptySet(node[1].getType().toType()))); } else if(node[0].isConst() && node[1].isConst()) { std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -237,11 +239,11 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { case kind::INTERSECTION: { if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; - return RewriteResponse(REWRITE_DONE, node[0]); - } else if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[0]); - } else if(node[1].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[1]); + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[1]); } else if(node[0].isConst() && node[1].isConst()) { std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -276,11 +278,11 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { // NOTE: case where it is CONST is taken care of at the top if(node[0] == node[1]) { Trace("sets-postrewrite") << "Sets::postRewrite returning " << node[0] << std::endl; - return RewriteResponse(REWRITE_DONE, node[0]); - } else if(node[0].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[1]); - } else if(node[1].getKind() == kind::EMPTYSET) { - return RewriteResponse(REWRITE_DONE, node[0]); + return RewriteResponse(REWRITE_AGAIN, node[0]); + } else if(node[0].getKind() == kind::EMPTYSET || node[1].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[1]); + } else if(node[1].getKind() == kind::EMPTYSET || node[0].getKind() == kind::UNIVERSE_SET) { + return RewriteResponse(REWRITE_AGAIN, node[0]); } else if(node[0].isConst() && node[1].isConst()) { std::set<Node> left = NormalForm::getElementsFromNormalConstant(node[0]); std::set<Node> right = NormalForm::getElementsFromNormalConstant(node[1]); @@ -303,7 +305,11 @@ RewriteResponse TheorySetsRewriter::postRewrite(TNode node) { } break; }//kind::UNION - + case kind::COMPLIMENT: { + Node univ = NodeManager::currentNM()->mkUniqueVar( node[0].getType(), kind::UNIVERSE_SET ); + return RewriteResponse( REWRITE_AGAIN, NodeManager::currentNM()->mkNode( kind::SETMINUS, univ, node[0] ) ); + } + break; case kind::CARD: { if(node[0].isConst()) { std::set<Node> elements = NormalForm::getElementsFromNormalConstant(node[0]); diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h index 89d481746..66e06b038 100644 --- a/src/theory/sets/theory_sets_type_rules.h +++ b/src/theory/sets/theory_sets_type_rules.h @@ -155,6 +155,27 @@ struct CardTypeRule { } };/* struct CardTypeRule */ +struct ComplimentTypeRule { + inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) + throw (TypeCheckingExceptionPrivate, AssertionException) { + Assert(n.getKind() == kind::COMPLIMENT); + TypeNode setType = n[0].getType(check); + if( check ) { + if(!setType.isSet()) { + throw TypeCheckingExceptionPrivate(n, "compliment operates on a set, non-set object found"); + } + } + return setType; + } + + inline static bool computeIsConst(NodeManager* nodeManager, TNode n) { + Assert(n.getKind() == kind::COMPLIMENT); + return false; + } +};/* struct ComplimentTypeRule */ + + + struct InsertTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) throw (TypeCheckingExceptionPrivate, AssertionException) { |