From: Kshitij Bansal Date: Mon, 9 Sep 2013 18:47:53 +0000 (-0400) Subject: add new theory (sets) X-Git-Tag: cvc5-1.0.0~7076^2~1 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=50c26544c83a71e87efa487e4af063b1b5647c0f;p=cvc5.git add new theory (sets) Specification (smt2) -- as per this commit, subject to change - Parameterized sort Set, e.g. (Set Int) - Empty set constant (typed), use with "as" to specify the type, e.g. (as emptyset (Set Int)) - Create a singleton set (setenum X (Set X)) : creates singleton set - Functions/operators (union (Set X) (Set X) (Set X)) (intersection (Set X) (Set X) (Set X)) (setminus (Set X) (Set X) (Set X)) - Predicates (in X (Set X) Bool) : membership (subseteq (Set X) (Set X) Bool) : set containment --- diff --git a/.gitignore b/.gitignore index 741f08ccd..b3cce03ed 100644 --- a/.gitignore +++ b/.gitignore @@ -30,3 +30,4 @@ config.reconfig /debug/ /personal.conf /personal.mk +/antlr-3.4 diff --git a/src/Makefile.am b/src/Makefile.am index f20fabf6b..86067d3ef 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -20,7 +20,7 @@ AM_CPPFLAGS = \ 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 @@ -220,6 +220,13 @@ libcvc4_la_SOURCES = \ 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 \ @@ -453,6 +460,7 @@ EXTRA_DIST = \ theory/idl/kinds \ theory/builtin/kinds \ theory/datatypes/kinds \ + theory/sets/kinds \ theory/strings/kinds \ theory/arrays/kinds \ theory/quantifiers/kinds \ diff --git a/src/context/cdhashset.h b/src/context/cdhashset.h index e2ffac49b..881c3f629 100644 --- a/src/context/cdhashset.h +++ b/src/context/cdhashset.h @@ -57,6 +57,10 @@ public: return super::size(); } + bool empty() const { + return super::empty(); + } + bool insert(const V& v) { return super::insert_safe(v, true); } diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5fe7b34c1..41f69e587 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -540,6 +540,11 @@ ArrayType ExprManager::mkArrayType(Type indexType, Type constituentType) const { 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. diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3f0ec2f9c..f5e01d545 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -376,6 +376,9 @@ public: /** 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); diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index caf8f5ad4..b4d20b514 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -751,6 +751,9 @@ public: /** 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); @@ -1058,6 +1061,16 @@ inline TypeNode NodeManager::mkArrayType(TypeNode indexType, 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"); diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 672fc6aae..d0fe77aae 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -292,6 +292,12 @@ bool Type::isArray() const { 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); @@ -480,6 +486,11 @@ ArrayType::ArrayType(const Type& t) throw(IllegalArgumentException) : 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); @@ -517,6 +528,10 @@ Type ArrayType::getConstituentType() const { return makeType(d_typeNode->getArrayConstituentType()); } +Type SetType::getElementType() const { + return makeType(d_typeNode->getSetElementType()); +} + DatatypeType ConstructorType::getRangeType() const { return DatatypeType(makeType(d_typeNode->getConstructorRangeType())); } diff --git a/src/expr/type.h b/src/expr/type.h index 3c772d461..b4761e1d6 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -49,6 +49,7 @@ class RealType; class StringType; class BitVectorType; class ArrayType; +class SetType; class DatatypeType; class ConstructorType; class SelectorType; @@ -301,6 +302,12 @@ public: 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 */ @@ -488,6 +495,20 @@ public: 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. */ diff --git a/src/expr/type_node.h b/src/expr/type_node.h index c823190bf..a49ae31bf 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -466,6 +466,9 @@ public: /** 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; @@ -475,6 +478,9 @@ public: /** 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 @@ -867,6 +873,15 @@ inline TypeNode TypeNode::getConstructorRangeType() const { 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; } diff --git a/src/options/Makefile.am b/src/options/Makefile.am index 5b0894680..8780922c9 100644 --- a/src/options/Makefile.am +++ b/src/options/Makefile.am @@ -40,7 +40,9 @@ 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 OPTIONS_FILES = \ $(patsubst %.cpp,%,$(filter %.cpp,$(OPTIONS_FILES_SRCS))) @@ -101,7 +103,9 @@ nodist_liboptions_la_SOURCES = \ ../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 \ diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index f97f4a8ae..6974c62af 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -833,6 +833,11 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] 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."); @@ -1028,6 +1033,9 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] | str[s,false] { expr = MK_CONST( ::CVC4::String(s) ); } + | EMPTYSET_TOK + { expr = MK_CONST( ::CVC4::EmptySet()); } + // NOTE: Theory constants go here ; @@ -1298,6 +1306,12 @@ builtinOp[CVC4::Kind& kind] | 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 ; @@ -1407,6 +1421,11 @@ sortSymbol[CVC4::Type& t, CVC4::parser::DeclarationCheck check] 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); @@ -1688,6 +1707,14 @@ REPLUS_TOK : 're.+'; 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 |. diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5dc3043af..fcb352ea7 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -203,6 +203,10 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, break; } + case kind::EMPTYSET: + out << "(as emptyset " << n.getConst().getType() << ")"; + break; + default: // fall back on whatever operator<< does on underlying type; we // might luck out and be SMT-LIB v2 compliant @@ -343,7 +347,16 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, 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); @@ -528,6 +541,14 @@ static string smtKindString(Kind k) throw() { 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 */ } diff --git a/src/theory/arrays/array_info.h b/src/theory/arrays/array_info.h index 1f97c02ca..0a2a96603 100644 --- a/src/theory/arrays/array_info.h +++ b/src/theory/arrays/array_info.h @@ -75,8 +75,6 @@ public: } ~Info() { - //FIXME! - //indices->deleteSelf(); indices->deleteSelf(); stores->deleteSelf(); in_stores->deleteSelf(); diff --git a/src/theory/logic_info.cpp b/src/theory/logic_info.cpp index 525b129cf..a30867ee1 100644 --- a/src/theory/logic_info.cpp +++ b/src/theory/logic_info.cpp @@ -122,6 +122,10 @@ std::string LogicInfo::getLogicString() const { } ++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 " @@ -256,6 +260,10 @@ void LogicInfo::setLogicString(std::string logicString) throw(IllegalArgumentExc arithNonLinear(); p += 4; } + if(!strncmp(p, "_SETS", 5)) { + enableTheory(THEORY_SETS); + p += 5; + } } } if(*p != '\0') { diff --git a/src/theory/sets/.gitignore b/src/theory/sets/.gitignore new file mode 100644 index 000000000..4c83ffd6f --- /dev/null +++ b/src/theory/sets/.gitignore @@ -0,0 +1 @@ +README.WHATS-NEXT diff --git a/src/theory/sets/Makefile b/src/theory/sets/Makefile new file mode 100644 index 000000000..68a2c5cb6 --- /dev/null +++ b/src/theory/sets/Makefile @@ -0,0 +1,4 @@ +topdir = ../../.. +srcdir = src/theory/sets + +include $(topdir)/Makefile.subdir diff --git a/src/theory/sets/Makefile.am b/src/theory/sets/Makefile.am new file mode 100644 index 000000000..00678628f --- /dev/null +++ b/src/theory/sets/Makefile.am @@ -0,0 +1,20 @@ +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 diff --git a/src/theory/sets/expr_patterns.h b/src/theory/sets/expr_patterns.h new file mode 100644 index 000000000..089549457 --- /dev/null +++ b/src/theory/sets/expr_patterns.h @@ -0,0 +1,51 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/sets/kinds b/src/theory/sets/kinds new file mode 100644 index 000000000..bae0c5f1d --- /dev/null +++ b/src/theory/sets/kinds @@ -0,0 +1,55 @@ +# 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 diff --git a/src/theory/sets/options b/src/theory/sets/options new file mode 100644 index 000000000..dc6c6e907 --- /dev/null +++ b/src/theory/sets/options @@ -0,0 +1,14 @@ +# +# 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 diff --git a/src/theory/sets/options_handlers.h b/src/theory/sets/options_handlers.h new file mode 100644 index 000000000..ff535945e --- /dev/null +++ b/src/theory/sets/options_handlers.h @@ -0,0 +1,14 @@ +#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 */ diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h new file mode 100644 index 000000000..ea435d9b7 --- /dev/null +++ b/src/theory/sets/term_info.h @@ -0,0 +1,57 @@ +/********************* */ +/*! \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 CDTNodeList; +typedef context::CDHashSet CDNodeSet; +typedef context::CDHashSet 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 */ diff --git a/src/theory/sets/theory_sets.cpp b/src/theory/sets/theory_sets.cpp new file mode 100644 index 000000000..91195e67e --- /dev/null +++ b/src/theory/sets/theory_sets.cpp @@ -0,0 +1,55 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h new file mode 100644 index 000000000..c95229f05 --- /dev/null +++ b/src/theory/sets/theory_sets.h @@ -0,0 +1,65 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp new file mode 100644 index 000000000..8fd490554 --- /dev/null +++ b/src/theory/sets/theory_sets_private.cpp @@ -0,0 +1,871 @@ +/********************* */ +/*! \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& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set 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::const_iterator it = all.begin(); + std::set::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(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 np = d_settermPropagationQueue.front(); + d_settermPropagationQueue.pop(); + doSettermPropagation(np.first, np.second); + } + while(!d_conflict && !d_propagationQueue.empty()) { + std::pair 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 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(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 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 */ diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h new file mode 100644 index 000000000..f1a8c0a46 --- /dev/null +++ b/src/theory/sets/theory_sets_private.h @@ -0,0 +1,166 @@ +/********************* */ +/*! \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 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 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 > d_propagationQueue; + context::CDQueue< std::pair > 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 d_nodeSaver; + + /** Lemmas and helper functions */ + context::CDQueue d_pending; + context::CDQueue d_pendingDisequal; + context::CDHashSet 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 */ diff --git a/src/theory/sets/theory_sets_rewriter.cpp b/src/theory/sets/theory_sets_rewriter.cpp new file mode 100644 index 000000000..11a2e9297 --- /dev/null +++ b/src/theory/sets/theory_sets_rewriter.cpp @@ -0,0 +1,110 @@ +#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 */ diff --git a/src/theory/sets/theory_sets_rewriter.h b/src/theory/sets/theory_sets_rewriter.h new file mode 100644 index 000000000..f01d198cf --- /dev/null +++ b/src/theory/sets/theory_sets_rewriter.h @@ -0,0 +1,77 @@ +#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 */ diff --git a/src/theory/sets/theory_sets_type_enumerator.h b/src/theory/sets/theory_sets_type_enumerator.h new file mode 100644 index 000000000..2f4cc6a2f --- /dev/null +++ b/src/theory/sets/theory_sets_type_enumerator.h @@ -0,0 +1,161 @@ + +#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 { + unsigned d_index; + TypeNode d_constituentType; + NodeManager* d_nm; + std::vector d_indexVec; + std::vector d_constituentVec; + bool d_finished; + Node d_setConst; + +public: + + SetEnumerator(TypeNode type) throw(AssertionException) : + TypeEnumeratorBase(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(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::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 */ diff --git a/src/theory/sets/theory_sets_type_rules.h b/src/theory/sets/theory_sets_type_rules.h new file mode 100644 index 000000000..026c90ca4 --- /dev/null +++ b/src/theory/sets/theory_sets_type_rules.h @@ -0,0 +1,176 @@ +#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(); + 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 */ diff --git a/src/theory/theory.h b/src/theory/theory.h index 2359d5d86..e8d53e539 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -620,6 +620,9 @@ public: * 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() { } diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 47ba50aad..63024e5d5 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -671,6 +671,7 @@ bool TheoryEngine::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 @@ -680,7 +681,7 @@ void TheoryEngine::postsolve() { #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \ if (theory::TheoryTraits::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 @@ -961,7 +962,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo 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; @@ -1011,6 +1012,7 @@ void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theo // 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; } } diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index f8e361081..8bb849496 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -833,12 +833,14 @@ public: 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; diff --git a/src/util/Makefile.am b/src/util/Makefile.am index 1d6ce1a73..0717df907 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -87,6 +87,8 @@ libutil_la_SOURCES = \ abstract_value.cpp \ array_store_all.h \ array_store_all.cpp \ + emptyset.h \ + emptyset.cpp \ model.h \ model.cpp \ sort_inference.h \ diff --git a/src/util/emptyset.cpp b/src/util/emptyset.cpp new file mode 100644 index 000000000..fa1bb8f10 --- /dev/null +++ b/src/util/emptyset.cpp @@ -0,0 +1,12 @@ +#include "util/emptyset.h" +#include + +using namespace std; + +namespace CVC4 { + +std::ostream& operator<<(std::ostream& out, const EmptySet& asa) { + return out << "emptyset(" << asa.getType() << ')'; +} + +}/* CVC4 namespace */ diff --git a/src/util/emptyset.h b/src/util/emptyset.h new file mode 100644 index 000000000..aae08e43b --- /dev/null +++ b/src/util/emptyset.h @@ -0,0 +1,65 @@ + +#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 + +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 */ + + +} diff --git a/test/Makefile.am b/test/Makefile.am index 8a7a5a0a7..1da15dc43 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -56,6 +56,7 @@ subdirs_to_check = \ regress/regress0/decision \ regress/regress0/fmf \ regress/regress0/strings \ + regress/regress0/sets \ regress/regress1 \ regress/regress1/arith \ regress/regress2 \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index d7663e298..067b5d381 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,5 +1,5 @@ -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),) diff --git a/test/regress/regress0/quantifiers/set8.smt2 b/test/regress/regress0/quantifiers/set8.smt2 index 684d94b7a..6e4a84672 100644 --- a/test/regress/regress0/quantifiers/set8.smt2 +++ b/test/regress/regress0/quantifiers/set8.smt2 @@ -1,26 +1,26 @@ (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) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 index 9bd49f714..56228e082 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base.smt2 @@ -2,124 +2,124 @@ (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) diff --git a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 index 4d65ffac5..2a7e59d6e 100644 --- a/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 +++ b/test/regress/regress0/rewriterules/set_A_new_fast_tableau-base_sat.smt2 @@ -2,11 +2,11 @@ (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) ;;;;;;;;;;;;;;;;;;;; @@ -14,112 +14,112 @@ (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) diff --git a/test/regress/regress0/sets/Makefile b/test/regress/regress0/sets/Makefile new file mode 100644 index 000000000..67ae35206 --- /dev/null +++ b/test/regress/regress0/sets/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/sets + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/sets/Makefile.am b/test/regress/regress0/sets/Makefile.am new file mode 100644 index 000000000..f040a6cd0 --- /dev/null +++ b/test/regress/regress0/sets/Makefile.am @@ -0,0 +1,75 @@ +# 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: diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 new file mode 100644 index 000000000..a8eccf4ad --- /dev/null +++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 @@ -0,0 +1,133 @@ +(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) diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2 new file mode 100644 index 000000000..47fc25661 --- /dev/null +++ b/test/regress/regress0/sets/emptyset.smt2 @@ -0,0 +1,4 @@ +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(assert (in 5 (as emptyset (Set Int) ))) +(check-sat) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 new file mode 100644 index 000000000..02577b00a --- /dev/null +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -0,0 +1,18 @@ +(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) diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2 new file mode 100644 index 000000000..c4b3dd551 --- /dev/null +++ b/test/regress/regress0/sets/error1.smt2 @@ -0,0 +1,14 @@ +; 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) diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2 new file mode 100644 index 000000000..ac678c552 --- /dev/null +++ b/test/regress/regress0/sets/error2.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_ALL_SUPPORTED) +(set-info :status unsat) +(assert (= (as emptyset (Set Int)) (setenum 5))) +(check-sat) diff --git a/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 new file mode 100644 index 000000000..290ee95d5 --- /dev/null +++ b/test/regress/regress0/sets/feb3/ListElts.hs.fqout.cvc4.317.smt2 @@ -0,0 +1,99 @@ +; 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) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 new file mode 100644 index 000000000..b90563199 --- /dev/null +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -0,0 +1,75 @@ +(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) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 new file mode 100644 index 000000000..204af2f2d --- /dev/null +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -0,0 +1,18 @@ +(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) diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 new file mode 100644 index 000000000..ad0a7e464 --- /dev/null +++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 @@ -0,0 +1,812 @@ +(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) diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 new file mode 100644 index 000000000..c1c65cea5 --- /dev/null +++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 @@ -0,0 +1,470 @@ +(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) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 new file mode 100644 index 000000000..c4ee3b710 --- /dev/null +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 @@ -0,0 +1,18 @@ +(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). diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 new file mode 100644 index 000000000..7fea3435e --- /dev/null +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -0,0 +1,49 @@ +(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) diff --git a/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 new file mode 100644 index 000000000..6c32bb578 --- /dev/null +++ b/test/regress/regress0/sets/jan27/ListElem.hs.fqout.cvc4.38.smt2 @@ -0,0 +1,59 @@ +(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) diff --git a/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 new file mode 100644 index 000000000..bcc4c33da --- /dev/null +++ b/test/regress/regress0/sets/jan27/deepmeas0.hs.fqout.cvc4.41.smt2 @@ -0,0 +1,59 @@ +; 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) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 new file mode 100644 index 000000000..5a44c0344 --- /dev/null +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -0,0 +1,34 @@ +; 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) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 new file mode 100644 index 000000000..67d64bd05 --- /dev/null +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.cvc4.3577.smt2 @@ -0,0 +1,287 @@ +; 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) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 new file mode 100644 index 000000000..f37a8ccfe --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.10.smt2 @@ -0,0 +1,106 @@ +(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) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 new file mode 100644 index 000000000..59cc1a00e --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.cvc4.1832.smt2 @@ -0,0 +1,227 @@ +(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) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 new file mode 100644 index 000000000..5fa5101f0 --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -0,0 +1,27 @@ +(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) diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 new file mode 100644 index 000000000..d01b7468e --- /dev/null +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 @@ -0,0 +1,18 @@ +(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) diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 new file mode 100644 index 000000000..57d5d72ca --- /dev/null +++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 @@ -0,0 +1,149 @@ +(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) diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2 new file mode 100644 index 000000000..8ed9a2e57 --- /dev/null +++ b/test/regress/regress0/sets/setel-eq.smt2 @@ -0,0 +1,10 @@ +(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) diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2 new file mode 100644 index 000000000..a2ce4b3c2 --- /dev/null +++ b/test/regress/regress0/sets/sets-equal.smt2 @@ -0,0 +1,14 @@ +(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) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 new file mode 100644 index 000000000..0f5e41864 --- /dev/null +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -0,0 +1,11 @@ +(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) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 new file mode 100644 index 000000000..c85ae4837 --- /dev/null +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -0,0 +1,17 @@ +; 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) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 new file mode 100644 index 000000000..1bd0eb396 --- /dev/null +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -0,0 +1,64 @@ +; 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) diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2 new file mode 100644 index 000000000..d2a94fdf4 --- /dev/null +++ b/test/regress/regress0/sets/sets-sharing.smt2 @@ -0,0 +1,11 @@ +(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) diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2 new file mode 100644 index 000000000..74ce72747 --- /dev/null +++ b/test/regress/regress0/sets/sets-testlemma.smt2 @@ -0,0 +1,8 @@ +; 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) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 new file mode 100644 index 000000000..6f6d3e019 --- /dev/null +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -0,0 +1,15 @@ +; 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) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 new file mode 100644 index 000000000..59c2a2024 --- /dev/null +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -0,0 +1,16 @@ +; 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) diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2 new file mode 100644 index 000000000..b594ac74d --- /dev/null +++ b/test/regress/regress0/sets/union-1a.smt2 @@ -0,0 +1,16 @@ +; 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) diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 new file mode 100644 index 000000000..86fed459b --- /dev/null +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -0,0 +1,16 @@ +; 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) diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2 new file mode 100644 index 000000000..85fce759c --- /dev/null +++ b/test/regress/regress0/sets/union-1b.smt2 @@ -0,0 +1,16 @@ +; 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) diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 new file mode 100644 index 000000000..32d949a53 --- /dev/null +++ b/test/regress/regress0/sets/union-2.smt2 @@ -0,0 +1,13 @@ +; 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) diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index 5f6a93ae7..f569d6389 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -512,6 +512,7 @@ public: info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); info.disableTheory(THEORY_STRINGS); + info.disableTheory(THEORY_SETS); info.arithOnlyLinear(); info.disableIntegers(); info.lock();