/debug/
/personal.conf
/personal.mk
+/antlr-3.4
AM_CXXFLAGS = -Wall -Wno-unknown-pragmas -Wno-parentheses $(FLAG_VISIBILITY_HIDDEN)
SUBDIRS = lib options expr util prop/minisat prop/bvminisat . parser compat bindings main
-THEORIES = builtin booleans uf arith bv arrays datatypes strings quantifiers rewriterules idl
+THEORIES = builtin booleans uf arith bv arrays datatypes sets strings quantifiers rewriterules idl
lib_LTLIBRARIES = libcvc4.la
theory/datatypes/theory_datatypes.h \
theory/datatypes/datatypes_rewriter.h \
theory/datatypes/theory_datatypes.cpp \
+ theory/sets/theory_sets.h \
+ theory/sets/theory_sets.cpp \
+ theory/sets/theory_sets_private.h \
+ theory/sets/theory_sets_private.cpp \
+ theory/sets/theory_sets_rewriter.h \
+ theory/sets/theory_sets_rewriter.cpp \
+ theory/sets/theory_sets_type_rules.h \
theory/strings/theory_strings.h \
theory/strings/theory_strings.cpp \
theory/strings/theory_strings_rewriter.h \
theory/idl/kinds \
theory/builtin/kinds \
theory/datatypes/kinds \
+ theory/sets/kinds \
theory/strings/kinds \
theory/arrays/kinds \
theory/quantifiers/kinds \
return super::size();
}
+ bool empty() const {
+ return super::empty();
+ }
+
bool insert(const V& v) {
return super::insert_safe(v, true);
}
return ArrayType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkArrayType(*indexType.d_typeNode, *constituentType.d_typeNode))));
}
+SetType ExprManager::mkSetType(Type elementType) const {
+ NodeManagerScope nms(d_nodeManager);
+ return SetType(Type(d_nodeManager, new TypeNode(d_nodeManager->mkSetType(*elementType.d_typeNode))));
+}
+
DatatypeType ExprManager::mkDatatypeType(const Datatype& datatype) {
// Not worth a special implementation; this doesn't need to be fast
// code anyway.
/** Make the type of arrays with the given parameterization. */
ArrayType mkArrayType(Type indexType, Type constituentType) const;
+ /** Make the type of set with the given parameterization. */
+ SetType mkSetType(Type elementType) const;
+
/** Make a type representing the given datatype. */
DatatypeType mkDatatypeType(const Datatype& datatype);
/** Make the type of arrays with the given parameterization */
inline TypeNode mkArrayType(TypeNode indexType, TypeNode constituentType);
+ /** Make the type of arrays with the given parameterization */
+ inline TypeNode mkSetType(TypeNode elementType);
+
/** Make a type representing a constructor with the given parameterization */
TypeNode mkConstructorType(const DatatypeConstructor& constructor, TypeNode range);
return mkTypeNode(kind::ARRAY_TYPE, indexType, constituentType);
}
+inline TypeNode NodeManager::mkSetType(TypeNode elementType) {
+ CheckArgument(!elementType.isNull(), elementType,
+ "unexpected NULL element type");
+ // TODO: Confirm meaning of isFunctionLike(). --K
+ CheckArgument(!elementType.isFunctionLike(), elementType,
+ "cannot store function-like types in sets");
+ Debug("sets") << "making sets type " << elementType << std::endl;
+ return mkTypeNode(kind::SET_TYPE, elementType);
+}
+
inline TypeNode NodeManager::mkSelectorType(TypeNode domain, TypeNode range) {
CheckArgument(!domain.isFunctionLike(), domain,
"cannot create higher-order function types");
return d_typeNode->isArray();
}
+/** Is this a Set type? */
+bool Type::isSet() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isSet();
+}
+
/** Is this a sort kind */
bool Type::isSort() const {
NodeManagerScope nms(d_nodeManager);
CheckArgument(isNull() || isArray(), this);
}
+SetType::SetType(const Type& t) throw(IllegalArgumentException) :
+ Type(t) {
+ CheckArgument(isNull() || isSet(), this);
+}
+
SortType::SortType(const Type& t) throw(IllegalArgumentException) :
Type(t) {
CheckArgument(isNull() || isSort(), this);
return makeType(d_typeNode->getArrayConstituentType());
}
+Type SetType::getElementType() const {
+ return makeType(d_typeNode->getSetElementType());
+}
+
DatatypeType ConstructorType::getRangeType() const {
return DatatypeType(makeType(d_typeNode->getConstructorRangeType()));
}
class StringType;
class BitVectorType;
class ArrayType;
+class SetType;
class DatatypeType;
class ConstructorType;
class SelectorType;
bool isArray() const;
/**
+ * Is this a Set type?
+ * @return true if the type is a Set type
+ */
+ bool isSet() const;
+
+ /**
* Is this a datatype type?
* @return true if the type is a datatype type
*/
Type getConstituentType() const;
};/* class ArrayType */
+/**
+ * Class encapsulating an set type.
+ */
+class CVC4_PUBLIC SetType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ SetType(const Type& type = Type()) throw(IllegalArgumentException);
+
+ /** Get the index type */
+ Type getElementType() const;
+};/* class SetType */
+
/**
* Class encapsulating a user-defined sort.
*/
/** Is this an array type? */
bool isArray() const;
+ /** Is this a Set type? */
+ bool isSet() const;
+
/** Get the index type (for array types) */
TypeNode getArrayIndexType() const;
/** Get the return type (for constructor types) */
TypeNode getConstructorRangeType() const;
+ /** Get the element type (for set types) */
+ TypeNode getSetElementType() const;
+
/**
* Is this a function type? Function-like things (e.g. datatype
* selectors) that aren't actually functions are NOT considered
return (*this)[getNumChildren()-1];
}
+inline bool TypeNode::isSet() const {
+ return getKind() == kind::SET_TYPE;
+}
+
+inline TypeNode TypeNode::getSetElementType() const {
+ Assert(isSet());
+ return (*this)[0];
+}
+
inline bool TypeNode::isFunction() const {
return getKind() == kind::FUNCTION_TYPE;
}
../parser/options.cpp \
../parser/options.h \
../theory/idl/options.cpp \
- ../theory/idl/options.h
+ ../theory/idl/options.h \
+ ../theory/sets/options.cpp \
+ ../theory/sets/options.h
OPTIONS_FILES = \
$(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS)))
../parser/options.cpp \
../parser/options.h \
../theory/idl/options.cpp \
- ../theory/idl/options.h
+ ../theory/idl/options.h \
+ ../theory/sets/options.cpp \
+ ../theory/sets/options.h
BUILT_SOURCES = \
exprs-builts \
MK_CONST(AscriptionType(dtc.getSpecializedConstructorType(type))), f.getOperator() ));
v.insert(v.end(), f.begin(), f.end());
expr = MK_EXPR(CVC4::kind::APPLY_CONSTRUCTOR, v);
+ } else if(f.getKind() == CVC4::kind::EMPTYSET) {
+ Debug("parser") << "Empty set encountered: " << f << " "
+ << f2 << " " << type << std::endl;
+ // TODO: what is f2 about, should we add some assertions?
+ expr = MK_CONST( ::CVC4::EmptySet(type) );
} else {
if(f.getType() != type) {
PARSER_STATE->parseError("Type ascription not satisfied.");
| str[s,false]
{ expr = MK_CONST( ::CVC4::String(s) ); }
+ | EMPTYSET_TOK
+ { expr = MK_CONST( ::CVC4::EmptySet()); }
+
// NOTE: Theory constants go here
;
| REPLUS_TOK { $kind = CVC4::kind::REGEXP_PLUS; }
| REOPT_TOK { $kind = CVC4::kind::REGEXP_OPT; }
| RERANGE_TOK { $kind = CVC4::kind::REGEXP_RANGE; }
+ | SETUNION_TOK { $kind = CVC4::kind::UNION; }
+ | SETINT_TOK { $kind = CVC4::kind::INTERSECTION; }
+ | SETMINUS_TOK { $kind = CVC4::kind::SETMINUS; }
+ | SETSUB_TOK { $kind = CVC4::kind::SUBSET; }
+ | SETIN_TOK { $kind = CVC4::kind::IN; }
+ | SETSINGLETON_TOK { $kind = CVC4::kind::SET_SINGLETON; }
// NOTE: Theory operators go here
;
PARSER_STATE->parseError("Illegal array type.");
}
t = EXPR_MANAGER->mkArrayType( args[0], args[1] );
+ } else if(name == "Set") {
+ if(args.size() != 1) {
+ PARSER_STATE->parseError("Illegal set type.");
+ }
+ t = EXPR_MANAGER->mkSetType( args[0] );
} else if(check == CHECK_DECLARED ||
PARSER_STATE->isDeclared(name, SYM_SORT)) {
t = PARSER_STATE->getSort(name, args);
REOPT_TOK : 're.opt';
RERANGE_TOK : 're.range';
+SETUNION_TOK: 'union';
+SETINT_TOK: 'intersection';
+SETMINUS_TOK: 'setminus';
+SETSUB_TOK: 'subseteq';
+SETIN_TOK: 'in';
+SETSINGLETON_TOK: 'setenum';
+EMPTYSET_TOK: 'emptyset';
+
/**
* A sequence of printable ASCII characters (except backslash) that starts
* and ends with | and does not otherwise contain |.
break;
}
+ case kind::EMPTYSET:
+ out << "(as emptyset " << n.getConst<EmptySet>().getType() << ")";
+ break;
+
default:
// fall back on whatever operator<< does on underlying type; we
// might luck out and be SMT-LIB v2 compliant
stillNeedToPrintParams = false;
break;
- // datatypes
+ // sets
+ case kind::UNION:
+ case kind::INTERSECTION:
+ case kind::SETMINUS:
+ case kind::SUBSET:
+ case kind::IN:
+ case kind::SET_TYPE:
+ case kind::SET_SINGLETON: out << smtKindString(k) << " "; break;
+
+ // datatypes
case kind::APPLY_TYPE_ASCRIPTION: {
out << "as ";
toStream(out, n[0], toDepth < 0 ? toDepth : toDepth - 1, types);
case kind::BITVECTOR_SIGN_EXTEND: return "sign_extend";
case kind::BITVECTOR_ROTATE_LEFT: return "rotate_left";
case kind::BITVECTOR_ROTATE_RIGHT: return "rotate_right";
+
+ case kind::UNION: return "union";
+ case kind::INTERSECTION: return "intersection";
+ case kind::SETMINUS: return "setminus";
+ case kind::SUBSET: return "subseteq";
+ case kind::IN: return "in";
+ case kind::SET_TYPE: return "Set";
+ case kind::SET_SINGLETON: return "setenum";
default:
; /* fall through */
}
}
~Info() {
- //FIXME!
- //indices->deleteSelf();
indices->deleteSelf();
stores->deleteSelf();
in_stores->deleteSelf();
}
++seen;
}
+ if(d_theories[THEORY_SETS]) {
+ ss << "_SETS";
+ ++seen;
+ }
if(seen != d_sharingTheories) {
Unhandled("can't extract a logic string from LogicInfo; at least one "
arithNonLinear();
p += 4;
}
+ if(!strncmp(p, "_SETS", 5)) {
+ enableTheory(THEORY_SETS);
+ p += 5;
+ }
}
}
if(*p != '\0') {
--- /dev/null
+README.WHATS-NEXT
--- /dev/null
+topdir = ../../..
+srcdir = src/theory/sets
+
+include $(topdir)/Makefile.subdir
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@builddir@/../.. -I@srcdir@/../../include -I@srcdir@/../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libsets.la
+
+libsets_la_SOURCES = \
+ theory_sets.h \
+ theory_sets.cpp \
+ theory_sets_private.h \
+ theory_sets_private.cpp \
+ theory_sets_rewriter.h \
+ theory_sets_rewriter.cpp \
+ theory_sets_type_rules.h \
+ theory_set_type_enumerator.h
+
+EXTRA_DIST = \
+ kinds \
+ options_handlers.h
--- /dev/null
+/********************* */
+/*! \file expr_patterns.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Expr patterns.
+ **
+ ** Expr patterns.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace expr {
+namespace pattern {
+
+static Node AND(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::AND, a, b);
+}
+
+static Node OR(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::OR, a, b);
+}
+
+static Node OR(TNode a, TNode b, TNode c) {
+ return NodeManager::currentNM()->mkNode(kind::OR, a, b, c);
+}
+
+static Node IN(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::IN, a, b);
+}
+
+static Node EQUAL(TNode a, TNode b) {
+ return NodeManager::currentNM()->mkNode(kind::EQUAL, a, b);
+}
+
+static Node NOT(TNode a) {
+ return NodeManager::currentNM()->mkNode(kind::NOT, a);
+}
+
+}/* CVC4::expr::pattern namespace */
+}/* CVC4::expr namespace */
+}/* CVC4 namespace */
--- /dev/null
+# kinds -*- sh -*-
+#
+# For documentation on this file format, please refer to
+# src/theory/builtin/kinds.
+#
+
+theory THEORY_SETS ::CVC4::theory::sets::TheorySets "theory/sets/theory_sets.h"
+typechecker "theory/sets/theory_sets_type_rules.h"
+rewriter ::CVC4::theory::sets::TheorySetsRewriter "theory/sets/theory_sets_rewriter.h"
+
+properties check propagate #presolve postsolve
+
+# Theory content goes here.
+
+# constants...
+constant EMPTYSET \
+ ::CVC4::EmptySet \
+ ::CVC4::EmptySetHashFunction \
+ "util/emptyset.h" \
+ "empty set"
+
+# types...
+operator SET_TYPE 1 "set type" # the type
+cardinality SET_TYPE \
+ "::CVC4::theory::sets::SetsProperties::computeCardinality(%TYPE%)" \
+ "theory/sets/theory_sets_type_rules.h"
+well-founded SET_TYPE \
+ "::CVC4::theory::sets::SetsProperties::isWellFounded(%TYPE%)" \
+ "::CVC4::theory::sets::SetsProperties::mkGroundTerm(%TYPE%)" \
+ "theory/sets/theory_sets_type_rules.h"
+enumerator SET_TYPE \
+ "::CVC4::theory::sets::SetEnumerator" \
+ "theory/sets/theory_sets_type_enumerator.h"
+
+# operators...
+operator UNION 2 "set union"
+operator INTERSECTION 2 "set intersection"
+operator SETMINUS 2 "set subtraction"
+operator SUBSET 2 "subset"
+operator IN 2 "set membership"
+
+operator SET_SINGLETON 1 "singleton set"
+
+typerule UNION ::CVC4::theory::sets::SetUnionTypeRule
+typerule INTERSECTION ::CVC4::theory::sets::SetIntersectionTypeRule
+typerule SETMINUS ::CVC4::theory::sets::SetSetminusTypeRule
+typerule SUBSET ::CVC4::theory::sets::SetSubsetTypeRule
+typerule IN ::CVC4::theory::sets::SetInTypeRule
+typerule SET_SINGLETON ::CVC4::theory::sets::SetSingletonTypeRule
+typerule EMPTYSET ::CVC4::theory::sets::EmptySetTypeRule
+
+construle SET_SINGLETON ::CVC4::theory::sets::SetConstTypeRule
+construle UNION ::CVC4::theory::sets::SetConstTypeRule
+
+endtheory
--- /dev/null
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SETS "theory/sets/options.h" Sets
+
+option setsPropagate --sets-propagate bool :default true
+ determines whether to propagate learnt facts to Theory Engine / SAT solver
+
+option setsEagerLemmas --sets-eager-lemmas bool :default false
+ if true, will add lemmas even if not at FULL_EFFORT
+
+endmodule
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+#define __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__OPTIONS_HANDLERS_H */
--- /dev/null
+/********************* */
+/*! \file term_info.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-2014 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Term info.
+ **
+ ** Term info.
+ **/
+
+#include "cvc4_private.h"
+
+#pragma once
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+
+typedef context::CDList<TNode> CDTNodeList;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
+
+class TheorySetsTermInfo {
+public:
+ CDTNodeList* elementsInThisSet;
+ CDTNodeList* elementsNotInThisSet;
+ CDTNodeList* parents;
+
+ TheorySetsTermInfo(context::Context* c)
+ {
+ elementsInThisSet = new(true)CDTNodeList(c);
+ elementsNotInThisSet = new(true)CDTNodeList(c);
+ parents = new(true)CDTNodeList(c);
+ }
+
+ void addToElementList(TNode n, bool polarity) {
+ if(polarity) elementsInThisSet -> push_back(n);
+ else elementsNotInThisSet -> push_back(n);
+ }
+
+ ~TheorySetsTermInfo() {
+ elementsInThisSet -> deleteSelf();
+ elementsNotInThisSet -> deleteSelf();
+ parents -> deleteSelf();
+ }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_sets.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-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.
+ **
+ ** Sets theory.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+TheorySets::TheorySets(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo) :
+ Theory(THEORY_SETS, c, u, out, valuation, logicInfo),
+ d_internal(new TheorySetsPrivate(*this, c, u)) {
+}
+
+TheorySets::~TheorySets() {
+ delete d_internal;
+}
+
+void TheorySets::check(Effort e) {
+ d_internal->check(e);
+}
+
+void TheorySets::propagate(Effort e) {
+ d_internal->propagate(e);
+}
+
+Node TheorySets::explain(TNode node) {
+ return d_internal->explain(node);
+}
+
+void TheorySets::preRegisterTerm(TNode node) {
+ return d_internal->preRegisterTerm(node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_sets.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-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.
+ **
+ ** Sets theory.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_H
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsPrivate;
+
+class TheorySets : public Theory {
+private:
+ friend class TheorySetsPrivate;
+ TheorySetsPrivate* d_internal;
+public:
+
+ /**
+ * Constructs a new instance of TheorySets w.r.t. the provided
+ * contexts.
+ */
+ TheorySets(context::Context* c,
+ context::UserContext* u,
+ OutputChannel& out,
+ Valuation valuation,
+ const LogicInfo& logicInfo);
+
+ ~TheorySets();
+
+ void check(Effort);
+
+ void propagate(Effort);
+
+ Node explain(TNode);
+
+ std::string identify() const { return "THEORY_SETS"; }
+
+ void preRegisterTerm(TNode node);
+
+};/* class TheorySets */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_H */
--- /dev/null
+/********************* */
+/*! \file theory_sets_private.cpp
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-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.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "theory/sets/theory_sets.h"
+#include "theory/sets/theory_sets_private.h"
+
+#include "theory/sets/options.h"
+#include "theory/sets/expr_patterns.h" // ONLY included here
+
+#include "util/result.h"
+
+using namespace std;
+using namespace CVC4::expr::pattern;
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+const char* element_of_str = " \u2208 ";
+
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+/**************************** TheorySetsPrivate *****************************/
+
+void TheorySetsPrivate::check(Theory::Effort level) {
+
+ CodeTimer checkCodeTimer(d_statistics.d_checkTime);
+
+ while(!d_external.done() && !d_conflict) {
+ // Get all the assertions
+ Assertion assertion = d_external.get();
+ TNode fact = assertion.assertion;
+
+ Debug("sets") << "\n\n[sets] TheorySetsPrivate::check(): processing "
+ << fact << std::endl;
+
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ // Solve each
+ switch(atom.getKind()) {
+ case kind::EQUAL:
+ Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+ << "be equal to " << atom[1] << std::endl;
+ assertEquality(fact, fact, /* learnt = */ false);
+ break;
+
+ case kind::IN:
+ Debug("sets") << atom[0] << " should " << (polarity ? "":"NOT ")
+ << "be in " << atom[1] << std::endl;
+ assertMemebership(fact, fact, /* learnt = */ false);
+ break;
+
+ default:
+ Unhandled(fact.getKind());
+ }
+ finishPropagation();
+
+ Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl;
+
+ if(d_conflict && !d_equalityEngine.consistent()) return;
+ Assert(!d_conflict);
+ Assert(d_equalityEngine.consistent());
+ }
+
+ Debug("sets") << "[sets] is complete = " << isComplete() << std::endl;
+
+ if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) {
+ d_external.d_out->lemma(getLemma());
+ }
+
+ return;
+}/* TheorySetsPrivate::check() */
+
+
+void TheorySetsPrivate::assertEquality(TNode fact, TNode reason, bool learnt)
+{
+ Debug("sets-assert") << "\n[sets-assert] adding equality: " << fact
+ << ", " << reason
+ << ", " << learnt << std::endl;
+
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ // fact already holds
+ if( holds(atom, polarity) ) {
+ Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl;
+ return;
+ }
+
+ // assert fact & check for conflict
+ if(learnt) {
+ registerReason(reason, /*save=*/ true);
+ }
+ d_equalityEngine.assertEquality(atom, polarity, reason);
+
+ if(!d_equalityEngine.consistent()) {
+ Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl;
+ d_conflict = true;
+ return;
+ }
+
+ if(!polarity && atom[0].getType().isSet()) {
+ addToPending(atom);
+ }
+
+}/* TheorySetsPrivate::assertEquality() */
+
+
+void TheorySetsPrivate::assertMemebership(TNode fact, TNode reason, bool learnt)
+{
+ Debug("sets-assert") << "\n[sets-assert] adding membership: " << fact
+ << ", " << reason
+ << ", " << learnt << std::endl;
+
+ bool polarity = fact.getKind() == kind::NOT ? false : true;
+ TNode atom = polarity ? fact : fact[0];
+
+ // fact already holds
+ if( holds(atom, polarity) ) {
+ Debug("sets-assert") << "[sets-assert] already present, skipping" << std::endl;
+ return;
+ }
+
+ // assert fact & check for conflict
+ if(learnt) {
+ registerReason(reason, true);
+ }
+ d_equalityEngine.assertPredicate(atom, polarity, reason);
+
+ if(!d_equalityEngine.consistent()) {
+ Debug("sets-assert") << "[sets-assert] running into a conflict" << std::endl;
+ d_conflict = true;
+ return;
+ }
+
+ // update term info data structures
+ d_termInfoManager->notifyMembership(fact);
+
+ // propagation
+ TNode x = d_equalityEngine.getRepresentative(atom[0]);
+ eq::EqClassIterator j(d_equalityEngine.getRepresentative(atom[1]),
+ &d_equalityEngine);
+ TNode S = (*j);
+ Node cur_atom = IN(x, S);
+
+ /**
+ * It is sufficient to do emptyset propagation outside the loop as
+ * constant term is guaranteed to be class representative.
+ */
+ if(polarity && S.getKind() == kind::EMPTYSET) {
+ Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
+ << std::endl;
+ learnLiteral(cur_atom, false, cur_atom);
+ Assert(d_conflict);
+ return;
+ }
+
+ for(; !j.isFinished(); ++j) {
+ TNode S = (*j);
+ Node cur_atom = IN(x, S);
+
+ // propagation : children
+ Debug("sets-prop") << "[sets-prop] Propagating 'down' for "
+ << x << element_of_str << S << std::endl;
+ if(S.getKind() == kind::UNION ||
+ S.getKind() == kind::INTERSECTION ||
+ S.getKind() == kind::SETMINUS ||
+ S.getKind() == kind::SET_SINGLETON) {
+ doSettermPropagation(x, S);
+ if(d_conflict) return;
+ }// propagation: children
+
+
+ // propagation : parents
+ Debug("sets-prop") << "[sets-prop] Propagating 'up' for "
+ << x << element_of_str << S << std::endl;
+ const CDTNodeList* parentList = d_termInfoManager->getParents(S);
+ for(typeof(parentList->begin()) k = parentList->begin();
+ k != parentList->end(); ++k) {
+ doSettermPropagation(x, *k);
+ if(d_conflict) return;
+ }// propagation : parents
+
+
+ }//j loop
+
+}/* TheorySetsPrivate::assertMemebership() */
+
+
+void TheorySetsPrivate::doSettermPropagation(TNode x, TNode S)
+{
+ Debug("sets-prop") << "[sets-prop] doSettermPropagation("
+ << x << ", " << S << std::endl;
+
+ Assert(S.getType().isSet() && S.getType().getSetElementType() == x.getType());
+
+ Node literal, left_literal, right_literal;
+
+ // axiom: literal <=> left_literal AND right_literal
+ switch(S.getKind()) {
+ case kind::INTERSECTION:
+ literal = IN(x, S) ;
+ left_literal = IN(x, S[0]) ;
+ right_literal = IN(x, S[1]) ;
+ break;
+ case kind::UNION:
+ literal = NOT( IN(x, S) );
+ left_literal = NOT( IN(x, S[0]) );
+ right_literal = NOT( IN(x, S[1]) );
+ break;
+ case kind::SETMINUS:
+ literal = IN(x, S) ;
+ left_literal = IN(x, S[0]) ;
+ right_literal = NOT( IN(x, S[1]) );
+ break;
+ case kind::SET_SINGLETON: {
+ Node atom = IN(x, S);
+ if(holds(atom, true)) {
+ learnLiteral(EQUAL(x, S[0]), true, atom);
+ } else if(holds(atom, false)) {
+ learnLiteral(EQUAL(x, S[0]), false, NOT(atom));
+ }
+ return;
+ }
+ default:
+ Unhandled();
+ }
+
+ Debug("sets-prop-details")
+ << "[sets-prop-details] " << literal << " IFF " << left_literal
+ << " AND " << right_literal << std::endl;
+
+ Debug("sets-prop-details")
+ << "[sets-prop-details] "
+ << (holds(literal) ? "yes" : (holds(literal.negate()) ? " no" : " _ "))
+ << " IFF "
+ << (holds(left_literal) ? "yes" : (holds(left_literal.negate()) ? "no " : " _ "))
+ << " AND "
+ << (holds(right_literal) ? "yes" : (holds(right_literal.negate()) ? "no " : " _ "))
+ << std::endl;
+
+ Assert( present( IN(x, S) ) ||
+ present( IN(x, S[0]) ) ||
+ present( IN(x, S[1]) ) );
+
+ if( holds(literal) ) {
+ // 1a. literal => left_literal
+ Debug("sets-prop") << "[sets-prop] ... via case 1a. ..." << std::endl;
+ learnLiteral(left_literal, literal);
+ if(d_conflict) return;
+
+ // 1b. literal => right_literal
+ Debug("sets-prop") << "[sets-prop] ... via case 1b. ..." << std::endl;
+ learnLiteral(right_literal, literal);
+ if(d_conflict) return;
+
+ // subsumption requirement met, exit
+ return;
+ }
+ else if( holds(literal.negate() ) ) {
+ // 4. neg(literal), left_literal => neg(right_literal)
+ if( holds(left_literal) ) {
+ Debug("sets-prop") << "[sets-prop] ... via case 4. ..." << std::endl;
+ learnLiteral(right_literal.negate(), AND( literal.negate(),
+ left_literal) );
+ if(d_conflict) return;
+ }
+
+ // 5. neg(literal), right_literal => neg(left_literal)
+ if( holds(right_literal) ) {
+ Debug("sets-prop") << "[sets-prop] ... via case 5. ..." << std::endl;
+ learnLiteral(left_literal.negate(), AND( literal.negate(),
+ right_literal) );
+ if(d_conflict) return;
+ }
+ }
+ else {
+ // 2,3. neg(left_literal) v neg(right_literal) => neg(literal)
+ if(holds(left_literal.negate())) {
+ Debug("sets-prop") << "[sets-prop] ... via case 2. ..." << std::endl;
+ learnLiteral(literal.negate(), left_literal.negate());
+ if(d_conflict) return;
+ }
+ else if(holds(right_literal.negate())) {
+ Debug("sets-prop") << "[sets-prop] ... via case 3. ..." << std::endl;
+ learnLiteral(literal.negate(), right_literal.negate());
+ if(d_conflict) return;
+ }
+
+ // 6. the axiom itself:
+ else if(holds(left_literal) && holds(right_literal)) {
+ Debug("sets-prop") << "[sets-prop] ... via case 6. ..." << std::endl;
+ learnLiteral(literal, AND(left_literal, right_literal) );
+ if(d_conflict) return;
+ }
+ }
+
+ // check fulfilling rule
+ Node n;
+ switch(S.getKind()) {
+ case kind::UNION:
+ if( holds(IN(x, S)) &&
+ !present( IN(x, S[0]) ) )
+ addToPending( IN(x, S[0]) );
+ break;
+ case kind::SETMINUS: // intentional fallthrough
+ case kind::INTERSECTION:
+ if( holds(IN(x, S[0])) &&
+ !present( IN(x, S[1]) ))
+ addToPending( IN(x, S[1]) );
+ break;
+ default:
+ Assert(false, "MembershipEngine::doSettermPropagation");
+ }
+}
+
+
+void TheorySetsPrivate::learnLiteral(TNode atom, bool polarity, Node reason) {
+ Debug("sets-learn") << "[sets-learn] learnLiteral(" << atom
+ << ", " << polarity << ")" << std::endl;
+
+ if( holds(atom, polarity) ) {
+ Debug("sets-learn") << "[sets-learn] \u2514 already known, skipping" << std::endl;
+ return;
+ }
+
+ if( holds(atom, !polarity) ) {
+ Debug("sets-learn") << "[sets-learn] \u2514 conflict found" << std::endl;
+
+ registerReason(reason, /*save=*/ true);
+
+ if(atom.getKind() == kind::EQUAL) {
+ d_equalityEngine.assertEquality(atom, polarity, reason);
+ } else {
+ d_equalityEngine.assertPredicate(atom, polarity, reason);
+ }
+ Assert(d_conflict); // should be marked due to equality engine
+ return;
+ }
+
+ Assert(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IN);
+
+ Node learnt_literal = polarity ? Node(atom) : NOT(atom);
+ d_propagationQueue.push_back( make_pair(learnt_literal, reason) );
+}
+
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+/********************** Helper functions ***************************/
+
+Node mkAnd(const std::vector<TNode>& conjunctions) {
+ Assert(conjunctions.size() > 0);
+
+ std::set<TNode> all;
+
+ for (unsigned i = 0; i < conjunctions.size(); ++i) {
+ TNode t = conjunctions[i];
+
+ if (t.getKind() == kind::AND) {
+ for(TNode::iterator child_it = t.begin();
+ child_it != t.end(); ++child_it) {
+ Assert((*child_it).getKind() != kind::AND);
+ all.insert(*child_it);
+ }
+ }
+ else {
+ all.insert(t);
+ }
+
+ }
+
+ Assert(all.size() > 0);
+
+ if (all.size() == 1) {
+ // All the same, or just one
+ return conjunctions[0];
+ }
+
+ NodeBuilder<> conjunction(kind::AND);
+ std::set<TNode>::const_iterator it = all.begin();
+ std::set<TNode>::const_iterator it_end = all.end();
+ while (it != it_end) {
+ conjunction << *it;
+ ++ it;
+ }
+
+ return conjunction;
+}/* mkAnd() */
+
+
+TheorySetsPrivate::Statistics::Statistics() :
+ d_checkTime("theory::sets::time") {
+ StatisticsRegistry::registerStat(&d_checkTime);
+}
+
+
+TheorySetsPrivate::Statistics::~Statistics() {
+ StatisticsRegistry::unregisterStat(&d_checkTime);
+}
+
+
+bool TheorySetsPrivate::present(TNode atom) {
+ return holds(atom) || holds(atom.notNode());
+}
+
+
+bool TheorySetsPrivate::holds(TNode atom, bool polarity) {
+ Node polarity_atom = NodeManager::currentNM()->mkConst<bool>(polarity);
+
+ Node atomModEq = NodeManager::currentNM()->mkNode
+ (atom.getKind(), d_equalityEngine.getRepresentative(atom[0]),
+ d_equalityEngine.getRepresentative(atom[1]) );
+
+ d_equalityEngine.addTerm(atomModEq);
+
+ return d_equalityEngine.areEqual(atomModEq, polarity_atom);
+}
+
+
+void TheorySetsPrivate::registerReason(TNode reason, bool save)
+{
+ if(save) d_nodeSaver.insert(reason);
+
+ if(reason.getKind() == kind::AND) {
+ Assert(reason.getNumChildren() == 2);
+ registerReason(reason[0], false);
+ registerReason(reason[1], false);
+ } else if(reason.getKind() == kind::NOT) {
+ registerReason(reason[0], false);
+ } else if(reason.getKind() == kind::IN) {
+ d_equalityEngine.addTerm(reason);
+ Assert(present(reason));
+ } else if(reason.getKind() == kind::EQUAL) {
+ d_equalityEngine.addTerm(reason);
+ Assert(present(reason));
+ } else if(reason.getKind() == kind::CONST_BOOLEAN) {
+ // That's OK, already in EqEngine
+ } else {
+ Unhandled();
+ }
+}
+
+void TheorySetsPrivate::finishPropagation()
+{
+ while(!d_conflict && !d_settermPropagationQueue.empty()) {
+ std::pair<TNode,TNode> np = d_settermPropagationQueue.front();
+ d_settermPropagationQueue.pop();
+ doSettermPropagation(np.first, np.second);
+ }
+ while(!d_conflict && !d_propagationQueue.empty()) {
+ std::pair<Node,Node> np = d_propagationQueue.front();
+ d_propagationQueue.pop();
+ TNode atom = np.first.getKind() == kind::NOT ? np.first[0] : np.first;
+ if(atom.getKind() == kind::IN) {
+ assertMemebership(np.first, np.second, /* learnt = */ true);
+ } else {
+ assertEquality(np.first, np.second, /* learnt = */ true);
+ }
+ }
+}
+
+void TheorySetsPrivate::addToPending(Node n) {
+ if(d_pendingEverInserted.find(n) == d_pendingEverInserted.end()) {
+ if(n.getKind() == kind::IN) {
+ d_pending.push(n);
+ } else {
+ Assert(n.getKind() == kind::EQUAL);
+ d_pendingDisequal.push(n);
+ }
+ d_pendingEverInserted.insert(n);
+ }
+}
+
+bool TheorySetsPrivate::isComplete() {
+ while(!d_pending.empty() && present(d_pending.front()))
+ d_pending.pop();
+ return d_pending.empty() && d_pendingDisequal.empty();
+}
+
+Node TheorySetsPrivate::getLemma() {
+ Assert(!d_pending.empty() || !d_pendingDisequal.empty());
+
+ Node lemma;
+
+ if(!d_pending.empty()) {
+ Node n = d_pending.front();
+ d_pending.pop();
+
+ Assert(!present(n));
+ Assert(n.getKind() == kind::IN);
+
+ lemma = OR(n, NOT(n));
+ } else {
+ Node n = d_pendingDisequal.front();
+ d_pendingDisequal.pop();
+
+ Assert(n.getKind() == kind::EQUAL && n[0].getType().isSet());
+ Node x = NodeManager::currentNM()->mkSkolem("sde_$$", n[0].getType().getSetElementType());
+ Node l1 = IN(x, n[0]), l2 = IN(x, n[1]);
+
+ // d_equalityEngine.addTerm(x);
+ // d_equalityEngine.addTerm(l1);
+ // d_equalityEngine.addTerm(l2);
+ // d_terms.insert(x);
+
+ lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2));
+ }
+
+ Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl;
+
+ return lemma;
+}
+
+
+TheorySetsPrivate::TheorySetsPrivate(TheorySets& external,
+ context::Context* c,
+ context::UserContext* u):
+ d_external(external),
+ d_notify(*this),
+ d_equalityEngine(d_notify, c, "theory::sets::TheorySetsPrivate"),
+ d_conflict(c),
+ d_termInfoManager(NULL),
+ d_propagationQueue(c),
+ d_settermPropagationQueue(c),
+ d_nodeSaver(c),
+ d_pending(u),
+ d_pendingDisequal(u),
+ d_pendingEverInserted(u)
+{
+ d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine);
+
+ d_equalityEngine.addFunctionKind(kind::UNION);
+ d_equalityEngine.addFunctionKind(kind::INTERSECTION);
+ d_equalityEngine.addFunctionKind(kind::SETMINUS);
+
+ d_equalityEngine.addFunctionKind(kind::IN);
+ d_equalityEngine.addFunctionKind(kind::SUBSET);
+}/* TheorySetsPrivate::TheorySetsPrivate() */
+
+TheorySetsPrivate::~TheorySetsPrivate()
+{
+ delete d_termInfoManager;
+}
+
+
+
+void TheorySetsPrivate::propagate(Theory::Effort e)
+{
+ return;
+}
+
+bool TheorySetsPrivate::propagate(TNode literal) {
+ Debug("sets-prop") << " propagate(" << literal << ")" << std::endl;
+
+ // If already in conflict, no more propagation
+ if (d_conflict) {
+ Debug("sets-prop") << "TheoryUF::propagate(" << literal << "): already in conflict" << std::endl;
+ return false;
+ }
+
+ // Propagate out
+ bool ok = d_external.d_out->propagate(literal);
+ if (!ok) {
+ d_conflict = true;
+ }
+
+ return ok;
+}/* TheorySetsPropagate::propagate(TNode) */
+
+
+void TheorySetsPrivate::conflict(TNode a, TNode b)
+{
+ if (a.getKind() == kind::CONST_BOOLEAN) {
+ d_conflictNode = explain(a.iffNode(b));
+ } else {
+ d_conflictNode = explain(a.eqNode(b));
+ }
+ d_external.d_out->conflict(d_conflictNode);
+ Debug("sets") << "[sets] conflict: " << a << " iff " << b
+ << ", explaination " << d_conflictNode << std::endl;
+ d_conflict = true;
+}
+
+Node TheorySetsPrivate::explain(TNode literal)
+{
+ Debug("sets") << "TheorySetsPrivate::explain(" << literal << ")"
+ << std::endl;
+
+ bool polarity = literal.getKind() != kind::NOT;
+ TNode atom = polarity ? literal : literal[0];
+ std::vector<TNode> assumptions;
+
+ if(atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
+ d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
+ } else if(atom.getKind() == kind::IN) {
+ if( !d_equalityEngine.hasTerm(atom)) {
+ d_equalityEngine.addTerm(atom);
+ }
+ d_equalityEngine.explainPredicate(atom, polarity, assumptions);
+ } else {
+ Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "
+ << polarity << "); kind" << atom.getKind() << std::endl;
+ Unhandled();
+ }
+
+ return mkAnd(assumptions);
+}
+
+void TheorySetsPrivate::preRegisterTerm(TNode node)
+{
+ Debug("sets") << "TheorySetsPrivate::preRegisterTerm(" << node << ")"
+ << std::endl;
+
+ switch(node.getKind()) {
+ case kind::EQUAL:
+ // TODO: what's the point of this
+ d_equalityEngine.addTriggerEquality(node);
+ break;
+ case kind::IN:
+ // TODO: what's the point of this
+ d_equalityEngine.addTriggerPredicate(node);
+ break;
+ default:
+ d_termInfoManager->addTerm(node);
+ d_equalityEngine.addTriggerTerm(node, THEORY_SETS);
+ // d_equalityEngine.addTerm(node);
+ }
+ if(node.getKind() == kind::SET_SINGLETON) {
+ Node true_node = NodeManager::currentNM()->mkConst<bool>(true);
+ learnLiteral(IN(node[0], node), true, true_node);
+ //intentional fallthrough
+ }
+}
+
+
+
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+/**************************** eq::NotifyClass *****************************/
+
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerEquality(TNode equality, bool value)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyTriggerEquality: equality = " << equality << " value = " << value << std::endl;
+ if (value) {
+ return d_theory.propagate(equality);
+ } else {
+ // We use only literal triggers so taking not is safe
+ return d_theory.propagate(equality.notNode());
+ }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerPredicate(TNode predicate, bool value)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyTriggerPredicate: predicate = " << predicate << " value = " << value << std::endl;
+ if (value) {
+ return d_theory.propagate(predicate);
+ } else {
+ return d_theory.propagate(predicate.notNode());
+ }
+}
+
+bool TheorySetsPrivate::NotifyClass::eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyTriggerTermEquality: tag = " << tag << " t1 = " << t1 << " t2 = " << t2 << " value = " << value << std::endl;
+ if(value) {
+ d_theory.d_termInfoManager->mergeTerms(t1, t2);
+ }
+ return true;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyConstantTermMerge " << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+ d_theory.conflict(t1, t2);
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyNewClass(TNode t)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyNewClass:" << " t = " << t << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyPreMerge(TNode t1, TNode t2)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyPreMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyPostMerge(TNode t1, TNode t2)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyPostMerge:" << " t1 = " << t1 << " t2 = " << t2 << std::endl;
+}
+
+void TheorySetsPrivate::NotifyClass::eqNotifyDisequal(TNode t1, TNode t2, TNode reason)
+{
+ Debug("sets-eq") << "[sets-eq] eqNotifyDisequal:" << " t1 = " << t1 << " t2 = " << t2 << " reason = " << reason << std::endl;
+}
+
+
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+/**************************** TermInfoManager *****************************/
+
+void TheorySetsPrivate::TermInfoManager::mergeLists
+(CDTNodeList* la, const CDTNodeList* lb) const {
+ // straight from theory/arrays/array_info.cpp
+ std::set<TNode> temp;
+ CDTNodeList::const_iterator it;
+ for(it = la->begin() ; it != la->end(); it++ ) {
+ temp.insert((*it));
+ }
+
+ for(it = lb->begin() ; it!= lb->end(); it++ ) {
+ if(temp.count(*it) == 0) {
+ la->push_back(*it);
+ }
+ }
+}
+
+TheorySetsPrivate::TermInfoManager::TermInfoManager
+(TheorySetsPrivate& theory, context::Context* satContext, eq::EqualityEngine* eq):
+ d_theory(theory),
+ d_context(satContext),
+ d_eqEngine(eq),
+ d_terms(satContext),
+ d_info()
+{ }
+
+TheorySetsPrivate::TermInfoManager::~TermInfoManager() {
+ for( typeof(d_info.begin()) it = d_info.begin();
+ it != d_info.end(); ++it) {
+ delete (*it).second;
+ }
+}
+
+void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) {
+ bool polarity = fact.getKind() != kind::NOT;
+ TNode atom = polarity ? fact : fact[0];
+
+ TNode x = d_eqEngine->getRepresentative(atom[0]);
+ TNode S = d_eqEngine->getRepresentative(atom[1]);
+
+ Debug("sets-terminfo") << "[sets-terminfo] Adding membership " << x
+ << " in " << S << " " << polarity << std::endl;
+
+ d_info[S]->addToElementList(x, polarity);
+}
+
+const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) {
+ return d_info[x]->parents;
+}
+
+void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) {
+ unsigned numChild = n.getNumChildren();
+
+ if(!d_terms.contains(n)) {
+ d_terms.insert(n);
+ d_info[n] = new TheorySetsTermInfo(d_context);
+ }
+
+ if(n.getKind() == kind::UNION ||
+ n.getKind() == kind::INTERSECTION ||
+ n.getKind() == kind::SETMINUS ||
+ n.getKind() == kind::SET_SINGLETON) {
+
+ for(unsigned i = 0; i < numChild; ++i) {
+ if(d_terms.contains(n[i])) {
+ Debug("sets-parent") << "Adding " << n << " to parent list of "
+ << n[i] << std::endl;
+ d_info[n[i]]->parents->push_back(n);
+ }
+ }
+
+ }
+}
+
+void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue
+(CDTNodeList* l, TNode S, bool polarity)
+{
+ for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) {
+ Debug("sets-prop") << "[sets-terminfo] setterm todo: "
+ << IN(*i, d_eqEngine->getRepresentative(S))
+ << std::endl;
+
+ d_eqEngine->addTerm(IN(d_eqEngine->getRepresentative(*i),
+ d_eqEngine->getRepresentative(S)));
+
+ for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine);
+ !j.isFinished(); ++j) {
+
+ TNode x = (*i);
+ TNode S = (*j);
+ Node cur_atom = IN(x, S);
+
+ // propagation : empty set
+ if(polarity && S.getKind() == kind::EMPTYSET) {
+ Debug("sets-prop") << "[sets-prop] something in empty set? conflict."
+ << std::endl;
+ d_theory.learnLiteral(cur_atom, false, cur_atom);
+ return;
+ }// propagation: empty set
+
+ // propagation : children
+ if(S.getKind() == kind::UNION ||
+ S.getKind() == kind::INTERSECTION ||
+ S.getKind() == kind::SETMINUS ||
+ S.getKind() == kind::SET_SINGLETON) {
+ d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S));
+ }// propagation: children
+
+ // propagation : parents
+ const CDTNodeList* parentList = getParents(S);
+ for(typeof(parentList->begin()) k = parentList->begin();
+ k != parentList->end(); ++k) {
+ d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k));
+ }// propagation : parents
+
+
+ }//j loop
+
+ }
+
+}
+
+void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) {
+ // merge b into a
+
+ if(!a.getType().isSet()) return;
+
+ Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a
+ << ", b = " << b << std::endl;
+ Debug("sets-terminfo") << "[sets-terminfo] reps"
+ << ", a: " << d_eqEngine->getRepresentative(a)
+ << ", b: " << d_eqEngine->getRepresentative(b)
+ << std::endl;
+
+ typeof(d_info.begin()) ita = d_info.find(a);
+ typeof(d_info.begin()) itb = d_info.find(b);
+
+ Assert(ita != d_info.end());
+ Assert(itb != d_info.end());
+
+ pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true );
+ pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false );
+ pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false );
+ pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true );
+
+ mergeLists((*ita).second->elementsInThisSet,
+ (*itb).second->elementsInThisSet);
+
+ mergeLists((*ita).second->elementsNotInThisSet,
+ (*itb).second->elementsNotInThisSet);
+}
+
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_sets_private.h
+ ** \verbatim
+ ** Original author: Kshitij Bansal
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2013-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.
+ **
+ ** Sets theory implementation.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H
+
+#include "context/cdhashset.h"
+#include "context/cdqueue.h"
+
+#include "theory/theory.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/sets/term_info.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+/** Internal classes, forward declared here */
+class TheorySetsTermInfoManager;
+class TheorySets;
+
+class TheorySetsPrivate {
+public:
+
+ /**
+ * Constructs a new instance of TheorySetsPrivate w.r.t. the provided
+ * contexts.
+ */
+ TheorySetsPrivate(TheorySets& external,
+ context::Context* c,
+ context::UserContext* u);
+
+ ~TheorySetsPrivate();
+
+ void check(Theory::Effort);
+
+ void propagate(Theory::Effort);
+
+ Node explain(TNode);
+
+ std::string identify() const { return "THEORY_SETS_PRIVATE"; }
+
+ void preRegisterTerm(TNode node);
+
+private:
+ TheorySets& d_external;
+
+ class Statistics {
+ public:
+ TimerStat d_checkTime;
+
+ Statistics();
+ ~Statistics();
+ } d_statistics;
+
+ /** Functions to handle callbacks from equality engine */
+ class NotifyClass : public eq::EqualityEngineNotify {
+ TheorySetsPrivate& d_theory;
+
+ public:
+ NotifyClass(TheorySetsPrivate& theory): d_theory(theory) {}
+ bool eqNotifyTriggerEquality(TNode equality, bool value);
+ bool eqNotifyTriggerPredicate(TNode predicate, bool value);
+ bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value);
+ void eqNotifyConstantTermMerge(TNode t1, TNode t2);
+ void eqNotifyNewClass(TNode t);
+ void eqNotifyPreMerge(TNode t1, TNode t2);
+ void eqNotifyPostMerge(TNode t1, TNode t2);
+ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
+ } d_notify;
+
+ /** Equality engine */
+ eq::EqualityEngine d_equalityEngine;
+
+ context::CDO<bool> d_conflict;
+ Node d_conflictNode;
+
+ /** Proagate out to output channel */
+ bool propagate(TNode);
+
+ /** generate and send out conflict node */
+ void conflict(TNode, TNode);
+
+ class TermInfoManager {
+ TheorySetsPrivate& d_theory;
+ context::Context* d_context;
+ eq::EqualityEngine* d_eqEngine;
+
+ CDNodeSet d_terms;
+ std::hash_map<TNode, TheorySetsTermInfo*, TNodeHashFunction> d_info;
+
+ void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const;
+ void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity);
+ public:
+ TermInfoManager(TheorySetsPrivate&,
+ context::Context* satContext,
+ eq::EqualityEngine*);
+ ~TermInfoManager();
+ void notifyMembership(TNode fact);
+ const CDTNodeList* getParents(TNode x);
+ void addTerm(TNode n);
+ void mergeTerms(TNode a, TNode b);
+ };
+ TermInfoManager* d_termInfoManager;
+
+ /** Assertions and helper functions */
+ bool present(TNode atom);
+ bool holds(TNode lit) {
+ bool polarity = lit.getKind() == kind::NOT ? false : true;
+ TNode atom = polarity ? lit : lit[0];
+ return holds(atom, polarity);
+ }
+ bool holds(TNode atom, bool polarity);
+
+ void assertEquality(TNode fact, TNode reason, bool learnt);
+ void assertMemebership(TNode fact, TNode reason, bool learnt);
+
+ /** Propagation / learning and helper functions. */
+ context::CDQueue< std::pair<Node, Node> > d_propagationQueue;
+ context::CDQueue< std::pair<TNode, TNode> > d_settermPropagationQueue;
+
+ void doSettermPropagation(TNode x, TNode S);
+ void registerReason(TNode reason, bool save);
+ void learnLiteral(TNode atom, bool polarity, Node reason);
+ void learnLiteral(TNode lit, Node reason) {
+ if(lit.getKind() == kind::NOT) {
+ learnLiteral(lit[0], false, reason);
+ } else {
+ learnLiteral(lit, true, reason);
+ }
+ }
+ void finishPropagation();
+
+ // for any nodes we need to save, because others use TNode
+ context::CDHashSet <Node, NodeHashFunction> d_nodeSaver;
+
+ /** Lemmas and helper functions */
+ context::CDQueue <TNode> d_pending;
+ context::CDQueue <TNode> d_pendingDisequal;
+ context::CDHashSet <Node, NodeHashFunction> d_pendingEverInserted;
+
+ void addToPending(Node n);
+ bool isComplete();
+ Node getLemma();
+};/* class TheorySetsPrivate */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_PRIVATE_H */
--- /dev/null
+#include "theory/sets/theory_sets_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+bool checkConstantMembership(TNode elementTerm, TNode setTerm)
+{
+ switch(setTerm.getKind()) {
+ case kind::EMPTYSET:
+ return false;
+ case kind::SET_SINGLETON:
+ return elementTerm == setTerm[0];
+ case kind::UNION:
+ return checkConstantMembership(elementTerm, setTerm[0]) ||
+ checkConstantMembership(elementTerm, setTerm[1]);
+ case kind::INTERSECTION:
+ return checkConstantMembership(elementTerm, setTerm[0]) &&
+ checkConstantMembership(elementTerm, setTerm[1]);
+ case kind::SETMINUS:
+ return checkConstantMembership(elementTerm, setTerm[0]) &&
+ !checkConstantMembership(elementTerm, setTerm[1]);
+ default:
+ Unhandled();
+ }
+}
+
+// static
+RewriteResponse TheorySetsRewriter::postRewrite(TNode node) {
+ NodeManager* nm = NodeManager::currentNM();
+
+ switch(node.getKind()) {
+
+ case kind::IN: {
+ if(!node[0].isConst() || !node[1].isConst())
+ break;
+
+ // both are constants
+ bool isMember = checkConstantMembership(node[0], node[1]);
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(isMember));
+ }
+
+ case kind::SUBSET: {
+ // rewrite (A subset-or-equal B) as (A union B = B)
+ TNode A = node[0];
+ TNode B = node[1];
+ return RewriteResponse(REWRITE_AGAIN,
+ nm->mkNode(kind::EQUAL,
+ nm->mkNode(kind::UNION, A, B),
+ B) );
+ }//kind::SUBSET
+
+ case kind::EQUAL:
+ case kind::IFF: {
+ //rewrite: t = t with true (t term)
+ //rewrite: c = c' with c different from c' false (c, c' constants)
+ //otherwise: sort them
+ if(node[0] == node[1]) {
+ Trace("sets-postrewrite") << "Sets::postRewrite returning true" << std::endl;
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+ }
+ else if (node[0].isConst() && node[1].isConst()) {
+ Trace("sets-postrewrite") << "Sets::postRewrite returning false" << std::endl;
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(false));
+ }
+ else if (node[0] > node[1]) {
+ Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+ Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+ return RewriteResponse(REWRITE_DONE, newNode);
+ }
+ break;
+ }
+
+ case kind::UNION:
+ 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] > node[1]) {
+ Node newNode = nm->mkNode(node.getKind(), node[1], node[0]);
+ Trace("sets-postrewrite") << "Sets::postRewrite returning " << newNode << std::endl;
+ return RewriteResponse(REWRITE_DONE, newNode);
+ }
+ break;
+ }
+
+ default:
+ break;
+
+ }//switch(node.getKind())
+
+ // This default implementation
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+// static
+RewriteResponse TheorySetsRewriter::preRewrite(TNode node) {
+ NodeManager* nm = NodeManager::currentNM();
+
+ // do nothing
+ if(node.getKind() == kind::EQUAL && node[0] == node[1])
+ return RewriteResponse(REWRITE_DONE, nm->mkConst(true));
+ // Further optimization, if constants but differing ones
+
+ return RewriteResponse(REWRITE_DONE, node);
+}
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class TheorySetsRewriter {
+public:
+
+ /**
+ * Rewrite a node into the normal form for the theory of sets.
+ * Called in post-order (really reverse-topological order) when
+ * traversing the expression DAG during rewriting. This is the
+ * main function of the rewriter, and because of the ordering,
+ * it can assume its children are all rewritten already.
+ *
+ * This function can return one of three rewrite response codes
+ * along with the rewritten node:
+ *
+ * REWRITE_DONE indicates that no more rewriting is needed.
+ * REWRITE_AGAIN means that the top-level expression should be
+ * rewritten again, but that its children are in final form.
+ * REWRITE_AGAIN_FULL means that the entire returned expression
+ * should be rewritten again (top-down with preRewrite(), then
+ * bottom-up with postRewrite()).
+ *
+ * Even if this function returns REWRITE_DONE, if the returned
+ * expression belongs to a different theory, it will be fully
+ * rewritten by that theory's rewriter.
+ */
+ static RewriteResponse postRewrite(TNode node);
+
+ /**
+ * Rewrite a node into the normal form for the theory of sets
+ * in pre-order (really topological order)---meaning that the
+ * children may not be in the normal form. This is an optimization
+ * for theories with cancelling terms (e.g., 0 * (big-nasty-expression)
+ * in arithmetic rewrites to 0 without the need to look at the big
+ * nasty expression). Since it's only an optimization, the
+ * implementation here can do nothing.
+ */
+ static RewriteResponse preRewrite(TNode node);
+
+ /**
+ * Rewrite an equality, in case special handling is required.
+ */
+ static Node rewriteEquality(TNode equality) {
+ // often this will suffice
+ return postRewrite(equality).node;
+ }
+
+ /**
+ * Initialize the rewriter.
+ */
+ static inline void init() {
+ // nothing to do
+ }
+
+ /**
+ * Shut down the rewriter.
+ */
+ static inline void shutdown() {
+ // nothing to do
+ }
+
+};/* class TheorySetsRewriter */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_REWRITER_H */
--- /dev/null
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+#define __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H
+
+#include "theory/type_enumerator.h"
+#include "expr/type_node.h"
+#include "expr/kind.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetEnumerator : public TypeEnumeratorBase<SetEnumerator> {
+ unsigned d_index;
+ TypeNode d_constituentType;
+ NodeManager* d_nm;
+ std::vector<bool> d_indexVec;
+ std::vector<TypeEnumerator*> d_constituentVec;
+ bool d_finished;
+ Node d_setConst;
+
+public:
+
+ SetEnumerator(TypeNode type) throw(AssertionException) :
+ TypeEnumeratorBase<SetEnumerator>(type),
+ d_index(0),
+ d_constituentType(type.getSetElementType()),
+ d_nm(NodeManager::currentNM()),
+ d_indexVec(),
+ d_constituentVec(),
+ d_finished(false),
+ d_setConst()
+ {
+ // d_indexVec.push_back(false);
+ // d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ d_setConst = d_nm->mkConst(EmptySet(type.toType()));
+ }
+
+ // An set enumerator could be large, and generally you don't want to
+ // go around copying these things; but a copy ctor is presently required
+ // by the TypeEnumerator framework.
+ SetEnumerator(const SetEnumerator& ae) throw() :
+ TypeEnumeratorBase<SetEnumerator>(ae.d_nm->mkSetType(ae.d_constituentType)),
+ d_constituentType(ae.d_constituentType),
+ d_nm(ae.d_nm),
+ d_indexVec(ae.d_indexVec),
+ d_constituentVec(),// copied below
+ d_finished(ae.d_finished),
+ d_setConst(ae.d_setConst)
+ {
+ for(std::vector<TypeEnumerator*>::const_iterator i =
+ ae.d_constituentVec.begin(), i_end = ae.d_constituentVec.end();
+ i != i_end;
+ ++i) {
+ d_constituentVec.push_back(new TypeEnumerator(**i));
+ }
+ }
+
+ ~SetEnumerator() {
+ while (!d_constituentVec.empty()) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+ }
+ }
+
+ Node operator*() throw(NoMoreValuesException) {
+ if (d_finished) {
+ throw NoMoreValuesException(getType());
+ }
+ Node n = d_setConst;
+
+ // For now only support only sets of size 1
+ Assert(d_index == 0 || d_index == 1);
+
+ if(d_index == 1) {
+ n = d_nm->mkNode(kind::SET_SINGLETON, *(*(d_constituentVec[0])));
+ }
+
+ // for (unsigned i = 0; i < d_indexVec.size(); ++i) {
+ // n = d_nm->mkNode(kind::STORE, n, d_indexVec[d_indexVec.size() - 1 - i], *(*(d_constituentVec[i])));
+ // }
+ Trace("set-type-enum") << "operator * prerewrite: " << n << std::endl;
+ n = Rewriter::rewrite(n);
+ Trace("set-type-enum") << "operator * returning: " << n << std::endl;
+ return n;
+ }
+
+ SetEnumerator& operator++() throw() {
+ Trace("set-type-enum") << "operator++ called, **this = " << **this << std::endl;
+
+ if (d_finished) {
+ Trace("set-type-enum") << "operator++ finished!" << std::endl;
+ return *this;
+ }
+
+ // increment by one, at the same time deleting all elements that
+ // cannot be incremented any further (note: we are keeping a set
+ // -- no repetitions -- thus some trickery to know what to pop and
+ // what not to.)
+ if(d_index > 0) {
+ Assert(d_index == d_constituentVec.size());
+
+ Node last_pre_increment;
+ last_pre_increment = *(*d_constituentVec.back());
+
+ ++(*d_constituentVec.back());
+
+ if (d_constituentVec.back()->isFinished()) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+
+ while(!d_constituentVec.empty()) {
+ Node cur_pre_increment = *(*d_constituentVec.back());
+ ++(*d_constituentVec.back());
+ Node cur_post_increment = *(*d_constituentVec.back());
+ if(last_pre_increment == cur_post_increment) {
+ delete d_constituentVec.back();
+ d_constituentVec.pop_back();
+ last_pre_increment = cur_pre_increment;
+ } else {
+ break;
+ }
+ }
+ }
+ }
+
+ if (d_constituentVec.empty()) {
+ ++d_index;
+ d_constituentVec.push_back(new TypeEnumerator(d_constituentType));
+ }
+
+ while (d_constituentVec.size() < d_index) {
+ TypeEnumerator *d_newEnumerator = new TypeEnumerator(*d_constituentVec.back());
+ ++(*d_newEnumerator);
+ if( (*d_newEnumerator).isFinished() ) {
+ Trace("set-type-enum") << "operator++ finished!" << std::endl;
+ d_finished = true;
+ return *this;
+ }
+ d_constituentVec.push_back(d_newEnumerator);
+ }
+
+ Trace("set-type-enum") << "operator++ returning, **this = " << **this << std::endl;
+ return *this;
+ }
+
+ bool isFinished() throw() {
+ Trace("set-type-enum") << "isFinished returning: " << d_finished << std::endl;
+ return d_finished;
+ }
+
+};/* class SetEnumerator */
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__TYPE_ENUMERATOR_H */
--- /dev/null
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+#define __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H
+
+namespace CVC4 {
+namespace theory {
+namespace sets {
+
+class SetsTypeRule {
+public:
+
+ /**
+ * Compute the type for (and optionally typecheck) a term belonging
+ * to the theory of sets.
+ *
+ * @param check if true, the node's type should be checked as well
+ * as computed.
+ */
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n,
+ bool check)
+ throw (TypeCheckingExceptionPrivate) {
+
+ // TODO: implement me!
+ Unimplemented();
+
+ }
+
+};/* class SetsTypeRule */
+
+// TODO: Union, Intersection and Setminus should be combined to one check
+struct SetUnionTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::UNION);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set union operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set union operating on sets of different types");
+ }
+ }
+ return setType;
+ }
+};/* struct SetUnionTypeRule */
+
+struct SetIntersectionTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::INTERSECTION);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set intersection operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set intersection operating on sets of different types");
+ }
+ }
+ return setType;
+ }
+};/* struct SetIntersectionTypeRule */
+
+struct SetSetminusTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SETMINUS);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set setminus operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set setminus operating on sets of different types");
+ }
+ }
+ return setType;
+ }
+};/* struct SetSetminusTypeRule */
+
+struct SetSubsetTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SUBSET);
+ TypeNode setType = n[0].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "set subset operating on non-set");
+ }
+ TypeNode secondSetType = n[1].getType(check);
+ if(secondSetType != setType) {
+ throw TypeCheckingExceptionPrivate(n, "set subset operating on sets of different types");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct SetSubsetTypeRule */
+
+struct SetInTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::IN);
+ TypeNode setType = n[1].getType(check);
+ if( check ) {
+ if(!setType.isSet()) {
+ throw TypeCheckingExceptionPrivate(n, "checking for membership in a non-set");
+ }
+ TypeNode elementType = n[0].getType(check);
+ if(elementType != setType.getSetElementType()) {
+ throw TypeCheckingExceptionPrivate(n, "set in operating on sets of different types");
+ }
+ }
+ return nodeManager->booleanType();
+ }
+};/* struct SetInTypeRule */
+
+struct SetSingletonTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+ Assert(n.getKind() == kind::SET_SINGLETON);
+ return nodeManager->mkSetType(n[0].getType(check));
+ }
+};/* struct SetInTypeRule */
+
+struct SetConstTypeRule {
+ inline static bool computeIsConst(NodeManager* nodeManager, TNode n) {
+ switch(n.getKind()) {
+ case kind::SET_SINGLETON:
+ return n[0].isConst();
+ case kind::UNION:
+ return n[0].isConst() && n[1].isConst();
+ default:
+ Unhandled();
+ }
+ }
+};
+
+struct EmptySetTypeRule {
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
+
+ Assert(n.getKind() == kind::EMPTYSET);
+ EmptySet emptySet = n.getConst<EmptySet>();
+ Type setType = emptySet.getType();
+ return TypeNode::fromType(setType);
+ }
+};
+
+
+struct SetsProperties {
+ inline static Cardinality computeCardinality(TypeNode type) {
+ Assert(type.getKind() == kind::SET_TYPE);
+ Cardinality elementCard = type[0].getCardinality();
+ return elementCard;
+ }
+
+ inline static bool isWellFounded(TypeNode type) {
+ return type[0].isWellFounded();
+ }
+
+ inline static Node mkGroundTerm(TypeNode type) {
+ Assert(type.isSet());
+ return NodeManager::currentNM()->mkConst(EmptySet(type.toType()));
+ }
+};
+
+}/* CVC4::theory::sets namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__SETS__THEORY_SETS_TYPE_RULES_H */
* check() or propagate() method called. A Theory may empty its
* assertFact() queue using get(). A Theory can raise conflicts,
* add lemmas, and propagate literals during presolve().
+ *
+ * NOTE: The presolve property must be added to the kinds file for
+ * the theory.
*/
virtual void presolve() { }
void TheoryEngine::postsolve() {
// Reset the interrupt flag
d_interrupted = false;
+ bool CVC4_UNUSED wasInConflict = d_inConflict;
try {
// Definition of the statement that is to be run by every theory
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
if (theory::TheoryTraits<THEORY>::hasPostsolve) { \
theoryOf(THEORY)->postsolve(); \
- Assert(! d_inConflict, "conflict raised during postsolve()"); \
+ Assert(! d_inConflict || wasInConflict, "conflict raised during postsolve()"); \
}
// Postsolve for each theory using the statement above
bool value;
if (d_propEngine->hasValue(assertion, value)) {
if (!value) {
- Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict" << endl;
+ Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
d_inConflict = true;
} else {
return;
// Check for propositional conflicts
bool value;
if (d_propEngine->hasValue(assertion, value) && !value) {
+ Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)" << endl;
d_inConflict = true;
}
}
void addTriggerPredicate(TNode predicate);
/**
- * Returns true if the two are currently in the database and equal.
+ * Returns true if the two terms are equal. Requires both terms to
+ * be in the database.
*/
bool areEqual(TNode t1, TNode t2) const;
/**
- * Check whether the two term are dis-equal.
+ * Check whether the two term are dis-equal. Requires both terms to
+ * be in the database.
*/
bool areDisequal(TNode t1, TNode t2, bool ensureProof) const;
abstract_value.cpp \
array_store_all.h \
array_store_all.cpp \
+ emptyset.h \
+ emptyset.cpp \
model.h \
model.cpp \
sort_inference.h \
--- /dev/null
+#include "util/emptyset.h"
+#include <iostream>
+
+using namespace std;
+
+namespace CVC4 {
+
+std::ostream& operator<<(std::ostream& out, const EmptySet& asa) {
+ return out << "emptyset(" << asa.getType() << ')';
+}
+
+}/* CVC4 namespace */
--- /dev/null
+
+#include "cvc4_public.h"
+
+#pragma once
+
+namespace CVC4 {
+ // messy; Expr needs ArrayStoreAll (because it's the payload of a
+ // CONSTANT-kinded expression), and ArrayStoreAll needs Expr.
+ class CVC4_PUBLIC EmptySet;
+}/* CVC4 namespace */
+
+#include "expr/expr.h"
+#include "expr/type.h"
+#include <iostream>
+
+namespace CVC4 {
+
+class CVC4_PUBLIC EmptySet {
+
+ const SetType d_type;
+
+public:
+
+ EmptySet() { } /* Null typed */
+ EmptySet(SetType t):d_type(t) { }
+
+
+ ~EmptySet() throw() {
+ }
+
+ SetType getType() const { return d_type; }
+
+ bool operator==(const EmptySet& asa) const throw() {
+ return d_type == asa.d_type;
+ }
+ bool operator!=(const EmptySet& asa) const throw() {
+ return !(*this == asa);
+ }
+
+ bool operator<(const EmptySet& asa) const throw() {
+ return d_type < asa.d_type;
+ }
+ bool operator<=(const EmptySet& asa) const throw() {
+ return d_type <= asa.d_type;
+ }
+ bool operator>(const EmptySet& asa) const throw() {
+ return !(*this <= asa);
+ }
+ bool operator>=(const EmptySet& asa) const throw() {
+ return !(*this < asa);
+ }
+
+
+};/* class EmptySet */
+
+std::ostream& operator<<(std::ostream& out, const EmptySet& asa) CVC4_PUBLIC;
+
+struct CVC4_PUBLIC EmptySetHashFunction {
+ inline size_t operator()(const EmptySet& asa) const {
+ return TypeHashFunction()(asa.getType());
+ }
+};/* struct EmptysetHashFunction */
+
+
+}
regress/regress0/decision \
regress/regress0/fmf \
regress/regress0/strings \
+ regress/regress0/sets \
regress/regress1 \
regress/regress1/arith \
regress/regress2 \
-SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings
-DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings
+SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
+DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
# don't override a BINARY imported from a personal.mk
@mk_if@eq ($(BINARY),)
(set-logic AUFLIA)
-(set-info :source | Set theory. |)
+(set-info :source | mySet theory. |)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(set-info :status unsat)
-(declare-sort Set 0)
+(declare-sort mySet 0)
(declare-sort Elem 0)
-(declare-fun member (Elem Set) Bool)
-(declare-fun subset (Set Set) Bool)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
-(assert (forall ((?s1 Set) (?s2 Set)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
-(assert (forall ((?s1 Set) (?s2 Set)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
-(declare-fun seteq (Set Set) Bool)
-(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
-(assert (forall ((?s1 Set) (?s2 Set)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
-(declare-fun union (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (union ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
-(declare-fun intersection (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (intersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
-(declare-fun difference (Set Set) Set)
-(assert (forall ((?x Elem) (?s1 Set) (?s2 Set)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
-(declare-fun a () Set)
-(declare-fun b () Set)
-(assert (not (seteq (intersection a b) (intersection b a))))
+(declare-fun member (Elem mySet) Bool)
+(declare-fun subset (mySet mySet) Bool)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (=> (and (member ?x ?s1) (subset ?s1 ?s2)) (member ?x ?s2))))
+(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (not (subset ?s1 ?s2)) (exists ((?x Elem)) (and (member ?x ?s1) (not (member ?x ?s2)))))))
+(assert (forall ((?s1 mySet) (?s2 mySet)) (=> (forall ((?x Elem)) (=> (member ?x ?s1) (member ?x ?s2))) (subset ?s1 ?s2))))
+(declare-fun seteq (mySet mySet) Bool)
+(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (= ?s1 ?s2))))
+(assert (forall ((?s1 mySet) (?s2 mySet)) (= (seteq ?s1 ?s2) (and (subset ?s1 ?s2) (subset ?s2 ?s1)))))
+(declare-fun myunion (mySet mySet) mySet)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myunion ?s1 ?s2)) (or (member ?x ?s1) (member ?x ?s2)))))
+(declare-fun myintersection (mySet mySet) mySet)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (myintersection ?s1 ?s2)) (and (member ?x ?s1) (member ?x ?s2)))))
+(declare-fun difference (mySet mySet) mySet)
+(assert (forall ((?x Elem) (?s1 mySet) (?s2 mySet)) (= (member ?x (difference ?s1 ?s2)) (and (member ?x ?s1) (not (member ?x ?s2))))))
+(declare-fun a () mySet)
+(declare-fun b () mySet)
+(assert (not (seteq (myintersection a b) (myintersection b a))))
(check-sat)
(exit)
(set-logic AUFLIA)
(set-info :status unsat)
-;; don't use a datatypes for currently focusing in uf
+;; don't use a datatypes for currently focusing my_in uf
(declare-sort elt 0)
(declare-sort set 0)
-(declare-fun in (elt set) Bool)
+(declare-fun my_in (elt set) Bool)
;;;;;;;;;;;;;;;;;;;;
;; inter
(declare-fun inter (set set) set)
(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
- ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
+ ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
+ (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
+ (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
+ () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
+ () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
+ (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
;;;;;;;;;;;;;;;;;
;; union
-(declare-fun union (set set) set)
+(declare-fun my_union (set set) set)
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
+ () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
+ (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
+ (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
+ () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
+ () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
+ (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
;;;;;;;;;;;;;;;;;;;;
;; diff
(declare-fun diff (set set) set)
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
+ () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
+ (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
+ (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
+ () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
+ () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
+ (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
;;;;;;;;;;;;;;;;
;;sing
(declare-fun sing (elt) set)
(assert-propagation ((?s elt))
- (((sing ?s))) () () (in ?s (sing ?s)) )
+ (((sing ?s))) () () (my_in ?s (sing ?s)) )
(assert-propagation ((?s elt) (?t1 elt))
- () () ((in ?s (sing ?t1))) (= ?s ?t1))
+ () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
(assert-propagation ((?s elt) (?t1 elt))
- () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
+ () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
;;;;;;;;;;;;;;;;;;;
;; fullfiling runned at Full effort
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
+ () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
+ (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
(assert-propagation ((?t1 set) (?t2 set))
- () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
+ () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2)))))
;;;;;;;;;;;;;;;;;;;
;; shortcut
(declare-fun subset (set set) Bool)
(assert-reduction ((?t1 set) (?t2 set))
- () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
+ () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
(declare-fun e () elt)
(declare-fun t1 () set)
(declare-fun t2 () set)
(declare-fun t3 () set)
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1)))))
+;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1))))
;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
+;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1))))
-;;(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t1 t2) t3))))) )
-(assert (not (= (union t1 (union t2 t3)) (union (union t1 t2) t3))) )
+;;(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t1 t2) t3))))) )
+(assert (not (= (my_union t1 (my_union t2 t3)) (my_union (my_union t1 t2) t3))) )
(check-sat)
(set-logic AUFLIA)
(set-info :status sat)
-;; don't use a datatypes for currently focusing in uf
+;; don't use a datatypes for currently focusing my_in uf
(declare-sort elt 0)
(declare-sort set 0)
-(declare-fun in (elt set) Bool)
+(declare-fun my_in (elt set) Bool)
;;;;;;;;;;;;;;;;;;;;
(declare-fun inter (set set) set)
(assert-propagation ((?s elt) (?t1 set) (?t2 set)) () ()
- ((in ?s (inter ?t1 ?t2))) (and (in ?s ?t1) (in ?s ?t2)))
+ ((my_in ?s (inter ?t1 ?t2))) (and (my_in ?s ?t1) (my_in ?s ?t2)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (inter ?t1 ?t2))) )
+ (((inter ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (inter ?t1 ?t2))) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((not (in ?s ?t2))) (not (in ?s (inter ?t1 ?t2))) )
+ (((inter ?t1 ?t2))) () ((not (my_in ?s ?t2))) (not (my_in ?s (inter ?t1 ?t2))) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t1)) (not (in ?s ?t2)) )
+ () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t1)) (not (my_in ?s ?t2)) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (inter ?t1 ?t2))) (in ?s ?t2)) (not (in ?s ?t1)))
+ () () ((not (my_in ?s (inter ?t1 ?t2))) (my_in ?s ?t2)) (not (my_in ?s ?t1)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((in ?s ?t1) (in ?s ?t2)) (in ?s (inter ?t1 ?t2)) )
+ (((inter ?t1 ?t2))) () ((my_in ?s ?t1) (my_in ?s ?t2)) (my_in ?s (inter ?t1 ?t2)) )
;;;;;;;;;;;;;;;;;
;; union
-(declare-fun union (set set) set)
+(declare-fun my_union (set set) set)
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (union ?t1 ?t2)))) (and (not (in ?s ?t1)) (not (in ?s ?t2))))
+ () () ((not (my_in ?s (my_union ?t1 ?t2)))) (and (not (my_in ?s ?t1)) (not (my_in ?s ?t2))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((union ?t1 ?t2))) () ((in ?s ?t1)) (in ?s (union ?t1 ?t2)))
+ (((my_union ?t1 ?t2))) () ((my_in ?s ?t1)) (my_in ?s (my_union ?t1 ?t2)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((union ?t1 ?t2))) () ((in ?s ?t2)) (in ?s (union ?t1 ?t2)))
+ (((my_union ?t1 ?t2))) () ((my_in ?s ?t2)) (my_in ?s (my_union ?t1 ?t2)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t1))) (in ?s ?t2))
+ () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t1))) (my_in ?s ?t2))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (union ?t1 ?t2)) (not (in ?s ?t2))) (in ?s ?t1))
+ () () ((my_in ?s (my_union ?t1 ?t2)) (not (my_in ?s ?t2))) (my_in ?s ?t1))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((union ?t1 ?t2))) () ((not (in ?s ?t1)) (not (in ?s ?t2))) (not (in ?s (union ?t1 ?t2))))
+ (((my_union ?t1 ?t2))) () ((not (my_in ?s ?t1)) (not (my_in ?s ?t2))) (not (my_in ?s (my_union ?t1 ?t2))))
;;;;;;;;;;;;;;;;;;;;
;; diff
(declare-fun diff (set set) set)
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (diff ?t1 ?t2))) (and (in ?s ?t1) (not (in ?s ?t2))))
+ () () ((my_in ?s (diff ?t1 ?t2))) (and (my_in ?s ?t1) (not (my_in ?s ?t2))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((diff ?t1 ?t2))) () ((not (in ?s ?t1))) (not (in ?s (diff ?t1 ?t2))) )
+ (((diff ?t1 ?t2))) () ((not (my_in ?s ?t1))) (not (my_in ?s (diff ?t1 ?t2))) )
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((diff ?t1 ?t2))) () ((in ?s ?t2)) (not (in ?s (diff ?t1 ?t2))))
+ (((diff ?t1 ?t2))) () ((my_in ?s ?t2)) (not (my_in ?s (diff ?t1 ?t2))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (diff ?t1 ?t2))) (in ?s ?t1)) (in ?s ?t2))
+ () () ((not (my_in ?s (diff ?t1 ?t2))) (my_in ?s ?t1)) (my_in ?s ?t2))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((not (in ?s (diff ?t1 ?t2))) (not (in ?s ?t2))) (not (in ?s ?t1)))
+ () () ((not (my_in ?s (diff ?t1 ?t2))) (not (my_in ?s ?t2))) (not (my_in ?s ?t1)))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((diff ?t1 ?t2))) () ((in ?s ?t1) (not (in ?s ?t2))) (in ?s (diff ?t1 ?t2)) )
+ (((diff ?t1 ?t2))) () ((my_in ?s ?t1) (not (my_in ?s ?t2))) (my_in ?s (diff ?t1 ?t2)) )
;;;;;;;;;;;;;;;;
;;sing
(declare-fun sing (elt) set)
(assert-propagation ((?s elt))
- (((sing ?s))) () () (in ?s (sing ?s)) )
+ (((sing ?s))) () () (my_in ?s (sing ?s)) )
(assert-propagation ((?s elt) (?t1 elt))
- () () ((in ?s (sing ?t1))) (= ?s ?t1))
+ () () ((my_in ?s (sing ?t1))) (= ?s ?t1))
(assert-propagation ((?s elt) (?t1 elt))
- () () ((not (in ?s (sing ?t1)))) (not (= ?s ?t1)))
+ () () ((not (my_in ?s (sing ?t1)))) (not (= ?s ?t1)))
;;;;;;;;;;;;;;;;;;;
;; fullfiling runned at Full effort
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- () () ((in ?s (union ?t1 ?t2))) (or (in ?s ?t1) (not (in ?s ?t1))))
+ () () ((my_in ?s (my_union ?t1 ?t2))) (or (my_in ?s ?t1) (not (my_in ?s ?t1))))
(assert-propagation ((?s elt) (?t1 set) (?t2 set))
- (((inter ?t1 ?t2))) () ((in ?s ?t1)) (or (in ?s ?t2) (not (in ?s ?t2))))
+ (((inter ?t1 ?t2))) () ((my_in ?s ?t1)) (or (my_in ?s ?t2) (not (my_in ?s ?t2))))
(assert-propagation ((?t1 set) (?t2 set))
- () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (in ?e ?t1) (not (in ?e ?t2))) (and (not (in ?e ?t1)) (in ?e ?t2)))))
+ () () ((not (= ?t1 ?t2))) (exists ((?e elt)) (or (and (my_in ?e ?t1) (not (my_in ?e ?t2))) (and (not (my_in ?e ?t1)) (my_in ?e ?t2)))))
;;;;;;;;;;;;;;;;;;;
;; shortcut
(declare-fun subset (set set) Bool)
(assert-reduction ((?t1 set) (?t2 set))
- () () ((subset ?t1 ?t2)) (= (union ?t1 ?t2) ?t2))
+ () () ((subset ?t1 ?t2)) (= (my_union ?t1 ?t2) ?t2))
(declare-fun e () elt)
(declare-fun t1 () set)
(declare-fun t2 () set)
(declare-fun t3 () set)
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e (union t1 t1)))))
-;;(assert (not (=> (in e (union t1 t1)) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e (my_union t1 t1)))))
+;;(assert (not (=> (my_in e (my_union t1 t1)) (my_in e t1))))
;; hyp
-;;(assert (=> (in e (union t1 t1)) (in e t1)))
+;;(assert (=> (my_in e (my_union t1 t1)) (my_in e t1)))
-;;(assert (not (=> (in e (inter (union t1 t2) (union t1 t1))) (in e t1))))
+;;(assert (not (=> (my_in e (inter (my_union t1 t2) (my_union t1 t1))) (my_in e t1))))
-(assert (or (and (not (in e (union t1 (union t2 t3)))) (in e (union (union t1 t2) t3))) (and (in e (union t1 (union t2 t3))) (not (in e (union (union t2 t2) t3))))) )
+(assert (or (and (not (my_in e (my_union t1 (my_union t2 t3)))) (my_in e (my_union (my_union t1 t2) t3))) (and (my_in e (my_union t1 (my_union t2 t3))) (not (my_in e (my_union (my_union t2 t2) t3))))) )
(check-sat)
--- /dev/null
+topdir = ../../../..
+srcdir = test/regress/regress0/sets
+
+include $(topdir)/Makefile.subdir
+
+# synonyms for "check"
+.PHONY: test
+test: check
--- /dev/null
+# don't override a BINARY imported from a personal.mk
+@mk_if@eq ($(BINARY),)
+@mk_empty@BINARY = cvc4
+end@mk_if@
+
+LOG_COMPILER = @srcdir@/../../run_regression
+AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT)
+
+if AUTOMAKE_1_11
+# old-style (pre-automake 1.12) test harness
+TESTS_ENVIRONMENT = \
+ $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \
+ $(AM_LOG_FLAGS) $(LOG_FLAGS)
+endif
+
+# These are run for all build profiles.
+# If a test shouldn't be run in e.g. competition mode,
+# put it below in "TESTS +="
+TESTS = \
+ union-1b-flip.smt2 \
+ sets-sharing.smt2 \
+ union-1a-flip.smt2 \
+ copy_check_heap_access_33_4.smt2 \
+ rec_copy_loop_check_heap_access_43_4.smt2 \
+ sets-testlemma.smt2 \
+ jan24/insert_invariant_37_2.smt2 \
+ jan24/deepmeas0.hs.fqout.cvc4.47.smt2 \
+ jan24/deepmeas0.hs.fqout.small.smt2 \
+ jan24/remove_check_free_31_6.smt2 \
+ sets-inter.smt2 \
+ sets-equal.smt2 \
+ union-2.smt2 \
+ jan27/deepmeas0.hs.fqout.cvc4.41.smt2 \
+ jan27/ListConcat.hs.fqout.cvc4.177.smt2 \
+ jan27/ListConcat.hs.fqout.177minimized.smt2 \
+ jan27/ListElem.hs.fqout.cvc4.38.smt2 \
+ feb3/ListElts.hs.fqout.cvc4.317.smt2 \
+ setel-eq.smt2 \
+ sets-new.smt2 \
+ jan30/UniqueZipper.hs.fqout.minimized10.smt2 \
+ jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 \
+ jan30/UniqueZipper.hs.fqout.minimized1832.smt2 \
+ jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 \
+ emptyset.smt2 \
+ sets-union.smt2 \
+ error2.smt2 \
+ union-1b.smt2 \
+ union-1a.smt2 \
+ error1.smt2 \
+ jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 \
+ jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 \
+ sets-sample.smt2 \
+ eqtest.smt2 \
+ emptyset.smt2 \
+ error2.smt2
+
+EXTRA_DIST = $(TESTS)
+
+#if CVC4_BUILD_PROFILE_COMPETITION
+#else
+#TESTS += \
+# error.cvc
+#endif
+#
+# and make sure to distribute it
+#EXTRA_DIST += \
+# error.cvc
+
+# synonyms for "check"
+.PHONY: regress regress0 test
+regress regress0 test: check
+
+# do nothing in this subdir
+.PHONY: regress1 regress2 regress3
+regress1 regress2 regress3:
--- /dev/null
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldInt Loc) Int)
+(declare-fun read$1 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Alloc_1$0 () SetLoc)
+(declare-fun Axiom_1$0 () Bool)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_1$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun cp_2$0 () Loc)
+(declare-fun curr_2$0 () Loc)
+(declare-fun data$0 () FldInt)
+(declare-fun lst$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun res_1$0 () Loc)
+(declare-fun sk_?X_4$0 () SetLoc)
+(declare-fun slseg_domain$0 (FldInt FldLoc Loc Loc) SetLoc)
+(declare-fun slseg_struct$0 (SetLoc FldInt FldLoc Loc Loc) Bool)
+(declare-fun tmp_2$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+ (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+ (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y)))
+ :named btwn_reach_1))
+
+(assert (! (forall ((?y Loc))
+ (or (not (= (read$1 next$0 null$0) null$0))
+ (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+ :named btwn_cycl_1))
+
+(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0))
+ :named btwn_step_1))
+
+(assert (! (forall ((l1 Loc) (l2 Loc))
+ (or (not Axiom_1$0)
+ (or (<= (read$0 data$0 l1) (read$0 data$0 l2))
+ (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X_4$0))
+ (not (in l2 sk_?X_4$0)))))
+ :named sortedness_3))
+
+(assert (! (= (read$1 next$0 null$0) null$0) :named read_null_1))
+
+(assert (! (not (in tmp_2$0 Alloc$0)) :named new_31_11))
+
+(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_copy_23_11_2))
+
+(assert (! (not (= lst$0 null$0)) :named if_else_26_6))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+ :named precondition_of_copy_23_11_4))
+
+(assert (! (= sk_?X_4$0 FP$0) :named precondition_of_copy_23_11_5))
+
+(assert (! (= res_1$0 tmp_2$0) :named assign_31_4))
+
+(assert (! (= cp_2$0 res_1$0) :named assign_32_4))
+
+(assert (! (= FP_1$0 (union FP$0 (setenum tmp_2$0))) :named assign_31_11))
+
+(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom_1$0)
+ (not (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0)))
+ :named unnamed_3))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 lst$0 l1 null$0)
+ (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0))
+ (not (= l1 null$0)))
+ (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0)))
+ (not (in l1 (slseg_domain$0 data$0 next$0 lst$0 null$0))))))
+ :named slseg_footprint_2))
+
+(assert (! (not (in curr_2$0 FP_1$0)) :named check_heap_access_33_4))
+
+(assert (! (not (= tmp_2$0 null$0)) :named new_31_11_1))
+
+(assert (! (slseg_struct$0 sk_?X_4$0 data$0 next$0 lst$0 null$0)
+ :named precondition_of_copy_23_11_6))
+
+(assert (! (= sk_?X_4$0 (slseg_domain$0 data$0 next$0 lst$0 null$0))
+ :named precondition_of_copy_23_11_7))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+ :named initial_footprint_of_copy_23_11_3))
+
+(assert (! (= curr_2$0 lst$0) :named assign_30_4))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_26_2_1))
+
+(assert (! (= Alloc_1$0 (union Alloc$0 (setenum tmp_2$0))) :named assign_31_11_1))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_1))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+ :named btwn_sndw_1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+ (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+ :named btwn_ord1_1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z))
+ (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+ :named btwn_ord2_1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+ (Btwn$0 next$0 ?x ?z ?z)))
+ :named btwn_trn1_1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+ (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+ :named btwn_trn2_1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+ (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+ :named btwn_trn3_1))
+
+(check-sat)
+(exit)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(assert (in 5 (as emptyset (Set Int) )))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(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 G () (Set Int) )
+(declare-fun H () (Set Int) )
+(declare-fun I () (Set Int) )
+(declare-fun x () Int)
+(assert (in x (intersection (union A B) C)))
+(assert (not (in x G)))
+(assert (= (union A B) D))
+(assert (= C (intersection E F)))
+(assert (and (= F H) (= G H) (= H I)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun A () (Set Int))
+(declare-fun C () (Set Int))
+(declare-fun D () (Set Int))
+(declare-fun E () (Set Int))
+(set-info :status sat)
+
+(assert (= A (union D C)))
+(assert (not (= A (union E A))))
+
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(assert (= (as emptyset (Set Int)) (setenum 5)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v67 () Int)
+(declare-fun z3f68 (Int) Int)
+(declare-fun z3f69 (Int) mySet)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3f71 (Int) Bool)
+(declare-fun z3v73 () Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v84 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3f96 () Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(declare-fun z3v100 () Int)
+(declare-fun z3v101 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v104 () Int)
+(declare-fun z3v107 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v113 () Int)
+(declare-fun z3v116 () Int)
+(declare-fun z3v117 () Int)
+(declare-fun z3v118 () Int)
+(declare-fun z3v119 () Int)
+(declare-fun z3v120 () Int)
+(declare-fun z3v121 () Int)
+(declare-fun z3v122 () Int)
+(declare-fun z3v123 () Int)
+(declare-fun z3v124 () Int)
+(declare-fun z3v125 () Int)
+(declare-fun z3v127 () Int)
+(declare-fun z3v130 () Int)
+(declare-fun z3v133 () Int)
+(declare-fun z3v134 () Int)
+(declare-fun z3v135 () Int)
+(declare-fun z3v136 () Int)
+(declare-fun z3v137 () Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v143 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v147 () Int)
+(declare-fun z3v150 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v152 () Int)
+(assert (= (z3f69 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v151))))
+(assert (= (z3f70 z3v152) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v151))))
+(assert (= (z3f68 z3v152) (+ 1 (z3f68 z3v151))))
+(assert (= (z3f71 z3v152) false))
+(assert (and (>= (z3f68 z3v140) 0) (>= (z3f68 z3v141) 0) (>= (z3f68 z3v151) 0) (>= (z3f68 z3v142) 0) (= (z3f69 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f69 z3v141))) (= (z3f70 z3v142) (smt_set_cup (smt_set_add smt_set_emp z3v143) (z3f70 z3v141))) (= (z3f68 z3v142) (+ 1 (z3f68 z3v141))) (= (z3f71 z3v142) false) (= z3v142 (z3f92 z3v143 z3v141)) (>= (z3f68 z3v142) 0) (= z3v142 z3v144) (>= (z3f68 z3v142) 0) (>= (z3f68 z3v144) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64)))
+(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v141))))
+(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140))))
+(assert (= (z3f69 z3v151) (smt_set_cup (z3f69 z3v141) (z3f69 z3v140))))
+(assert (smt_set_sub (z3f69 z3v151) (z3f69 z3v140)))
+(assert (= (z3f69 z3v151) (z3f69 z3v140)))
+(assert (<= z3v151 z3v140))
+(assert (>= z3v151 z3v140))
+(assert (<= (z3f68 z3v151) (z3f68 z3v140)))
+(assert (>= (z3f68 z3v151) (z3f68 z3v141)))
+(assert (>= (z3f68 z3v151) (z3f68 z3v140)))
+(assert (= (z3f68 z3v151) (z3f68 z3v140)))
+(assert (= z3v151 z3v140))
+(assert (>= (z3f68 z3v151) 0))
+(assert (not (= (z3f69 z3v152) (smt_set_cup (z3f69 z3v140) (z3f69 z3v140)))))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3f67 (Int) mySet)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3f83 (Int) Int)
+(declare-fun z3f84 (Int) Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3f86 (Int) Int)
+(declare-fun z3f87 (Int Int) Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3f90 (Int) mySet)
+(declare-fun z3f91 (Int) Bool)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3v95 () Int)
+(declare-fun z3v96 () Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v99 () Int)
+
+(assert (= z3v99 z3v89))
+(assert (>= (z3f70 z3v99) 0))
+
+(assert (and (not (z3f60 z3v79))
+ (not (z3f60 z3v79))
+ (= z3v79 z3v80)
+ (= (z3f60 z3v79)
+ (= z3v76 z3v81))
+ (= (z3f60 z3v80)
+ (= z3v76 z3v81))
+ (= (z3f83 z3v82) z3v81)
+ (= (z3f91 z3v78) false)
+ (= z3v78 (z3f92 z3v88 z3v89))
+ (= z3v82 z3v88)
+ (= (z3f67 z3v78)
+ (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88))
+ (z3f67 z3v89)))
+ (= (z3f62 z3v64) z3v64)))
+
+(assert (smt_set_mem z3v76 (z3f67 z3v78)))
+(assert (<= z3v95 z3v93))
+(assert (>= z3v95 z3v93))
+(assert (not (smt_set_mem z3v76 (z3f67 z3v99))))
+(check-sat)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+
+(assert (in x S))
+
+(assert (= S (union T (setenum y))))
+
+(assert (not (= x y)))
+
+(assert (not (in x T)))
+
+(check-sat)
--- /dev/null
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldInt Loc) Int)
+(declare-fun read$1 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Axiom$0 () Bool)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun c1_2$0 () SetInt)
+(declare-fun c2_2$0 () SetInt)
+(declare-fun content$0 () SetInt)
+(declare-fun curr_2$0 () Loc)
+(declare-fun data$0 () FldInt)
+(declare-fun lst$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun prev_2$0 () Loc)
+(declare-fun sk_?X$0 () SetLoc)
+(declare-fun sk_?X_1$0 () SetLoc)
+(declare-fun sk_?X_2$0 () SetLoc)
+(declare-fun sk_?X_3$0 () SetLoc)
+(declare-fun sk_?X_4$0 () SetLoc)
+(declare-fun sk_?X_5$0 () SetLoc)
+(declare-fun sk_?e$0 () Int)
+(declare-fun sk_?e_1$0 () Loc)
+(declare-fun sk_?e_2$0 () Loc)
+(declare-fun sk_?e_3$0 () Int)
+(declare-fun sk_FP$0 () SetLoc)
+(declare-fun sk_FP_1$0 () SetLoc)
+(declare-fun sk_l1$0 () Loc)
+(declare-fun sk_l1_1$0 () Loc)
+(declare-fun sk_l2$0 () Loc)
+(declare-fun sk_l2_1$0 () Loc)
+(declare-fun sorted_set_c$0 (FldInt FldLoc Loc Loc) SetInt)
+(declare-fun sorted_set_domain$0 (FldInt FldLoc Loc Loc) SetLoc)
+(declare-fun sorted_set_struct$0 (SetLoc FldInt FldLoc Loc Loc SetInt) Bool)
+(declare-fun val$0 () Int)
+(declare-fun witness$0 (Int SetInt) Loc)
+
+(assert (! (forall ((?y Loc))
+ (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+ (Btwn$0 next$0 null$0 (read$1 next$0 null$0) ?y)))
+ :named btwn_reach))
+
+(assert (! (forall ((?y Loc))
+ (or (not (= (read$1 next$0 null$0) null$0))
+ (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+ :named btwn_cycl))
+
+(assert (! (Btwn$0 next$0 null$0 (read$1 next$0 null$0) (read$1 next$0 null$0))
+ :named btwn_step))
+
+(assert (! (forall ((l1 Loc) (l2 Loc))
+ (or (not Axiom$0)
+ (or (= l1 l2) (< (read$0 data$0 l1) (read$0 data$0 l2))
+ (not (Btwn$0 next$0 l1 l2 null$0)) (not (in l1 sk_?X$0))
+ (not (in l2 sk_?X$0)))))
+ :named strict_sortedness))
+
+(assert (! (forall ((l1 Loc))
+ (or (= l1 null$0)
+ (in (read$0 data$0 l1)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (not (Btwn$0 next$0 lst$0 l1 null$0))))
+ :named sorted_set_1))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 curr_2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not
+ (in (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 prev_2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not
+ (in (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_1))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_2))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l1_1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_3))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_4))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l2_1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_5))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= sk_?e$0
+ (read$0 data$0
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_6))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ null$0)
+ (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))
+ (or
+ (and
+ (= sk_?e_3$0
+ (read$0 data$0
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))))
+ (in
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0)))
+ (not (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0)))))
+ :named sorted_set_2_7))
+
+(assert (! (forall ((l1 Loc))
+ (or (= l1 null$0)
+ (in (read$0 data$0 l1)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (not (Btwn$0 next$0 curr_2$0 l1 null$0))))
+ :named sorted_set_1_1))
+
+(assert (! (forall ((l1 Loc))
+ (or (= l1 curr_2$0)
+ (in (read$0 data$0 l1)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (not (Btwn$0 next$0 lst$0 l1 curr_2$0))))
+ :named sorted_set_1_2))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 curr_2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_8))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 prev_2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_9))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_10))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l1_1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_11))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_12))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l2_1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_13))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= sk_?e$0
+ (read$0 data$0
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_14))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ null$0)
+ (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))
+ (or
+ (and
+ (= sk_?e_3$0
+ (read$0 data$0
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (in
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0)))
+ (not
+ (in sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0)))))
+ :named sorted_set_2_15))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= (read$0 data$0 curr_2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in (read$0 data$0 curr_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_16))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= (read$0 data$0 prev_2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in (read$0 data$0 prev_2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_17))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in (read$0 data$0 sk_l1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_18))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l1_1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in (read$0 data$0 sk_l1_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_19))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l2$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in (read$0 data$0 sk_l2$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_20))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= (read$0 data$0 sk_l2_1$0)
+ (read$0 data$0
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in (read$0 data$0 sk_l2_1$0)
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_21))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= sk_?e$0
+ (read$0 data$0
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 sk_?e$0
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_22))
+
+(assert (! (and
+ (or
+ (=
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ null$0)
+ (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))
+ (or
+ (and
+ (= sk_?e_3$0
+ (read$0 data$0
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (in
+ (witness$0 sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0)))
+ (not
+ (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0)))))
+ :named sorted_set_2_23))
+
+(assert (! (= (read$1 next$0 null$0) null$0) :named read_null))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 lst$0 l1 null$0)
+ (in l1 (sorted_set_domain$0 data$0 next$0 lst$0 null$0))
+ (not (= l1 null$0)))
+ (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0)))
+ (not
+ (in l1
+ (sorted_set_domain$0 data$0 next$0 lst$0 null$0))))))
+ :named sorted_set_footprint))
+
+(assert (! (or (in sk_?e_3$0 c2_2$0)
+ (and (in sk_?e_2$0 sk_FP_1$0) (not (in sk_?e_2$0 FP$0)))
+ (and (in sk_?e_3$0 (union c1_2$0 c2_2$0))
+ (not (in sk_?e_3$0 content$0)))
+ (and (in sk_?e_3$0 c1_2$0)
+ (not
+ (in sk_?e_3$0
+ (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (and (in sk_?e_3$0 content$0)
+ (not (in sk_?e_3$0 (union c1_2$0 c2_2$0))))
+ (and (in sk_?e_3$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (not (in sk_?e_3$0 c1_2$0)))
+ (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0))
+ (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0))))
+ (not (= curr_2$0 lst$0)) (not (= prev_2$0 null$0))
+ (not
+ (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0
+ c1_2$0)))
+ :named invariant_37_2))
+
+(assert (! (= sk_FP_1$0 sk_?X_2$0) :named invariant_37_2_1))
+
+(assert (! (= sk_?X_5$0 (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))
+ :named invariant_37_2_2))
+
+(assert (! (= sk_?X_3$0 (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))
+ :named invariant_37_2_3))
+
+(assert (! (= sk_?X_1$0 (union sk_?X_3$0 sk_?X_4$0)) :named invariant_37_2_4))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+ :named precondition_of_insert_27_11))
+
+(assert (! (= sk_?X$0 FP$0) :named precondition_of_insert_27_11_1))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+ :named initial_footprint_of_insert_27_11))
+
+(assert (! (= curr_2$0 lst$0) :named assign_31_2))
+
+(assert (! (= c1_2$0 content$0) :named assign_34_2))
+
+(assert (! (or (and (Btwn$0 next$0 lst$0 null$0 null$0) Axiom$0)
+ (not
+ (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0
+ content$0)))
+ :named unnamed))
+
+(assert (! (or (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0 c1_2$0)
+ (not (Btwn$0 next$0 curr_2$0 null$0 null$0))
+ (! (and (Btwn$0 next$0 sk_l1$0 sk_l2$0 null$0) (in sk_l1$0 sk_?X_3$0)
+ (in sk_l2$0 sk_?X_3$0) (not (= sk_l1$0 sk_l2$0))
+ (not (< (read$0 data$0 sk_l1$0) (read$0 data$0 sk_l2$0))))
+ :named strict_sortedness_1))
+ :named unnamed_1))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
+ (in l1
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))
+ (not (= l1 curr_2$0)))
+ (and
+ (or (= l1 curr_2$0)
+ (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))
+ (not
+ (in l1
+ (sorted_set_domain$0 data$0 next$0 lst$0 curr_2$0))))))
+ :named sorted_set_footprint_1))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 curr_2$0 l1 null$0)
+ (in l1
+ (sorted_set_domain$0 data$0 next$0 curr_2$0 null$0))
+ (not (= l1 null$0)))
+ (and
+ (or (= l1 null$0)
+ (not (Btwn$0 next$0 curr_2$0 l1 null$0)))
+ (not
+ (in l1
+ (sorted_set_domain$0 data$0 next$0 curr_2$0
+ null$0))))))
+ :named sorted_set_footprint_2))
+
+(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_insert_27_11_1))
+
+(assert (! (or (= prev_2$0 curr_2$0)
+ (in sk_?e_1$0 (intersection sk_?X_4$0 sk_?X_3$0))
+ (and (in sk_?e_1$0 sk_FP$0) (not (in sk_?e_1$0 FP$0)))
+ (and (in sk_?e$0 (union c1_2$0 c2_2$0)) (not (in sk_?e$0 content$0)))
+ (and (in sk_?e$0 c1_2$0)
+ (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))))
+ (and (in sk_?e$0 c2_2$0)
+ (not (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))))
+ (and (in sk_?e$0 content$0) (not (in sk_?e$0 (union c1_2$0 c2_2$0))))
+ (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 curr_2$0 null$0))
+ (not (in sk_?e$0 c1_2$0)))
+ (and (in sk_?e$0 (sorted_set_c$0 data$0 next$0 lst$0 curr_2$0))
+ (not (in sk_?e$0 c2_2$0)))
+ (and (not (= curr_2$0 null$0)) (not (= prev_2$0 null$0))
+ (not (< (read$0 data$0 prev_2$0) (read$0 data$0 curr_2$0))))
+ (not (= (read$1 next$0 prev_2$0) curr_2$0))
+ (not (> val$0 (read$0 data$0 prev_2$0)))
+ (not (Btwn$0 next$0 lst$0 prev_2$0 curr_2$0))
+ (not
+ (sorted_set_struct$0 sk_?X_3$0 data$0 next$0 curr_2$0 null$0
+ c1_2$0))
+ (not
+ (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0
+ c2_2$0)))
+ :named invariant_37_2_5))
+
+(assert (! (= sk_FP$0 sk_?X_1$0) :named invariant_37_2_6))
+
+(assert (! (= sk_?X_4$0 sk_?X_5$0) :named invariant_37_2_7))
+
+(assert (! (= sk_?X_2$0 sk_?X_3$0) :named invariant_37_2_8))
+
+(assert (! (sorted_set_struct$0 sk_?X$0 data$0 next$0 lst$0 null$0 content$0)
+ :named precondition_of_insert_27_11_2))
+
+(assert (! (= sk_?X$0 (sorted_set_domain$0 data$0 next$0 lst$0 null$0))
+ :named precondition_of_insert_27_11_3))
+
+(assert (! (= content$0 (sorted_set_c$0 data$0 next$0 lst$0 null$0))
+ :named precondition_of_insert_27_11_4))
+
+(assert (! (= prev_2$0 null$0) :named assign_32_2))
+
+(assert (! (= c2_2$0 (as emptyset SetInt)) :named assign_35_2))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_29_0))
+
+(assert (! (or (sorted_set_struct$0 sk_?X_5$0 data$0 next$0 lst$0 curr_2$0 c2_2$0)
+ (not (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0))
+ (! (and (Btwn$0 next$0 sk_l1_1$0 sk_l2_1$0 curr_2$0)
+ (in sk_l1_1$0 sk_?X_5$0) (in sk_l2_1$0 sk_?X_5$0)
+ (not (= sk_l1_1$0 sk_l2_1$0))
+ (not (< (read$0 data$0 sk_l1_1$0) (read$0 data$0 sk_l2_1$0))))
+ :named strict_sortedness_2))
+ :named unnamed_2))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+ :named btwn_sndw))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+ (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+ :named btwn_ord1))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z))
+ (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+ :named btwn_ord2))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+ (Btwn$0 next$0 ?x ?z ?z)))
+ :named btwn_trn1))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+ (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+ :named btwn_trn2))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+ (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+ :named btwn_trn3))
+
+(check-sat)
+(exit)
--- /dev/null
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldLoc Loc) Loc)
+(declare-fun write$0 (FldLoc Loc Loc) FldLoc)
+(declare-fun ep$0 (FldLoc SetLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Frame$0 (SetLoc SetLoc FldLoc FldLoc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_1$0 () SetLoc)
+(declare-fun FP_2$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_1$0 () SetLoc)
+(declare-fun curr_2$0 () Loc)
+(declare-fun curr_3$0 () Loc)
+(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc)
+(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool)
+(declare-fun lst$0 () Loc)
+(declare-fun lst_1$0 () Loc)
+(declare-fun next$0 () FldLoc)
+(declare-fun next_1$0 () FldLoc)
+(declare-fun nondet_2$0 () Bool)
+(declare-fun sk_?X_27$0 () SetLoc)
+(declare-fun sk_?X_28$0 () SetLoc)
+(declare-fun sk_?X_29$0 () SetLoc)
+(declare-fun sk_?X_30$0 () SetLoc)
+(declare-fun sk_?X_31$0 () SetLoc)
+(declare-fun sk_?X_32$0 () SetLoc)
+(declare-fun sk_?X_33$0 () SetLoc)
+(declare-fun tmp_2$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+ (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+ (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y)))
+ :named btwn_reach_8))
+
+(assert (! (forall ((?y Loc))
+ (or (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)
+ (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) ?y)))
+ :named btwn_reach_9))
+
+(assert (! (forall ((?y Loc))
+ (or (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)
+ (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) ?y)))
+ :named btwn_reach_10))
+
+(assert (! (forall ((?y Loc))
+ (or (not (= (read$0 next$0 null$0) null$0))
+ (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+ :named btwn_cycl_8))
+
+(assert (! (forall ((?y Loc))
+ (or (not (= (read$0 next$0 tmp_2$0) tmp_2$0))
+ (not (Btwn$0 next$0 tmp_2$0 ?y ?y)) (= tmp_2$0 ?y)))
+ :named btwn_cycl_9))
+
+(assert (! (forall ((?y Loc))
+ (or (not (= (read$0 next$0 curr_3$0) curr_3$0))
+ (not (Btwn$0 next$0 curr_3$0 ?y ?y)) (= curr_3$0 ?y)))
+ :named btwn_cycl_10))
+
+(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0))
+ :named btwn_step_8))
+
+(assert (! (Btwn$0 next$0 tmp_2$0 (read$0 next$0 tmp_2$0) (read$0 next$0 tmp_2$0))
+ :named btwn_step_9))
+
+(assert (! (Btwn$0 next$0 curr_3$0 (read$0 next$0 curr_3$0) (read$0 next$0 curr_3$0))
+ :named btwn_step_10))
+
+(assert (! (forall ((?f FldLoc))
+ (or (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0)
+ (= null$0 (ep$0 ?f sk_?X_30$0 null$0))))
+ :named entry-point3_10))
+
+(assert (! (forall ((?f FldLoc))
+ (or (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0)
+ (= lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0))))
+ :named entry-point3_11))
+
+(assert (! (forall ((?f FldLoc))
+ (or (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0)
+ (= curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0))))
+ :named entry-point3_12))
+
+(assert (! (forall ((?f FldLoc))
+ (or (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0)
+ (= tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0))))
+ :named entry-point3_13))
+
+(assert (! (forall ((?f FldLoc))
+ (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0)
+ (ep$0 ?f sk_?X_30$0 null$0)))
+ :named entry-point1_10))
+
+(assert (! (forall ((?f FldLoc))
+ (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0)
+ (ep$0 ?f sk_?X_30$0 lst_1$0)))
+ :named entry-point1_11))
+
+(assert (! (forall ((?f FldLoc))
+ (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0)
+ (ep$0 ?f sk_?X_30$0 curr_3$0)))
+ :named entry-point1_12))
+
+(assert (! (forall ((?f FldLoc))
+ (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0)
+ (ep$0 ?f sk_?X_30$0 tmp_2$0)))
+ :named entry-point1_13))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (Btwn$0 ?f null$0 (ep$0 ?f sk_?X_30$0 null$0) ?y)
+ (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+ :named entry-point4_10))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (Btwn$0 ?f lst_1$0 (ep$0 ?f sk_?X_30$0 lst_1$0) ?y)
+ (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+ :named entry-point4_11))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (Btwn$0 ?f curr_3$0 (ep$0 ?f sk_?X_30$0 curr_3$0) ?y)
+ (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+ :named entry-point4_12))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (Btwn$0 ?f tmp_2$0 (ep$0 ?f sk_?X_30$0 tmp_2$0) ?y)
+ (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (in ?y sk_?X_30$0))))
+ :named entry-point4_13))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (not (Btwn$0 ?f null$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+ (in (ep$0 ?f sk_?X_30$0 null$0) sk_?X_30$0)))
+ :named entry-point2_10))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (not (Btwn$0 ?f lst_1$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+ (in (ep$0 ?f sk_?X_30$0 lst_1$0) sk_?X_30$0)))
+ :named entry-point2_11))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (not (Btwn$0 ?f curr_3$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+ (in (ep$0 ?f sk_?X_30$0 curr_3$0) sk_?X_30$0)))
+ :named entry-point2_12))
+
+(assert (! (forall ((?f FldLoc) (?y Loc))
+ (or (not (Btwn$0 ?f tmp_2$0 ?y ?y)) (not (in ?y sk_?X_30$0))
+ (in (ep$0 ?f sk_?X_30$0 tmp_2$0) sk_?X_30$0)))
+ :named entry-point2_13))
+
+(assert (! (= (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)
+ (read$0 next$0 tmp_2$0))
+ :named read_write2))
+
+(assert (! (or (= null$0 curr_3$0)
+ (= (read$0 next$0 null$0)
+ (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) null$0)))
+ :named read_write1))
+
+(assert (! (or (= tmp_2$0 curr_3$0)
+ (= (read$0 next$0 tmp_2$0)
+ (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) tmp_2$0)))
+ :named read_write1_1))
+
+(assert (! (or (= curr_3$0 curr_3$0)
+ (= (read$0 next$0 curr_3$0)
+ (read$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)) curr_3$0)))
+ :named read_write1_2))
+
+(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_5))
+
+(assert (! (= (read$0 next_1$0 null$0) null$0) :named read_null_6))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 lst$0 l1 curr_2$0)
+ (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0))
+ (not (= l1 curr_2$0)))
+ (and
+ (or (= l1 curr_2$0)
+ (not (Btwn$0 next$0 lst$0 l1 curr_2$0)))
+ (not (in l1 (lseg_domain$0 next$0 lst$0 curr_2$0))))))
+ :named lseg_footprint_20))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 curr_3$0 l1 null$0)
+ (in l1 (lseg_domain$0 next$0 curr_3$0 null$0))
+ (not (= l1 null$0)))
+ (and
+ (or (= l1 null$0)
+ (not (Btwn$0 next$0 curr_3$0 l1 null$0)))
+ (not (in l1 (lseg_domain$0 next$0 curr_3$0 null$0))))))
+ :named lseg_footprint_21))
+
+(assert (! (not (in tmp_2$0 FP_2$0)) :named check_free_31_6))
+
+(assert (! (not (in null$0 Alloc$0)) :named framecondition_of_remove_loop_18_4_15))
+
+(assert (! (not (= lst$0 null$0)) :named if_else_13_6_4))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+ :named precondition_of_remove_10_11_20))
+
+(assert (! (= sk_?X_33$0 FP$0) :named precondition_of_remove_10_11_21))
+
+(assert (! (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0) :named invariant_18_4_62))
+
+(assert (! (= FP$0 (union FP_1$0 FP$0)) :named invariant_18_4_63))
+
+(assert (! (= sk_?X_31$0 (lseg_domain$0 next$0 curr_2$0 null$0))
+ :named invariant_18_4_64))
+
+(assert (! (= sk_?X_30$0 (union sk_?X_31$0 sk_?X_32$0)) :named invariant_18_4_65))
+
+(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_66))
+
+(assert (! (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)
+ :named invariant_18_4_67))
+
+(assert (! (= sk_?X_29$0 (union sk_?X_28$0 sk_?X_27$0)) :named invariant_18_4_68))
+
+(assert (! (= sk_?X_28$0 (lseg_domain$0 next$0 curr_3$0 null$0))
+ :named invariant_18_4_69))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_27$0 sk_?X_28$0))
+ :named invariant_18_4_70))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+ :named initial_footprint_of_remove_10_11_10))
+
+(assert (! (Frame$0 FP_1$0 Alloc$0 next$0 next$0)
+ :named framecondition_of_remove_loop_18_4_16))
+
+(assert (! (= next_1$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0)))
+ :named assign_30_6))
+
+(assert (! (= curr_2$0 lst$0) :named assign_17_4_4))
+
+(assert (! (= FP_2$0
+ (union (setminus FP$0 FP_1$0)
+ (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0))))
+ :named framecondition_of_remove_loop_18_4_17))
+
+(assert (! (or (Btwn$0 next$0 lst$0 curr_2$0 curr_2$0)
+ (not (lseg_struct$0 sk_?X_32$0 next$0 lst$0 curr_2$0)))
+ :named unnamed_23))
+
+(assert (! (or (Btwn$0 next$0 curr_3$0 null$0 null$0)
+ (not (lseg_struct$0 sk_?X_28$0 next$0 curr_3$0 null$0)))
+ :named unnamed_24))
+
+(assert (! (or (= (read$0 next$0 curr_3$0) null$0) (not nondet_2$0))
+ :named unnamed_25))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 lst_1$0 l1 curr_3$0)
+ (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
+ (not (= l1 curr_3$0)))
+ (and
+ (or (= l1 curr_3$0)
+ (not (Btwn$0 next$0 lst_1$0 l1 curr_3$0)))
+ (not (in l1 (lseg_domain$0 next$0 lst_1$0 curr_3$0))))))
+ :named lseg_footprint_22))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 lst$0 l1 null$0)
+ (in l1 (lseg_domain$0 next$0 lst$0 null$0))
+ (not (= l1 null$0)))
+ (and (or (= l1 null$0) (not (Btwn$0 next$0 lst$0 l1 null$0)))
+ (not (in l1 (lseg_domain$0 next$0 lst$0 null$0))))))
+ :named lseg_footprint_23))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 curr_2$0 l1 null$0)
+ (in l1 (lseg_domain$0 next$0 curr_2$0 null$0))
+ (not (= l1 null$0)))
+ (and
+ (or (= l1 null$0)
+ (not (Btwn$0 next$0 curr_2$0 l1 null$0)))
+ (not (in l1 (lseg_domain$0 next$0 curr_2$0 null$0))))))
+ :named lseg_footprint_24))
+
+(assert (! (not (in null$0 Alloc$0)) :named initial_footprint_of_remove_10_11_11))
+
+(assert (! (not (= tmp_2$0 null$0)) :named if_else_28_8_2))
+
+(assert (! (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)
+ :named precondition_of_remove_10_11_22))
+
+(assert (! (= sk_?X_33$0 (lseg_domain$0 next$0 lst$0 null$0))
+ :named precondition_of_remove_10_11_23))
+
+(assert (! (not (= curr_2$0 null$0)) :named invariant_18_4_71))
+
+(assert (! (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)
+ :named invariant_18_4_72))
+
+(assert (! (= sk_?X_32$0 (lseg_domain$0 next$0 lst$0 curr_2$0))
+ :named invariant_18_4_73))
+
+(assert (! (= sk_?X_30$0 FP_1$0) :named invariant_18_4_74))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_32$0 sk_?X_31$0))
+ :named invariant_18_4_75))
+
+(assert (! (not (= curr_3$0 null$0)) :named invariant_18_4_76))
+
+(assert (! (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)
+ :named invariant_18_4_77))
+
+(assert (! (= sk_?X_29$0
+ (union (intersection Alloc$0 FP_1$0) (setminus Alloc$0 Alloc$0)))
+ :named invariant_18_4_78))
+
+(assert (! (= sk_?X_27$0 (lseg_domain$0 next$0 lst_1$0 curr_3$0))
+ :named invariant_18_4_79))
+
+(assert (! (= (as emptyset SetLoc) (as emptyset SetLoc)) :named invariant_18_4_80))
+
+(assert (! (= Alloc$0 (union FP_2$0 Alloc$0))
+ :named framecondition_of_remove_loop_18_4_18))
+
+(assert (! (= tmp_2$0 (read$0 next$0 curr_3$0)) :named assign_27_4_2))
+
+(assert (! (= lst_1$0 lst$0) :named framecondition_of_remove_loop_18_4_19))
+
+(assert (! (= FP_Caller_1$0 (setminus FP_Caller$0 FP$0)) :named assign_13_2_5))
+
+(assert (! (or (Btwn$0 next$0 lst_1$0 curr_3$0 curr_3$0)
+ (not (lseg_struct$0 sk_?X_27$0 next$0 lst_1$0 curr_3$0)))
+ :named unnamed_26))
+
+(assert (! (or (Btwn$0 next$0 lst$0 null$0 null$0)
+ (not (lseg_struct$0 sk_?X_33$0 next$0 lst$0 null$0)))
+ :named unnamed_27))
+
+(assert (! (or (Btwn$0 next$0 curr_2$0 null$0 null$0)
+ (not (lseg_struct$0 sk_?X_31$0 next$0 curr_2$0 null$0)))
+ :named unnamed_28))
+
+(assert (! (forall ((?u Loc) (?v Loc) (?z Loc))
+ (and
+ (or
+ (Btwn$0 (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
+ ?z ?u ?v)
+ (not
+ (or
+ (and (Btwn$0 next$0 ?z ?u ?v)
+ (or (Btwn$0 next$0 ?z ?v curr_3$0)
+ (and (Btwn$0 next$0 ?z ?v ?v)
+ (not
+ (Btwn$0 next$0 ?z curr_3$0
+ curr_3$0)))))
+ (and (not (= curr_3$0 ?v))
+ (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+ (and
+ (Btwn$0 next$0 ?z curr_3$0
+ curr_3$0)
+ (not (Btwn$0 next$0 ?z ?v ?v))))
+ (Btwn$0 next$0 ?z ?u curr_3$0)
+ (or
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+ ?v curr_3$0)
+ (and
+ (Btwn$0 next$0
+ (read$0 next$0 tmp_2$0) ?v ?v)
+ (not
+ (Btwn$0 next$0
+ (read$0 next$0 tmp_2$0)
+ curr_3$0 curr_3$0)))))
+ (and (not (= curr_3$0 ?v))
+ (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+ (and
+ (Btwn$0 next$0 ?z curr_3$0
+ curr_3$0)
+ (not (Btwn$0 next$0 ?z ?v ?v))))
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u
+ ?v)
+ (or
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+ ?v curr_3$0)
+ (and
+ (Btwn$0 next$0
+ (read$0 next$0 tmp_2$0) ?v ?v)
+ (not
+ (Btwn$0 next$0
+ (read$0 next$0 tmp_2$0)
+ curr_3$0 curr_3$0))))))))
+ (or
+ (and (Btwn$0 next$0 ?z ?u ?v)
+ (or (Btwn$0 next$0 ?z ?v curr_3$0)
+ (and (Btwn$0 next$0 ?z ?v ?v)
+ (not (Btwn$0 next$0 ?z curr_3$0 curr_3$0)))))
+ (and (not (= curr_3$0 ?v))
+ (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+ (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
+ (not (Btwn$0 next$0 ?z ?v ?v))))
+ (Btwn$0 next$0 ?z ?u curr_3$0)
+ (or
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+ curr_3$0)
+ (and
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+ ?v)
+ (not
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+ curr_3$0 curr_3$0)))))
+ (and (not (= curr_3$0 ?v))
+ (or (Btwn$0 next$0 ?z curr_3$0 ?v)
+ (and (Btwn$0 next$0 ?z curr_3$0 curr_3$0)
+ (not (Btwn$0 next$0 ?z ?v ?v))))
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?u ?v)
+ (or
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+ curr_3$0)
+ (and
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0) ?v
+ ?v)
+ (not
+ (Btwn$0 next$0 (read$0 next$0 tmp_2$0)
+ curr_3$0 curr_3$0)))))
+ (not
+ (Btwn$0
+ (write$0 next$0 curr_3$0 (read$0 next$0 tmp_2$0))
+ ?z ?u ?v)))))
+ :named btwn_write))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_5))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+ :named btwn_sndw_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+ (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+ :named btwn_ord1_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z))
+ (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+ :named btwn_ord2_5))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+ (Btwn$0 next$0 ?x ?z ?z)))
+ :named btwn_trn1_5))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+ (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+ :named btwn_trn2_5))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+ (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+ :named btwn_trn3_5))
+
+(check-sat)
+(exit)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+
+(assert (not (= S T)))
+(assert (= T (union smt_set_emp S)))
+(check-sat)
+
+; What was the bug?
+;
+; When two sets were disequal, the corresponding lemma
+; was not being generated (stating there in an element
+; in one, but not in the other).
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v54 () Int)
+(declare-fun z3f55 (Int) Int)
+(declare-fun z3v56 () Int)
+(declare-fun z3v57 () Int)
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(declare-fun z3f60 (Int) mySet)
+(declare-fun z3f61 (Int) Bool)
+(declare-fun z3f62 (Int Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3f65 (Int) mySet)
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(declare-fun z3v68 () Int)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v71 () Int)
+(declare-fun z3v72 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(assert (= (z3f60 z3v94) (z3f65 z3v56)))
+(assert (and (>= (z3f55 z3v56) 0) (>= (z3f55 z3v58) 0) (= (z3f60 z3v58) smt_set_emp) (= (z3f55 z3v58) 0) (= (z3f61 z3v58) true) (= z3v58 z3f90) (>= (z3f55 z3v58) 0) (= z3v58 z3v63) (>= (z3f55 z3v58) 0) (>= (z3f55 z3v64) 0) (= (z3f65 z3v64) (smt_set_cup (z3f60 z3v63) (z3f65 z3v56))) (= (z3f60 z3v64) (smt_set_cup (smt_set_add smt_set_emp z3v63) (z3f60 z3v56))) (= (z3f55 z3v64) (+ 1 (z3f55 z3v56))) (= (z3f61 z3v64) false) (= z3v64 (z3f62 z3v63 z3v56)) (>= (z3f55 z3v64) 0) (= z3v64 z3v66) (>= (z3f55 z3v64) 0) (>= (z3f55 z3v63) 0) (>= (z3f55 z3v66) 0) (= (z3f70 z3v69) z3v69) (= (z3f70 z3v71) z3v71) (= (z3f70 z3v72) z3v72)))
+(assert (not (= (z3f60 z3v94) (z3f65 z3v66))))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+
+; What was the bug?
+;
+; When asserting equality to equality engine, correct reason
+; was not being sent (the fact itself was being sent as reason)
+
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v56 () Int)
+(declare-fun z3v57 () Int)
+(assert (distinct z3v56 z3v57))
+(declare-fun z3v58 () Int)
+(declare-fun z3f59 (Int) Int)
+(declare-fun z3v60 () Int)
+(declare-fun z3f61 (Int) Bool)
+(declare-fun z3v62 () Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3f66 (Int) mySet)
+(declare-fun z3f67 (Int) Bool)
+(declare-fun z3f68 (Int Int) Int)
+(declare-fun z3v69 () Int)
+(declare-fun z3v70 () Int)
+(declare-fun z3f71 (Int) Int)
+(declare-fun z3v72 () Int)
+(declare-fun z3v73 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v75 () Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3f82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v84 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(assert (= z3v90 z3v56))
+(assert (z3f61 z3v90))
+(assert (and (>= (z3f59 z3v58) 0) (z3f61 z3v60) (z3f61 z3v60) (= z3v60 z3v62) (= (z3f61 z3v60) (= z3v64 z3v63)) (= (z3f61 z3v62) (= z3v64 z3v63)) (>= (z3f59 z3v65) 0) (= (z3f66 z3v65) (smt_set_cup (smt_set_add smt_set_emp z3v64) (z3f66 z3v58))) (= (z3f59 z3v65) (+ 1 (z3f59 z3v58))) (= (z3f67 z3v65) false) (= z3v65 (z3f68 z3v64 z3v58)) (>= (z3f59 z3v65) 0) (= z3v65 z3v69) (>= (z3f59 z3v65) 0) (>= (z3f59 z3v69) 0) (z3f61 z3v56) (= (z3f71 z3v70) z3v70) (= (z3f71 z3v72) z3v72) (not (z3f61 z3v57)) (= (z3f71 z3v73) z3v73)))
+(assert (not (= (z3f61 z3v90) (smt_set_mem z3v63 (z3f66 z3v69)))))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v58 () Int)
+(declare-fun z3v59 () Int)
+(assert (distinct z3v58 z3v59))
+(declare-fun z3f60 (Int) Bool)
+(declare-fun z3v61 () Int)
+(declare-fun z3f62 (Int) Int)
+(declare-fun z3v63 () Int)
+(declare-fun z3v64 () Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3f67 (Int) mySet)
+(declare-fun z3v69 () Int)
+(declare-fun z3f70 (Int) Int)
+(declare-fun z3v76 () Int)
+(declare-fun z3v77 () Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v81 () Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3f83 (Int) Int)
+(declare-fun z3f84 (Int) Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3f86 (Int) Int)
+(declare-fun z3f87 (Int Int) Int)
+(declare-fun z3v88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3f90 (Int) mySet)
+(declare-fun z3f91 (Int) Bool)
+(declare-fun z3f92 (Int Int) Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3v94 () Int)
+(declare-fun z3v95 () Int)
+(declare-fun z3v96 () Int)
+(declare-fun z3v97 () Int)
+(assert (and (not (z3f60 z3v79)) (not (z3f60 z3v79)) (= z3v79 z3v80) (= (z3f60 z3v79) (= z3v76 z3v81)) (= (z3f60 z3v80) (= z3v76 z3v81)) (= (z3f83 z3v82) z3v81) (= (z3f84 z3v82) z3v81) (= (z3f86 z3v82) z3v85) (= z3v82 (z3f87 z3v81 z3v85)) (= z3v82 z3v88) (>= (z3f70 z3v78) 0) (= (z3f67 z3v78) (smt_set_cup (smt_set_add smt_set_emp (z3f83 z3v88)) (z3f67 z3v89))) (= (z3f90 z3v78) (smt_set_cup (smt_set_add smt_set_emp z3v88) (z3f90 z3v89))) (= (z3f70 z3v78) (+ 1 (z3f70 z3v89))) (= (z3f91 z3v78) false) (= z3v78 (z3f92 z3v88 z3v89)) (>= (z3f70 z3v78) 0) (= z3v78 z3v77) (>= (z3f70 z3v78) 0) (>= (z3f70 z3v89) 0) (>= (z3f70 z3v77) 0) (>= (z3f70 z3v97) 0) (= z3v97 z3v89) (>= (z3f70 z3v97) 0) (z3f60 z3v58) (= (z3f62 z3v61) z3v61) (= (z3f62 z3v63) z3v63) (not (z3f60 z3v59)) (= (z3f62 z3v64) z3v64)))
+(assert (smt_set_mem z3v76 (z3f67 z3v78)))
+(assert (<= z3v95 z3v93))
+(assert (>= z3v95 z3v93))
+(assert (= z3v95 z3v93))
+(assert (smt_set_mem z3v76 (z3f67 z3v77)))
+(declare-fun z3v98 () Int)
+(assert (not (< z3v98 z3v85)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+
+; Observed behavior
+;
+; Benchmark taking too long. Lemmas being generated indefinitely with
+; skolems due to the "two sets not being equal" axiom.
+;
+; What was the bug?
+;
+;
+
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt))
+
+(declare-fun f (Int) mySet)
+(declare-fun x () Int)
+(declare-fun y () Int)
+
+(declare-fun S () mySet)
+(declare-fun T () mySet)
+
+(assert (= (f x)
+ (union S T)))
+
+(assert (= (f x)
+ (union T (f y))))
+
+(assert (not (= (f y)
+ (union T (f y)))))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v60 () Int)
+(declare-fun z3v61 () Int)
+(assert (distinct z3v60 z3v61))
+(declare-fun z3f62 (Int) Bool)
+(declare-fun z3v63 () Int)
+(declare-fun z3f64 (Int) Int)
+(declare-fun z3v65 () Int)
+(declare-fun z3v66 () Int)
+(declare-fun z3v69 () mySet)
+(declare-fun z3v70 () mySet)
+(declare-fun z3v72 () mySet)
+(declare-fun z3v73 () mySet)
+(declare-fun z3v75 () Int)
+(declare-fun z3f76 (Int) Int)
+(declare-fun z3v79 () Int)
+(declare-fun z3v80 () Int)
+(declare-fun z3v84 () Int)
+(declare-fun z3v87 () mySet)
+(declare-fun z3v88 () mySet)
+(declare-fun z3v90 () mySet)
+(declare-fun z3v91 () mySet)
+(declare-fun z3v93 () mySet)
+(declare-fun z3v94 () mySet)
+(declare-fun z3v96 () Int)
+(declare-fun z3f97 (Int) mySet)
+(declare-fun z3f98 (Int) Bool)
+(declare-fun z3v99 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v105 () mySet)
+(declare-fun z3v107 () mySet)
+(declare-fun z3v108 () mySet)
+(declare-fun z3v109 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v111 () Int)
+(declare-fun z3v112 () Int)
+(declare-fun z3v113 () mySet)
+(declare-fun z3v114 () mySet)
+(declare-fun z3v117 () mySet)
+(declare-fun z3v118 () mySet)
+(declare-fun z3v121 () mySet)
+(declare-fun z3v123 () mySet)
+(declare-fun z3v124 () mySet)
+(declare-fun z3v126 () mySet)
+(declare-fun z3v128 () Int)
+(declare-fun z3v132 () Int)
+(declare-fun z3v135 () mySet)
+(declare-fun z3v136 () mySet)
+(declare-fun z3v138 () mySet)
+(declare-fun z3v140 () Int)
+(declare-fun z3v143 () mySet)
+(declare-fun z3v144 () mySet)
+(declare-fun z3v145 () mySet)
+(declare-fun z3v146 () Int)
+(declare-fun z3v147 () Int)
+(declare-fun z3v148 () mySet)
+(declare-fun z3v149 () mySet)
+(declare-fun z3v155 () mySet)
+(declare-fun z3v156 () mySet)
+(declare-fun z3v157 () mySet)
+(declare-fun z3v160 () Int)
+(declare-fun z3v161 () Int)
+(declare-fun z3v162 () Int)
+(declare-fun z3v163 () Int)
+(declare-fun z3v164 () mySet)
+(declare-fun z3v165 () mySet)
+(declare-fun z3v169 () Int)
+(declare-fun z3v172 () mySet)
+(declare-fun z3v173 () mySet)
+(declare-fun z3v175 () Int)
+(declare-fun z3v176 () Int)
+(declare-fun z3v177 () Int)
+(declare-fun z3v178 () Int)
+(declare-fun z3f179 (Int Int) Int)
+(declare-fun z3v180 () Int)
+(declare-fun z3v181 () Int)
+(declare-fun z3f183 () Int)
+(declare-fun z3v184 () Int)
+(declare-fun z3v185 () Int)
+(declare-fun z3v186 () Int)
+(declare-fun z3v187 () Int)
+(declare-fun z3v188 () Int)
+(declare-fun z3v189 () Int)
+(declare-fun z3v192 () Int)
+(declare-fun z3v193 () Int)
+(declare-fun z3v197 () Int)
+(declare-fun z3v198 () mySet)
+(declare-fun z3v200 () Int)
+(declare-fun z3v201 () Int)
+(declare-fun z3v202 () Int)
+(declare-fun z3v203 () Int)
+(declare-fun z3v204 () Int)
+(declare-fun z3v206 () Int)
+(declare-fun z3v207 () Int)
+(declare-fun z3v208 () Int)
+(declare-fun z3v209 () Int)
+(declare-fun z3v210 () Int)
+(declare-fun z3v211 () Int)
+(declare-fun z3f212 (Int) Int)
+(declare-fun z3f213 (Int) Int)
+(declare-fun z3v214 () Int)
+(declare-fun z3v215 () Int)
+(declare-fun z3v217 () Int)
+(declare-fun z3v218 () Int)
+(declare-fun z3v219 () Int)
+(declare-fun z3v220 () Int)
+(declare-fun z3f221 (Int Int) Int)
+(declare-fun z3v222 () Int)
+(declare-fun z3v223 () Int)
+(declare-fun z3v224 () Int)
+(declare-fun z3v225 () Int)
+(declare-fun z3v226 () Int)
+(declare-fun z3v227 () Int)
+(declare-fun z3v228 () Int)
+(declare-fun z3v229 () Int)
+(declare-fun z3v230 () Int)
+(declare-fun z3v231 () Int)
+(declare-fun z3v232 () Int)
+(declare-fun z3v233 () Int)
+(declare-fun z3v234 () Int)
+(declare-fun z3v235 () Int)
+(declare-fun z3v236 () Int)
+(declare-fun z3v237 () Int)
+(declare-fun z3v238 () Int)
+(declare-fun z3v239 () Int)
+(declare-fun z3v240 () Int)
+(declare-fun z3v241 () Int)
+(declare-fun z3v242 () Int)
+(declare-fun z3v243 () Int)
+(declare-fun z3v244 () Int)
+(declare-fun z3v245 () Int)
+(declare-fun z3v246 () Int)
+(declare-fun z3v247 () Int)
+(declare-fun z3v248 () Int)
+(declare-fun z3v249 () Int)
+(declare-fun z3v250 () Int)
+(declare-fun z3v251 () Int)
+(declare-fun z3v252 () Int)
+(declare-fun z3v253 () Int)
+(declare-fun z3v254 () Int)
+(declare-fun z3v255 () Int)
+(declare-fun z3v256 () Int)
+(declare-fun z3v257 () Int)
+(declare-fun z3v258 () Int)
+(declare-fun z3v259 () Int)
+(declare-fun z3v260 () Int)
+(declare-fun z3v261 () Int)
+(declare-fun z3v262 () Int)
+(declare-fun z3v263 () Int)
+(declare-fun z3v264 () Int)
+(declare-fun z3v265 () Int)
+(declare-fun z3v266 () Int)
+(declare-fun z3v267 () Int)
+(declare-fun z3v268 () Int)
+(declare-fun z3v269 () Int)
+(declare-fun z3v271 () Int)
+(declare-fun z3v273 () Int)
+(declare-fun z3v275 () Int)
+(declare-fun z3v277 () Int)
+(declare-fun z3v279 () Int)
+(declare-fun z3v281 () Int)
+(declare-fun z3v283 () Int)
+(declare-fun z3v286 () Int)
+(declare-fun z3v289 () Int)
+(declare-fun z3v290 () Int)
+(declare-fun z3v291 () Int)
+(declare-fun z3v292 () mySet)
+(declare-fun z3v295 () mySet)
+(declare-fun z3v297 () Int)
+(declare-fun z3v301 () Int)
+(declare-fun z3v302 () Int)
+(declare-fun z3v303 () Int)
+(declare-fun z3v304 () Int)
+(declare-fun z3v305 () Int)
+(declare-fun z3v306 () Int)
+(declare-fun z3v307 () Int)
+(declare-fun z3v308 () Int)
+(declare-fun z3v309 () Int)
+(declare-fun z3v310 () Int)
+(declare-fun z3v312 () Int)
+(declare-fun z3v314 () Int)
+(declare-fun z3v315 () Int)
+(declare-fun z3v316 () Int)
+(declare-fun z3v317 () Int)
+(declare-fun z3v318 () Int)
+(declare-fun z3v319 () Int)
+(declare-fun z3v320 () Int)
+(declare-fun z3v321 () Int)
+(declare-fun z3v322 () Int)
+(declare-fun z3v324 () Int)
+(declare-fun z3v327 () Int)
+(declare-fun z3v328 () Int)
+(declare-fun z3v329 () Int)
+(declare-fun z3v330 () Int)
+(declare-fun z3v331 () Int)
+(declare-fun z3v332 () Int)
+(declare-fun z3v333 () Int)
+(declare-fun z3v334 () Int)
+(declare-fun z3v335 () Int)
+(declare-fun z3v336 () Int)
+(declare-fun z3v337 () Int)
+(declare-fun z3v338 () Int)
+(declare-fun z3v339 () Int)
+(declare-fun z3v340 () Int)
+(declare-fun z3v341 () Int)
+(declare-fun z3v342 () Int)
+(declare-fun z3v343 () Int)
+(declare-fun z3v345 () Int)
+(declare-fun z3v349 () Int)
+(declare-fun z3v350 () Int)
+(declare-fun z3v351 () Int)
+(declare-fun z3v352 () Int)
+(declare-fun z3v353 () Int)
+(declare-fun z3v354 () Int)
+(declare-fun z3v355 () Int)
+(declare-fun z3v359 () Int)
+(declare-fun z3v361 () Int)
+(declare-fun z3v362 () Int)
+(declare-fun z3v363 () Int)
+(declare-fun z3v364 () Int)
+(declare-fun z3v366 () Int)
+(declare-fun z3v367 () Int)
+(declare-fun z3v368 () Int)
+(declare-fun z3v369 () Int)
+(declare-fun z3v370 () Int)
+(declare-fun z3v375 () Int)
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375))))
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375))))
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375))))
+(assert (= (z3f97 z3v328) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v331) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v330) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v328) (z3f97 z3v375))))
+(assert (= (z3f97 z3v331) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375))))
+(assert (= (z3f97 z3v375) (z3f97 z3v331)))
+(assert (= (z3f97 z3v375) (z3f97 z3v328)))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v327) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v330))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v328) (z3f97 z3v327))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v330) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v331))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v330))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v328))))
+(assert (= (z3f97 z3v375) (smt_set_cup (z3f97 z3v331) (z3f97 z3v327))))
+(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v331)))
+(assert (smt_set_sub (z3f97 z3v375) (z3f97 z3v328)))
+(assert (<= z3v375 z3v331))
+(assert (<= z3v375 z3v328))
+(assert (= z3v375 z3v328))
+(assert (>= z3v375 z3v331))
+(assert (>= z3v375 z3v328))
+(assert (not (= z3v375 z3v330)))
+(assert (not (= z3v375 z3v327)))
+(assert (<= (z3f76 z3v375) (z3f76 z3v331)))
+(assert (<= (z3f76 z3v375) (z3f76 z3v328)))
+(assert (> (z3f76 z3v375) (z3f76 z3v330)))
+(assert (> (z3f76 z3v375) (z3f76 z3v327)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v331)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v330)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v328)))
+(assert (>= (z3f76 z3v375) (z3f76 z3v327)))
+(assert (= (z3f76 z3v375) (z3f76 z3v331)))
+(assert (= (z3f76 z3v375) (z3f76 z3v328)))
+(assert (> (z3f76 z3v375) 0))
+(assert (= z3v375 z3v331))
+(assert (>= (z3f76 z3v375) 0))
+(assert (and (>= (z3f76 z3v327) 0) (>= (z3f76 z3v328) 0) (= (z3f97 z3v328) (smt_set_cup (smt_set_add smt_set_emp z3v329) (z3f97 z3v330))) (= (z3f76 z3v328) (+ 1 (z3f76 z3v330))) (= (z3f98 z3v328) false) (= z3v328 (z3f179 z3v329 z3v330)) (>= (z3f76 z3v328) 0) (= z3v328 z3v331) (>= (z3f76 z3v328) 0) (>= (z3f76 z3v330) 0) (>= (z3f76 z3v331) 0) (z3f62 z3v60) (= (z3f64 z3v63) z3v63) (= (z3f64 z3v65) z3v65) (not (z3f62 z3v61)) (= (z3f64 z3v66) z3v66)))
+(assert (not (= (z3f97 z3v327) (smt_set_cup (z3f97 z3v327) (z3f97 z3v375)))))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(assert (distinct z3v66 z3v67))
+(declare-fun z3v68 () Int)
+(declare-fun z3f69 (Int) Int)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3v71 () Int)
+(declare-fun z3f72 (Int) mySet)
+(declare-fun z3v73 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v75 () Int)
+(declare-fun z3f76 (Int) Bool)
+(declare-fun z3f77 (Int Int) Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3f79 (Int) Bool)
+(declare-fun z3v80 () Int)
+(declare-fun z3f81 (Int) Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3f94 (Int) Int)
+(declare-fun z3f95 (Int) Int)
+(declare-fun z3f96 (Int Int Int) Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(assert (= z3v99 z3v98))
+(assert (and (>= (z3f69 z3v85) 0)
+ (not (smt_set_mem z3v86 (z3f70 z3v85)))
+ (= (z3f72 z3v85) smt_set_emp)
+ (>= (z3f69 z3v87) 0)
+ (= (z3f72 z3v87) smt_set_emp)
+ (= (z3f70 z3v87) smt_set_emp)
+ (= (z3f69 z3v87) 0)
+ (= (z3f76 z3v87) true)
+ (= z3v87 z3f88)
+ (>= (z3f69 z3v87) 0)
+ (= z3v87 z3v89)
+ (>= (z3f69 z3v87) 0)
+ (= (z3f70 z3v87)
+ (z3f70 z3v90))
+ (= (z3f72 z3v87) smt_set_emp)
+ (>= (z3f69 z3v89) 0)
+ (= (z3f70 z3v89)
+ (z3f70 z3v90))
+ (= (z3f72 z3v89) smt_set_emp)
+ (>= (z3f69 z3v90) 0)
+ (= (z3f72 z3v90)
+ (ite (smt_set_mem z3v86 (z3f70 z3v85))
+ (smt_set_cup (smt_set_add smt_set_emp z3v86)
+ (z3f72 z3v85))
+ (z3f72 z3v85)))
+ (= (z3f70 z3v90)
+ (smt_set_cup (smt_set_add smt_set_emp z3v86)
+ (z3f70 z3v85)))
+ (= (z3f69 z3v90)
+ (+ 1 (z3f69 z3v85)))
+ (= (z3f76 z3v90) false)
+ (>= (z3f69 z3v91) 0)
+ (= (z3f72 z3v91) smt_set_emp)
+ (= (z3f70 z3v91) smt_set_emp)
+ (= (z3f69 z3v91) 0)
+ (= (z3f76 z3v91) true)
+ (= z3v91 z3f88)
+ (>= (z3f69 z3v91) 0)
+ (= z3v91 z3v92)
+ (>= (z3f69 z3v91) 0)
+ (not (smt_set_mem z3v86 (z3f70 z3v91)))
+ (= (z3f72 z3v91) smt_set_emp)
+ (= (z3f94 z3v93) z3v92)
+ (= (z3f95 z3v93) z3v85)
+ (= z3v93 (z3f96 z3v86 z3v92 z3v85))
+ (= z3v93 z3v97)
+ (= (smt_set_cap (z3f70 (z3f94 z3v93))
+ (z3f70 (z3f95 z3v93))) smt_set_emp)
+ (>= (z3f69 z3v92) 0)
+ (not (smt_set_mem z3v86 (z3f70 z3v92)))
+ (= (z3f72 z3v92) smt_set_emp)
+ (= (smt_set_cap (z3f70 (z3f94 z3v97))
+ (z3f70 (z3f95 z3v97))) smt_set_emp)
+ (z3f79 z3v66)
+ (= (z3f81 z3v80) z3v80)
+ (= (z3f81 z3v82) z3v82)
+ (not (z3f79 z3v67))
+ (= (z3f81 z3v83) z3v83)))
+(assert (not (> z3v99 z3v98)))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet () (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+(define-fun smt_set_mem ((x Elt) (s mySet)) Bool (in x s))
+(define-fun smt_set_add ((s mySet) (x Elt)) mySet (union s (setenum x)))
+(define-fun smt_set_cup ((s1 mySet) (s2 mySet)) mySet (union s1 s2))
+(define-fun smt_set_cap ((s1 mySet) (s2 mySet)) mySet (intersection s1 s2))
+;(define-fun smt_set_com ((s mySet)) mySet ((_ map not) s))
+(define-fun smt_set_dif ((s1 mySet) (s2 mySet)) mySet (setminus s1 s2))
+;(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (= smt_set_emp (smt_set_dif s1 s2)))
+(define-fun smt_set_sub ((s1 mySet) (s2 mySet)) Bool (subseteq s1 s2))
+(declare-fun z3v66 () Int)
+(declare-fun z3v67 () Int)
+(assert (distinct z3v66 z3v67))
+(declare-fun z3v68 () Int)
+(declare-fun z3f69 (Int) Int)
+(declare-fun z3f70 (Int) mySet)
+(declare-fun z3v71 () Int)
+(declare-fun z3f72 (Int) mySet)
+(declare-fun z3v73 () Int)
+(declare-fun z3v74 () Int)
+(declare-fun z3v75 () Int)
+(declare-fun z3f76 (Int) Bool)
+(declare-fun z3f77 (Int Int) Int)
+(declare-fun z3v78 () Int)
+(declare-fun z3f79 (Int) Bool)
+(declare-fun z3v80 () Int)
+(declare-fun z3f81 (Int) Int)
+(declare-fun z3v82 () Int)
+(declare-fun z3v83 () Int)
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3f88 () Int)
+(declare-fun z3v89 () Int)
+(declare-fun z3v90 () Int)
+(declare-fun z3v91 () Int)
+(declare-fun z3v92 () Int)
+(declare-fun z3v93 () Int)
+(declare-fun z3f94 (Int) Int)
+(declare-fun z3f95 (Int) Int)
+(declare-fun z3f96 (Int Int Int) Int)
+(declare-fun z3v97 () Int)
+(declare-fun z3v98 () Int)
+(declare-fun z3v99 () Int)
+(declare-fun z3v100 () Int)
+(declare-fun z3v101 () Int)
+(declare-fun z3v102 () Int)
+(declare-fun z3v103 () Int)
+(declare-fun z3v104 () Int)
+(declare-fun z3v105 () Int)
+(declare-fun z3v106 () Int)
+(declare-fun z3v107 () Int)
+(declare-fun z3v108 () Int)
+(declare-fun z3v109 () Int)
+(declare-fun z3v110 () Int)
+(declare-fun z3v113 () Int)
+(declare-fun z3v114 () Int)
+(declare-fun z3v115 () Int)
+(declare-fun z3v116 () Int)
+(declare-fun z3v117 () Int)
+(declare-fun z3v118 () Int)
+(declare-fun z3v120 () Int)
+(declare-fun z3v121 () Int)
+(declare-fun z3v122 () Int)
+(declare-fun z3v124 () Int)
+(declare-fun z3v125 () Int)
+(declare-fun z3v126 () Int)
+(declare-fun z3v127 () Int)
+(declare-fun z3v128 () Int)
+(declare-fun z3v129 () Int)
+(declare-fun z3v131 () Int)
+(declare-fun z3v132 () Int)
+(declare-fun z3v133 () Int)
+(declare-fun z3v134 () Int)
+(declare-fun z3v135 () Int)
+(declare-fun z3v136 () Int)
+(declare-fun z3v137 () Int)
+(declare-fun z3v138 () Int)
+(declare-fun z3v139 () Int)
+(declare-fun z3v140 () Int)
+(declare-fun z3v141 () Int)
+(declare-fun z3v142 () Int)
+(declare-fun z3v144 () Int)
+(declare-fun z3v145 () Int)
+(declare-fun z3v146 () Int)
+(declare-fun z3v149 () Int)
+(declare-fun z3v151 () Int)
+(declare-fun z3v154 () Int)
+(declare-fun z3v155 () Int)
+(declare-fun z3v156 () Int)
+(declare-fun z3v157 () Int)
+(declare-fun z3v158 () Int)
+(declare-fun z3v159 () Int)
+(declare-fun z3v161 () Int)
+(declare-fun z3v163 () Int)
+(declare-fun z3v164 () Int)
+(declare-fun z3v165 () Int)
+(declare-fun z3v167 () Int)
+(declare-fun z3v170 () Int)
+(declare-fun z3v174 () Int)
+(declare-fun z3v175 () Int)
+(declare-fun z3v176 () Int)
+(declare-fun z3v179 () Int)
+(declare-fun z3v181 () Int)
+(declare-fun z3v182 () Int)
+(declare-fun z3v183 () Int)
+(declare-fun z3v184 () Int)
+(declare-fun z3v187 () Int)
+(declare-fun z3v188 () Int)
+(declare-fun z3v189 () Int)
+(declare-fun z3v190 () Int)
+(declare-fun z3f191 (Int) Int)
+(declare-fun z3f192 (Int) Int)
+(declare-fun z3v195 () Int)
+(declare-fun z3v196 () Int)
+(declare-fun z3v199 () Int)
+(declare-fun z3v200 () Int)
+(declare-fun z3v201 () Int)
+(declare-fun z3v202 () Int)
+(declare-fun z3v203 () Int)
+(declare-fun z3v206 () Int)
+(declare-fun z3v207 () Int)
+(declare-fun z3v208 () Int)
+(declare-fun z3v210 () Int)
+(declare-fun z3v211 () Int)
+(declare-fun z3v212 () Int)
+(declare-fun z3f213 (Int) Bool)
+(declare-fun z3f214 (Int) Int)
+(declare-fun z3v215 () Int)
+(declare-fun z3v216 () Int)
+(declare-fun z3v218 () Int)
+(declare-fun z3v220 () Int)
+(declare-fun z3v221 () Int)
+(declare-fun z3v222 () Int)
+(declare-fun z3v223 () Int)
+(declare-fun z3v224 () Int)
+(declare-fun z3v225 () Int)
+(declare-fun z3v226 () Int)
+(declare-fun z3v227 () Int)
+(declare-fun z3v228 () Int)
+(declare-fun z3v229 () Int)
+(declare-fun z3v230 () Int)
+(declare-fun z3v231 () Int)
+(declare-fun z3v233 () Int)
+(declare-fun z3v236 () Int)
+(declare-fun z3v242 () Int)
+(declare-fun z3v243 () Int)
+(declare-fun z3v244 () Int)
+(declare-fun z3v245 () Int)
+(declare-fun z3v247 () Int)
+(declare-fun z3v248 () Int)
+(declare-fun z3v249 () Int)
+(declare-fun z3v250 () Int)
+(declare-fun z3v251 () Int)
+(declare-fun z3v252 () Int)
+(declare-fun z3v253 () Int)
+(declare-fun z3v255 () Int)
+(declare-fun z3v256 () Int)
+(declare-fun z3v258 () Int)
+(declare-fun z3v259 () Int)
+(declare-fun z3v261 () Int)
+(declare-fun z3v262 () Int)
+(declare-fun z3v263 () Int)
+(declare-fun z3v264 () Int)
+(declare-fun z3v266 () Int)
+(declare-fun z3v268 () Int)
+(declare-fun z3v270 () Int)
+(declare-fun z3v271 () Int)
+(declare-fun z3v272 () Int)
+(declare-fun z3v274 () Int)
+(declare-fun z3v275 () Int)
+(declare-fun z3v276 () Int)
+(declare-fun z3v278 () Int)
+(declare-fun z3v279 () Int)
+(declare-fun z3v281 () Int)
+(declare-fun z3v282 () Int)
+(declare-fun z3v283 () Int)
+(declare-fun z3v284 () Int)
+(declare-fun z3v285 () Int)
+(declare-fun z3v287 () Int)
+(declare-fun z3v289 () Int)
+(declare-fun z3v290 () Int)
+(declare-fun z3v291 () Int)
+(declare-fun z3v292 () Int)
+(declare-fun z3v293 () Int)
+(declare-fun z3v296 () Int)
+(declare-fun z3v298 () Int)
+(declare-fun z3v299 () Int)
+(declare-fun z3f300 (Int Int) Int)
+(declare-fun z3v301 () Int)
+(declare-fun z3v302 () Int)
+(declare-fun z3v303 () Int)
+(declare-fun z3v304 () Int)
+(declare-fun z3v308 () Int)
+(declare-fun z3v309 () Int)
+(declare-fun z3v310 () Int)
+(declare-fun z3v314 () Int)
+(declare-fun z3v315 () Int)
+(declare-fun z3v316 () Int)
+(declare-fun z3v317 () Int)
+(declare-fun z3v318 () Int)
+(declare-fun z3v319 () Int)
+(declare-fun z3v320 () Int)
+(declare-fun z3v324 () Int)
+(declare-fun z3v325 () Int)
+(declare-fun z3v326 () Int)
+(declare-fun z3v327 () Int)
+(declare-fun z3v328 () Int)
+(declare-fun z3v330 () Int)
+(declare-fun z3v332 () Int)
+(declare-fun z3v333 () Int)
+(declare-fun z3v334 () Int)
+(declare-fun z3v335 () Int)
+(declare-fun z3v336 () Int)
+(declare-fun z3v337 () Int)
+(declare-fun z3v339 () Int)
+(declare-fun z3v340 () Int)
+(declare-fun z3v341 () Int)
+(declare-fun z3v342 () Int)
+(assert (= z3v342 z3v113))
+(assert (>= (z3f69 z3v342) 0))
+(assert (and (>= (z3f69 z3v113) 0) (>= (z3f69 z3v114) 0) (= (z3f72 z3v114) smt_set_emp) (= (z3f70 z3v114) smt_set_emp) (= (z3f69 z3v114) 0) (= (z3f76 z3v114) true) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) (ite (smt_set_mem z3v116 (z3f70 z3v113)) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f72 z3v113)) (z3f72 z3v113))) (= (z3f70 z3v115) (smt_set_cup (smt_set_add smt_set_emp z3v116) (z3f70 z3v113))) (= (z3f69 z3v115) (+ 1 (z3f69 z3v113))) (= (z3f76 z3v115) false) (= z3v115 (z3f77 z3v116 z3v113)) (>= (z3f69 z3v115) 0) (= z3v115 z3v117) (>= (z3f69 z3v115) 0) (= (z3f72 z3v115) smt_set_emp) (>= (z3f69 z3v117) 0) (= (z3f72 z3v117) smt_set_emp) (z3f79 z3v66) (= (z3f81 z3v80) z3v80) (= (z3f81 z3v82) z3v82) (not (z3f79 z3v67)) (= (z3f81 z3v83) z3v83)))
+(assert (not (and (= (z3f72 z3v342) smt_set_emp) (not (smt_set_mem z3v116 (z3f70 z3v342))))))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+
+; Observed
+;
+; sat as output instead of unsat
+;
+; What was going on?
+;
+; The solver was unable to reason that (emptyset) cannot equal
+; (setenum 0). There were no membership predicates anywhere, just
+; equalities.
+;
+; Fix
+;
+; Add the propagation rule: (true) => (in x (setenum x))
+
+(declare-fun z3f70 (Int) (Set Int))
+(declare-fun z3v85 () Int)
+(declare-fun z3v86 () Int)
+(declare-fun z3v87 () Int)
+(declare-fun z3v90 () Int)
+
+(assert (= (z3f70 z3v90) (union (z3f70 z3v85) (union (as emptyset (Set Int)) (setenum z3v86)))))
+(assert (= (z3f70 z3v90) (z3f70 z3v87)))
+(assert (= (as emptyset (Set Int)) (z3f70 z3v87)))
+(check-sat)
--- /dev/null
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort Elt () Int)
+(define-sort mySet ()
+ (Set Elt ))
+(define-fun smt_set_emp () mySet (as emptyset mySet))
+
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+(declare-fun x () Int)
+
+(assert (or (not (= S smt_set_emp)) (in x T)))
+
+(assert (= smt_set_emp
+ (ite (in x T)
+ (union (union smt_set_emp (setenum x)) S)
+ S)))
+(check-sat)
--- /dev/null
+(set-option :print-success false)
+(set-logic AUFLIA_SETS)
+(set-info :status unsat)
+(declare-sort Loc 0)
+(define-sort SetLoc () (Set Loc))
+(define-sort SetInt () (Set Int))
+(declare-sort FldLoc 0)
+(declare-sort FldInt 0)
+(declare-fun null$0 () Loc)
+(declare-fun read$0 (FldLoc Loc) Loc)
+(declare-fun Btwn$0 (FldLoc Loc Loc Loc) Bool)
+(declare-fun Alloc$0 () SetLoc)
+(declare-fun Alloc_2$0 () SetLoc)
+(declare-fun FP$0 () SetLoc)
+(declare-fun FP_3$0 () SetLoc)
+(declare-fun FP_Caller$0 () SetLoc)
+(declare-fun FP_Caller_2$0 () SetLoc)
+(declare-fun cp$0 () Loc)
+(declare-fun cp_1$0 () Loc)
+(declare-fun curr$0 () Loc)
+(declare-fun lseg_domain$0 (FldLoc Loc Loc) SetLoc)
+(declare-fun lseg_struct$0 (SetLoc FldLoc Loc Loc) Bool)
+(declare-fun next$0 () FldLoc)
+(declare-fun old_cp_2$0 () Loc)
+(declare-fun sk_?X_36$0 () SetLoc)
+(declare-fun sk_?X_37$0 () SetLoc)
+(declare-fun sk_?X_38$0 () SetLoc)
+(declare-fun tmp_1$0 () Loc)
+
+(assert (! (forall ((?y Loc))
+ (or (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)
+ (Btwn$0 next$0 null$0 (read$0 next$0 null$0) ?y)))
+ :named btwn_reach_6))
+
+(assert (! (forall ((?y Loc))
+ (or (not (= (read$0 next$0 null$0) null$0))
+ (not (Btwn$0 next$0 null$0 ?y ?y)) (= null$0 ?y)))
+ :named btwn_cycl_6))
+
+(assert (! (Btwn$0 next$0 null$0 (read$0 next$0 null$0) (read$0 next$0 null$0))
+ :named btwn_step_6))
+
+(assert (! (= (read$0 next$0 null$0) null$0) :named read_null_6))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 curr$0 l1 null$0)
+ (in l1 (lseg_domain$0 next$0 curr$0 null$0))
+ (not (= l1 null$0)))
+ (and (or (= l1 null$0) (not (Btwn$0 next$0 curr$0 l1 null$0)))
+ (not (in l1 (lseg_domain$0 next$0 curr$0 null$0))))))
+ :named lseg_footprint_14))
+
+(assert (! (not (in tmp_1$0 Alloc$0)) :named new_42_10))
+
+(assert (! (not (in null$0 Alloc$0))
+ :named initial_footprint_of_rec_copy_loop_34_11_4))
+
+(assert (! (not (= curr$0 null$0)) :named if_else_37_6))
+
+(assert (! (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0)
+ :named precondition_of_rec_copy_loop_34_11_16))
+
+(assert (! (= sk_?X_38$0 (lseg_domain$0 next$0 cp$0 null$0))
+ :named precondition_of_rec_copy_loop_34_11_17))
+
+(assert (! (= sk_?X_36$0 FP$0) :named precondition_of_rec_copy_loop_34_11_18))
+
+(assert (! (= (as emptyset SetLoc) (intersection sk_?X_38$0 sk_?X_37$0))
+ :named precondition_of_rec_copy_loop_34_11_19))
+
+(assert (! (= old_cp_2$0 cp$0) :named assign_41_4))
+
+(assert (! (= FP_Caller_2$0 (setminus FP_Caller$0 FP$0)) :named assign_37_2_2))
+
+(assert (! (= Alloc_2$0 (union Alloc$0 (setenum tmp_1$0))) :named assign_42_10))
+
+(assert (! (or (Btwn$0 next$0 cp$0 null$0 null$0)
+ (not (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0)))
+ :named unnamed_22))
+
+(assert (! (forall ((l1 Loc))
+ (or
+ (and (Btwn$0 next$0 cp$0 l1 null$0)
+ (in l1 (lseg_domain$0 next$0 cp$0 null$0))
+ (not (= l1 null$0)))
+ (and (or (= l1 null$0) (not (Btwn$0 next$0 cp$0 l1 null$0)))
+ (not (in l1 (lseg_domain$0 next$0 cp$0 null$0))))))
+ :named lseg_footprint_15))
+
+(assert (! (not (in cp_1$0 FP_3$0)) :named check_heap_access_43_4))
+
+(assert (! (not (= tmp_1$0 null$0)) :named new_42_10_1))
+
+(assert (! (lseg_struct$0 sk_?X_38$0 next$0 cp$0 null$0)
+ :named precondition_of_rec_copy_loop_34_11_20))
+
+(assert (! (= FP_Caller$0 (union FP$0 FP_Caller$0))
+ :named precondition_of_rec_copy_loop_34_11_21))
+
+(assert (! (= sk_?X_37$0 (lseg_domain$0 next$0 curr$0 null$0))
+ :named precondition_of_rec_copy_loop_34_11_22))
+
+(assert (! (= sk_?X_36$0 (union sk_?X_37$0 sk_?X_38$0))
+ :named precondition_of_rec_copy_loop_34_11_23))
+
+(assert (! (= Alloc$0 (union FP_Caller$0 Alloc$0))
+ :named initial_footprint_of_rec_copy_loop_34_11_5))
+
+(assert (! (= cp_1$0 tmp_1$0) :named assign_42_4))
+
+(assert (! (= FP_3$0 (union FP$0 (setenum tmp_1$0))) :named assign_42_10_1))
+
+(assert (! (or (Btwn$0 next$0 curr$0 null$0 null$0)
+ (not (lseg_struct$0 sk_?X_37$0 next$0 curr$0 null$0)))
+ :named unnamed_23))
+
+(assert (! (forall ((?x Loc)) (Btwn$0 next$0 ?x ?x ?x)) :named btwn_refl_6))
+
+(assert (! (forall ((?x Loc) (?y Loc)) (or (not (Btwn$0 next$0 ?x ?y ?x)) (= ?x ?y)))
+ :named btwn_sndw_6))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?x ?z ?z))
+ (Btwn$0 next$0 ?x ?y ?z) (Btwn$0 next$0 ?x ?z ?y)))
+ :named btwn_ord1_6))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z))
+ (and (Btwn$0 next$0 ?x ?y ?y) (Btwn$0 next$0 ?y ?z ?z))))
+ :named btwn_ord2_6))
+
+(assert (! (forall ((?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?y)) (not (Btwn$0 next$0 ?y ?z ?z))
+ (Btwn$0 next$0 ?x ?z ?z)))
+ :named btwn_trn1_6))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?y ?u ?z))
+ (and (Btwn$0 next$0 ?x ?y ?u) (Btwn$0 next$0 ?x ?u ?z))))
+ :named btwn_trn2_6))
+
+(assert (! (forall ((?u Loc) (?x Loc) (?y Loc) (?z Loc))
+ (or (not (Btwn$0 next$0 ?x ?y ?z)) (not (Btwn$0 next$0 ?x ?u ?y))
+ (and (Btwn$0 next$0 ?x ?u ?z) (Btwn$0 next$0 ?u ?y ?z))))
+ :named btwn_trn3_6))
+
+(check-sat)
+(exit)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun S () (Set Int))
+(declare-fun T () (Set Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (in y S))
+(assert (not (in x (union S T))))
+(assert (= x y))
+(check-sat)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun x () Int)
+(declare-fun y () Int)
+(declare-fun z () Int)
+(assert (= x y))
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(assert (not (in x a)))
+(assert (in y (union a b)))
+(assert (= x z))
+(assert (not (in z a)))
+(assert (= a b))
+(check-sat)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(define-sort SetInt () (Set Int))
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(declare-fun x () Int)
+;(assert (not (in x a)))
+(assert (in x (intersection a b)))
+(assert (not (in x b)))
+(check-sat)
+(exit)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort SetInt () (Set Int))
+
+(declare-fun A () SetInt)
+(declare-fun B () SetInt)
+(declare-fun x () Int)
+(assert (in x (union A B)))
+
+(assert (not (in x (intersection A B))))
+(assert (not (in x (setminus A B))))
+;(assert (not (in x (setminus B A))))
+;(assert (in x B))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+
+; Something simple to test parsing
+(push 1)
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(declare-fun c () (Set Int))
+(declare-fun e () Int)
+(assert (= a (setenum 5)))
+(assert (= c (union a b) ))
+(assert (not (= c (intersection a b) )))
+(assert (= c (setminus a b) ))
+(assert (subseteq a b))
+(assert (in e c))
+(assert (in e a))
+(assert (in e (intersection a b)))
+(check-sat)
+(pop 1)
+
+; UF can tell that this is UNSAT (union)
+(push 1)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(declare-fun z () (Set Int))
+(assert (= x y))
+(assert (not (= (union x z) (union y z))))
+(check-sat)
+(pop 1)
+
+; UF can tell that this is UNSAT (containment)
+(push 1)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(declare-fun e1 () Int)
+(declare-fun e2 () Int)
+(assert (= x y))
+(assert (= e1 e2))
+(assert (in e1 x))
+(assert (not (in e2 y)))
+(check-sat)
+(pop 1)
+
+; UF can tell that this is UNSAT (merge union + containment examples)
+(push 1)
+(declare-fun x () (Set Int))
+(declare-fun y () (Set Int))
+(declare-fun z () (Set Int))
+(declare-fun e1 () Int)
+(declare-fun e2 () Int)
+(assert (= x y))
+(assert (= e1 e2))
+(assert (in e1 (union x z)))
+(assert (not (in e2 (union y z))))
+(check-sat)
+(pop 1)
+
+(exit)
+(exit)
--- /dev/null
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+
+(declare-fun S () (Set Int))
+(declare-fun x () Int)
+
+(assert (in (+ 5 x) S))
+(assert (not (in 9 S)))
+(assert (= x 4))
+
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic QF_UFLIA_SETS)
+(set-info :status sat)
+(declare-fun x () (Set (_ BitVec 2)))
+(declare-fun y () (Set (_ BitVec 2)))
+(assert (not (= x y)))
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental --no-check-model
+; EXPECT: sat
+; EXPECT: unsat
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun a () (Set Int))
+(declare-fun b () (Set Int))
+(declare-fun x () Int)
+(assert (not (in x a)))
+(assert (in x (union a b)))
+(check-sat)
+;(get-model)
+(assert (not (in x b)))
+(check-sat)
+(exit)
--- /dev/null
+; COMMAND-LINE: --incremental --no-check-models
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (in x A))
+(push 1)
+(assert (not (in x (union A B))))
+(check-sat)
+(pop 1)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (not (in x (union A B))))
+(push 1)
+(assert (in x A))
+(check-sat)
+(pop 1)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental --no-check-models
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (in x B))
+(push 1)
+(assert (not (in x (union A B))))
+(check-sat)
+(pop 1)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --incremental
+; EXPECT: unsat
+; EXPECT: sat
+
+; x not in A U B => x not in A
+(set-logic ALL_SUPPORTED)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(assert (not (in x (union A B))))
+(push 1)
+(assert (in x B))
+(check-sat)
+(pop 1)
+(check-sat)
--- /dev/null
+; COMMAND-LINE: --no-check-models
+; EXPECT: sat
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(define-sort SetInt () (Set Int))
+(declare-fun A () (Set Int))
+(declare-fun B () (Set Int))
+(declare-fun x () Int)
+(declare-fun y () Int)
+(assert (in x (union A B)))
+(assert (not (in y A)))
+(assert (not (in y B)))
+(check-sat)
info = info.getUnlockedCopy();
TS_ASSERT( !info.isLocked() );
info.disableTheory(THEORY_STRINGS);
+ info.disableTheory(THEORY_SETS);
info.arithOnlyLinear();
info.disableIntegers();
info.lock();
projects / cvc5.git / commitdiff