summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/Makefile.am2
-rw-r--r--src/expr/sepconst.cpp29
-rw-r--r--src/expr/sepconst.h72
-rw-r--r--src/parser/cvc/Cvc.g8
-rw-r--r--src/parser/smt2/Smt2.g12
-rw-r--r--src/parser/smt2/smt2.cpp1
-rw-r--r--src/printer/cvc/cvc_printer.cpp4
-rw-r--r--src/printer/smt2/smt2_printer.cpp7
-rw-r--r--src/theory/quantifiers/term_database.cpp2
-rw-r--r--src/theory/quantifiers/trigger.cpp2
-rw-r--r--src/theory/sep/kinds8
-rw-r--r--src/theory/sep/theory_sep_type_rules.h8
-rw-r--r--src/theory/sets/kinds4
-rw-r--r--src/theory/sets/theory_sets_private.cpp69
-rw-r--r--src/theory/sets/theory_sets_private.h3
-rw-r--r--src/theory/sets/theory_sets_rewriter.cpp30
-rw-r--r--src/theory/sets/theory_sets_type_rules.h21
-rw-r--r--test/regress/regress0/sets/Makefile.am3
-rw-r--r--test/regress/regress0/sets/univset-simp.smt221
19 files changed, 151 insertions, 155 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) {
diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am
index f4f921c43..a92c534a1 100644
--- a/test/regress/regress0/sets/Makefile.am
+++ b/test/regress/regress0/sets/Makefile.am
@@ -74,7 +74,8 @@ TESTS = \
card-7.smt2 \
abt-min.smt2 \
abt-te-exh.smt2 \
- abt-te-exh2.smt2
+ abt-te-exh2.smt2 \
+ univset-simp.smt2
EXTRA_DIST = $(TESTS)
diff --git a/test/regress/regress0/sets/univset-simp.smt2 b/test/regress/regress0/sets/univset-simp.smt2
new file mode 100644
index 000000000..5d10e27cb
--- /dev/null
+++ b/test/regress/regress0/sets/univset-simp.smt2
@@ -0,0 +1,21 @@
+(set-logic ALL)
+(set-info :status sat)
+
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun d () (Set Int))
+(declare-fun e () (Set Int))
+(declare-fun f () (Set Int))
+
+(declare-fun x () Int)
+
+(assert (not (member 0 a)))
+(assert (member 0 b))
+(assert (not (member 1 c)))
+(assert (member 2 d))
+(assert (= e (as univset (Set Int))))
+(assert (= f (compliment d)))
+(assert (not (member x (as univset (Set Int)))))
+
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback