From: Tim King Date: Wed, 30 Apr 2014 21:28:00 +0000 (-0400) Subject: T-entailment work, and QCF (quant conflict find) work that uses it. X-Git-Tag: cvc5-1.0.0~6939^2 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c5e4a56d4895ce29cd37bac027bb3d486d687f9d;p=cvc5.git T-entailment work, and QCF (quant conflict find) work that uses it. This commit includes work from the past month on the T-entailment check infrastructure (due to Tim), an entailment check for arithmetic (also Tim), and QCF work that uses T-entailment (due to Andrew Reynolds). Signed-off-by: Morgan Deters --- diff --git a/src/Makefile.am b/src/Makefile.am index 2d306d464..e7cc9628e 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -354,6 +354,8 @@ libcvc4_la_SOURCES = \ theory/arith/fc_simplex.cpp \ theory/arith/soi_simplex.h \ theory/arith/soi_simplex.cpp \ + theory/arith/infer_bounds.h \ + theory/arith/infer_bounds.cpp \ theory/arith/approx_simplex.h \ theory/arith/approx_simplex.cpp \ theory/arith/attempt_solution_simplex.h \ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 36f9866f4..6dd1f4465 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -1192,7 +1192,7 @@ void SmtEngine::setDefaults() { if( options::ufssSymBreak() ){ options::sortInference.set( true ); } - if( options::qcfMode.wasSetByUser() ){ + if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){ options::quantConflictFind.set( true ); } diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 98aa43e71..f78893324 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -162,7 +162,7 @@ inline int deltaCoeff(Kind k){ * - (NOT (GT left right)) -> LEQ * If none of these match, it returns UNDEFINED_KIND. */ - inline Kind oldSimplifiedKind(TNode literal){ +inline Kind oldSimplifiedKind(TNode literal){ switch(literal.getKind()){ case kind::LT: case kind::GT: @@ -195,6 +195,19 @@ inline int deltaCoeff(Kind k){ } } +inline Kind negateKind(Kind k){ + switch(k){ + case kind::LT: return kind::GEQ; + case kind::GT: return kind::LEQ; + case kind::LEQ: return kind::GT; + case kind::GEQ: return kind::LT; + case kind::EQUAL: return kind::DISTINCT; + case kind::DISTINCT: return kind::EQUAL; + default: + return kind::UNDEFINED_KIND; + } +} + inline Node negateConjunctionAsClause(TNode conjunction){ Assert(conjunction.getKind() == kind::AND); NodeBuilder<> orBuilder(kind::OR); diff --git a/src/theory/arith/delta_rational.h b/src/theory/arith/delta_rational.h index 7945b44c3..c2924f239 100644 --- a/src/theory/arith/delta_rational.h +++ b/src/theory/arith/delta_rational.h @@ -191,6 +191,11 @@ public: return !(*this <= other); } + int compare(const DeltaRational& other) const{ + int cmpRes = c.cmp(other.c); + return (cmpRes != 0) ? cmpRes : (k.cmp(other.k)); + } + DeltaRational& operator=(const DeltaRational& other){ c = other.c; k = other.k; diff --git a/src/theory/arith/infer_bounds.cpp b/src/theory/arith/infer_bounds.cpp new file mode 100644 index 000000000..05a520d35 --- /dev/null +++ b/src/theory/arith/infer_bounds.cpp @@ -0,0 +1,319 @@ +/********************* */ +/*! \file infer_bounds.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "theory/arith/infer_bounds.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace arith { + +using namespace inferbounds; + +InferBoundAlgorithm::InferBoundAlgorithm() + : d_alg(None) +{} + +InferBoundAlgorithm::InferBoundAlgorithm(Algorithms a) + : d_alg(a) +{ + Assert(a != Simplex); +} + +InferBoundAlgorithm::InferBoundAlgorithm(const Maybe& simplexRounds) + : d_alg(Simplex) +{} + +Algorithms InferBoundAlgorithm::getAlgorithm() const{ + return d_alg; +} + +const Maybe& InferBoundAlgorithm::getSimplexRounds() const{ + Assert(getAlgorithm() == Simplex); + return d_simplexRounds; +} + + +InferBoundAlgorithm InferBoundAlgorithm::mkLookup(){ + return InferBoundAlgorithm(Lookup); +} + +InferBoundAlgorithm InferBoundAlgorithm::mkRowSum(){ + return InferBoundAlgorithm(RowSum); +} + +InferBoundAlgorithm InferBoundAlgorithm::mkSimplex(const Maybe& rounds){ + return InferBoundAlgorithm(rounds); +} + +ArithEntailmentCheckParameters::ArithEntailmentCheckParameters() + : EntailmentCheckParameters(theory::THEORY_ARITH) + , d_algorithms() +{} + +ArithEntailmentCheckParameters::~ArithEntailmentCheckParameters() +{} + + +void ArithEntailmentCheckParameters::addLookupRowSumAlgorithms(){ + addAlgorithm(InferBoundAlgorithm::mkLookup()); + addAlgorithm(InferBoundAlgorithm::mkRowSum()); +} + +void ArithEntailmentCheckParameters::addAlgorithm(const inferbounds::InferBoundAlgorithm& alg){ + d_algorithms.push_back(alg); +} + +ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::begin() const{ + return d_algorithms.begin(); +} + +ArithEntailmentCheckParameters::const_iterator ArithEntailmentCheckParameters::end() const{ + return d_algorithms.end(); +} + + +// SimplexInferBoundsParameters::SimplexInferBoundsParameters() +// : d_parameter(1) +// , d_upperBound(true) +// , d_threshold() +// {} + +// SimplexInferBoundsParameters::~SimplexInferBoundsParameters(){} + + + +// int SimplexInferBoundsParameters::getSimplexRoundParameter() const { +// return d_parameter; +// } + +// bool SimplexInferBoundsParameters::findLowerBound() const { +// return ! findUpperBound(); +// } + +// bool SimplexInferBoundsParameters::findUpperBound() const { +// return d_upperBound; +// } + +// void SimplexInferBoundsParameters::setThreshold(const DeltaRational& th){ +// d_threshold = th; +// d_useThreshold = true; +// } + +// bool SimplexInferBoundsParameters::useThreshold() const{ +// return d_useThreshold; +// } + +// const DeltaRational& SimplexInferBoundsParameters::getThreshold() const{ +// return d_threshold; +// } + +// SimplexInferBoundsParameters::SimplexInferBoundsParameters(int p, bool ub) +// : d_parameter(p) +// , d_upperBound(ub) +// , d_useThreshold(false) +// , d_threshold() +// {} + + +InferBoundsResult::InferBoundsResult() + : d_foundBound(false) + , d_budgetExhausted(false) + , d_boundIsProvenOpt(false) + , d_inconsistentState(false) + , d_reachedThreshold(false) + , d_value(false) + , d_term(Node::null()) + , d_upperBound(true) + , d_explanation(Node::null()) +{} + +InferBoundsResult::InferBoundsResult(Node term, bool ub) + : d_foundBound(false) + , d_budgetExhausted(false) + , d_boundIsProvenOpt(false) + , d_inconsistentState(false) + , d_reachedThreshold(false) + , d_value(false) + , d_term(term) + , d_upperBound(ub) + , d_explanation(Node::null()) +{} + +bool InferBoundsResult::foundBound() const { + return d_foundBound; +} +bool InferBoundsResult::boundIsOptimal() const { + return d_boundIsProvenOpt; +} +bool InferBoundsResult::inconsistentState() const { + return d_inconsistentState; +} + +bool InferBoundsResult::boundIsInteger() const{ + return foundBound() && d_value.isIntegral(); +} + +bool InferBoundsResult::boundIsRational() const { + return foundBound() && d_value.infinitesimalIsZero(); +} + +Integer InferBoundsResult::valueAsInteger() const{ + Assert(boundIsInteger()); + return getValue().floor(); +} +const Rational& InferBoundsResult::valueAsRational() const{ + Assert(boundIsRational()); + return getValue().getNoninfinitesimalPart(); +} + +const DeltaRational& InferBoundsResult::getValue() const{ + return d_value; +} + +Node InferBoundsResult::getTerm() const { return d_term; } + +Node InferBoundsResult::getLiteral() const{ + const Rational& q = getValue().getNoninfinitesimalPart(); + NodeManager* nm = NodeManager::currentNM(); + Node qnode = nm->mkConst(q); + + Kind k; + if(d_upperBound){ + // x <= q + c*delta + Assert(getValue().infinitesimalSgn() <= 0); + k = boundIsRational() ? kind::LEQ : kind::LT; + }else{ + // x >= q + c*delta + Assert(getValue().infinitesimalSgn() >= 0); + k = boundIsRational() ? kind::GEQ : kind::GT; + } + Node atom = nm->mkNode(k, getTerm(), qnode); + Node lit = Rewriter::rewrite(atom); + return lit; +} + +/* If there is a bound, this is a node that explains the bound. */ +Node InferBoundsResult::getExplanation() const{ + return d_explanation; +} + + +void InferBoundsResult::setBound(const DeltaRational& dr, Node exp){ + d_foundBound = true; + d_value = dr; + d_explanation = exp; +} + +//bool InferBoundsResult::foundBound() const { return d_foundBound; } +//bool InferBoundsResult::boundIsOptimal() const { return d_boundIsProvenOpt; } +//bool InferBoundsResult::inconsistentState() const { return d_inconsistentState; } + + +void InferBoundsResult::setBudgetExhausted() { d_budgetExhausted = true; } +void InferBoundsResult::setReachedThreshold() { d_reachedThreshold = true; } +void InferBoundsResult::setIsOptimal() { d_boundIsProvenOpt = true; } +void InferBoundsResult::setInconsistent() { d_inconsistentState = true; } + +bool InferBoundsResult::thresholdWasReached() const{ + return d_reachedThreshold; +} +bool InferBoundsResult::budgetIsExhausted() const{ + return d_budgetExhausted; +} + +std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr){ + os << "{InferBoundsResult " << std::endl; + os << "on " << ibr.getTerm() << ", "; + if(ibr.findUpperBound()){ + os << "find upper bound, "; + }else{ + os << "find lower bound, "; + } + if(ibr.foundBound()){ + os << "found a bound: "; + if(ibr.boundIsInteger()){ + os << ibr.valueAsInteger() << "(int), "; + }else if(ibr.boundIsRational()){ + os << ibr.valueAsRational() << "(rat), "; + }else{ + os << ibr.getValue() << "(extended), "; + } + + os << "as term " << ibr.getLiteral() << ", "; + os << "explanation " << ibr.getExplanation() << ", "; + }else { + os << "did not find a bound, "; + } + + if(ibr.boundIsOptimal()){ + os << "(opt), "; + } + + if(ibr.inconsistentState()){ + os << "(inconsistent), "; + } + if(ibr.budgetIsExhausted()){ + os << "(budget exhausted), "; + } + if(ibr.thresholdWasReached()){ + os << "(reached threshold), "; + } + os << "}"; + return os; +} + + +ArithEntailmentCheckSideEffects::ArithEntailmentCheckSideEffects() + : EntailmentCheckSideEffects(theory::THEORY_ARITH) + , d_simplexSideEffects (NULL) +{} + +ArithEntailmentCheckSideEffects::~ArithEntailmentCheckSideEffects(){ + if(d_simplexSideEffects != NULL){ + delete d_simplexSideEffects; + d_simplexSideEffects = NULL; + } +} + +InferBoundsResult& ArithEntailmentCheckSideEffects::getSimplexSideEffects(){ + if(d_simplexSideEffects == NULL){ + d_simplexSideEffects = new InferBoundsResult; + } + return *d_simplexSideEffects; +} + +namespace inferbounds { /* namespace arith */ + +std::ostream& operator<<(std::ostream& os, const Algorithms a){ + switch(a){ + case None: os << "AlgNone"; break; + case Lookup: os << "AlgLookup"; break; + case RowSum: os << "AlgRowSum"; break; + case Simplex: os << "AlgSimplex"; break; + default: + Unhandled(); + } + + return os; +} + +} /* namespace inferbounds */ + +} /* namespace arith */ +} /* namespace theory */ +} /* namespace CVC4 */ diff --git a/src/theory/arith/infer_bounds.h b/src/theory/arith/infer_bounds.h new file mode 100644 index 000000000..55486080a --- /dev/null +++ b/src/theory/arith/infer_bounds.h @@ -0,0 +1,161 @@ +/********************* */ +/*! \file infer_bounds.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "util/maybe.h" +#include "util/integer.h" +#include "util/rational.h" +#include "expr/node.h" +#include "theory/arith/delta_rational.h" +#include "theory/theory.h" +#include + +namespace CVC4 { +namespace theory { +namespace arith { + +namespace inferbounds { + enum Algorithms {None = 0, Lookup, RowSum, Simplex}; + enum SimplexParamKind { Unbounded, NumVars, Direct}; + +class InferBoundAlgorithm { +private: + Algorithms d_alg; + Maybe d_simplexRounds; + InferBoundAlgorithm(Algorithms a); + InferBoundAlgorithm(const Maybe& simplexRounds); + +public: + InferBoundAlgorithm(); + + Algorithms getAlgorithm() const; + const Maybe& getSimplexRounds() const; + + static InferBoundAlgorithm mkLookup(); + static InferBoundAlgorithm mkRowSum(); + static InferBoundAlgorithm mkSimplex(const Maybe& rounds); +}; + +std::ostream& operator<<(std::ostream& os, const Algorithms a); +} /* namespace inferbounds */ + +class ArithEntailmentCheckParameters : public EntailmentCheckParameters { +private: + typedef std::vector VecInferBoundAlg; + VecInferBoundAlg d_algorithms; + +public: + typedef VecInferBoundAlg::const_iterator const_iterator; + + ArithEntailmentCheckParameters(); + ~ArithEntailmentCheckParameters(); + + void addLookupRowSumAlgorithms(); + void addAlgorithm(const inferbounds::InferBoundAlgorithm& alg); + + const_iterator begin() const; + const_iterator end() const; +}; + + + +class InferBoundsResult { +public: + InferBoundsResult(); + InferBoundsResult(Node term, bool ub); + + void setBound(const DeltaRational& dr, Node exp); + bool foundBound() const; + + void setIsOptimal(); + bool boundIsOptimal() const; + + void setInconsistent(); + bool inconsistentState() const; + + const DeltaRational& getValue() const; + bool boundIsRational() const; + const Rational& valueAsRational() const; + bool boundIsInteger() const; + Integer valueAsInteger() const; + + Node getTerm() const; + Node getLiteral() const; + void setTerm(Node t){ d_term = t; } + + /* If there is a bound, this is a node that explains the bound. */ + Node getExplanation() const; + + bool budgetIsExhausted() const; + void setBudgetExhausted(); + + bool thresholdWasReached() const; + void setReachedThreshold(); + + bool findUpperBound() const { return d_upperBound; } + + void setFindLowerBound() { d_upperBound = false; } + void setFindUpperBound() { d_upperBound = true; } +private: + /* was a bound found */ + bool d_foundBound; + + /* was the budget exhausted */ + bool d_budgetExhausted; + + /* does the bound have to be optimal*/ + bool d_boundIsProvenOpt; + + /* was this started on an inconsistent state. */ + bool d_inconsistentState; + + /* reached the threshold. */ + bool d_reachedThreshold; + + /* the value of the bound */ + DeltaRational d_value; + + /* The input term. */ + Node d_term; + + /* Was the bound found an upper or lower bound.*/ + bool d_upperBound; + + /* Explanation of the bound. */ + Node d_explanation; +}; + +std::ostream& operator<<(std::ostream& os, const InferBoundsResult& ibr); + +class ArithEntailmentCheckSideEffects : public EntailmentCheckSideEffects{ +public: + ArithEntailmentCheckSideEffects(); + ~ArithEntailmentCheckSideEffects(); + + InferBoundsResult& getSimplexSideEffects(); + +private: + InferBoundsResult* d_simplexSideEffects; +}; + + +} /* namespace arith */ +} /* namespace theory */ +} /* namespace CVC4 */ diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 960a5a066..74453d985 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -17,6 +17,7 @@ #include "theory/arith/theory_arith.h" #include "theory/arith/theory_arith_private.h" +#include "theory/arith/infer_bounds.h" using namespace std; using namespace CVC4::kind; @@ -100,6 +101,43 @@ Node TheoryArith::getModelValue(TNode var) { return d_internal->getModelValue( var ); } + +std::pair TheoryArith::entailmentCheck (TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out) +{ + const ArithEntailmentCheckParameters* aparams = NULL; + if(params == NULL){ + ArithEntailmentCheckParameters* def = new ArithEntailmentCheckParameters(); + def->addLookupRowSumAlgorithms(); + aparams = def; + }else{ + AlwaysAssert(params->getTheoryId() == getId()); + aparams = dynamic_cast(params); + } + Assert(aparams != NULL); + + ArithEntailmentCheckSideEffects* ase = NULL; + if(out == NULL){ + ase = new ArithEntailmentCheckSideEffects(); + }else{ + AlwaysAssert(out->getTheoryId() == getId()); + ase = dynamic_cast(out); + } + Assert(ase != NULL); + + std::pair res = d_internal->entailmentCheck(lit, *aparams, *ase); + + if(params == NULL){ + delete aparams; + } + if(out == NULL){ + delete ase; + } + + return res; +} + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index eaa9a98c6..56a8d9b60 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -21,6 +21,7 @@ #include "expr/node.h" #include "theory/arith/theory_arith_private_forward.h" + namespace CVC4 { namespace theory { @@ -79,6 +80,12 @@ public: void addSharedTerm(TNode n); Node getModelValue(TNode var); + + + std::pair entailmentCheck(TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out); + };/* class TheoryArith */ }/* CVC4::theory::arith namespace */ diff --git a/src/theory/arith/theory_arith_private.cpp b/src/theory/arith/theory_arith_private.cpp index b0e66b564..efc93e26f 100644 --- a/src/theory/arith/theory_arith_private.cpp +++ b/src/theory/arith/theory_arith_private.cpp @@ -121,16 +121,21 @@ TheoryArithPrivate::TheoryArithPrivate(TheoryArith& containing, context::Context d_tableauResetDensity(1.6), d_tableauResetPeriod(10), d_conflicts(c), + d_blackBoxConflict(c, Node::null()), d_congruenceManager(c, d_constraintDatabase, SetupLiteralCallBack(*this), d_partialModel, RaiseConflict(*this, d_conflictBuffer)), d_cmEnabled(c, true), + d_dualSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), d_fcSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), d_soiSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), d_attemptSolSimplex(d_linEq, d_errorSet, RaiseConflict(*this, d_conflictBuffer), TempVarMalloc(*this)), + d_pass1SDP(NULL), d_otherSDP(NULL), d_lastContextIntegerAttempted(c,-1), + + d_DELTA_ZERO(0), d_approxCuts(c), d_fullCheckCounter(0), @@ -1822,10 +1827,6 @@ ConstraintP TheoryArithPrivate::constraintFromFactQueue(){ Assert(!done()); TNode assertion = get(); - if( options::finiteModelFind() && d_quantEngine && d_quantEngine->getBoundedIntegers() ){ - d_quantEngine->getBoundedIntegers()->assertNode(assertion); - } - Kind simpleKind = Comparison::comparisonKind(assertion); ConstraintP constraint = d_constraintDatabase.lookup(assertion); if(constraint == NullConstraint){ @@ -4621,6 +4622,7 @@ const BoundsInfo& TheoryArithPrivate::boundsInfo(ArithVar basic) const{ return d_rowTracking[ridx]; } + Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) { NodeManager* nm = NodeManager::currentNM(); @@ -4684,6 +4686,900 @@ Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) } + + +// InferBoundsResult TheoryArithPrivate::inferBound(TNode term, const InferBoundsParameters& param){ +// Node t = Rewriter::rewrite(term); +// Assert(Polynomial::isMember(t)); +// Polynomial p = Polynomial::parsePolynomial(t); +// if(p.containsConstant()){ +// Constant c = p.getHead().getConstant(); +// if(p.isConstant()){ +// InferBoundsResult res(t, param.findLowerBound()); +// res.setBound((DeltaRational)c.getValue(), mkBoolNode(true)); +// return res; +// }else{ +// Polynomial tail = p.getTail(); +// InferBoundsResult res = inferBound(tail.getNode(), param); +// if(res.foundBound()){ +// DeltaRational newBound = res.getValue() + c.getValue(); +// if(tail.isIntegral()){ +// Integer asInt = (param.findLowerBound()) ? newBound.ceiling() : newBound.floor(); +// newBound = DeltaRational(asInt); +// } +// res.setBound(newBound, res.getExplanation()); +// } +// return res; +// } +// }else if(param.findLowerBound()){ +// InferBoundsParameters find_ub = param; +// find_ub.setFindUpperBound(); +// if(param.useThreshold()){ +// find_ub.setThreshold(- param.getThreshold() ); +// } +// Polynomial negP = -p; +// InferBoundsResult res = inferBound(negP.getNode(), find_ub); +// res.setFindLowerBound(); +// if(res.foundBound()){ +// res.setTerm(p.getNode()); +// res.setBound(-res.getValue(), res.getExplanation()); +// } +// return res; +// }else{ +// Assert(param.findUpperBound()); +// // does not contain a constant +// switch(param.getEffort()){ +// case InferBoundsParameters::Lookup: +// return inferUpperBoundLookup(t, param); +// case InferBoundsParameters::Simplex: +// return inferUpperBoundSimplex(t, param); +// case InferBoundsParameters::LookupAndSimplexOnFailure: +// case InferBoundsParameters::TryBoth: +// { +// InferBoundsResult lookup = inferUpperBoundLookup(t, param); +// if(lookup.foundBound()){ +// if(param.getEffort() == InferBoundsParameters::LookupAndSimplexOnFailure || +// lookup.boundIsOptimal()){ +// return lookup; +// } +// } +// InferBoundsResult simplex = inferUpperBoundSimplex(t, param); +// if(lookup.foundBound() && simplex.foundBound()){ +// return (lookup.getValue() <= simplex.getValue()) ? lookup : simplex; +// }else if(lookup.foundBound()){ +// return lookup; +// }else{ +// return simplex; +// } +// } +// default: +// Unreachable(); +// return InferBoundsResult(); +// } +// } +// } + + +std::pair TheoryArithPrivate::entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ + using namespace inferbounds; + + // l k r + // diff : (l - r) k 0 + Debug("arith::entailCheck") << "TheoryArithPrivate::entailmentCheck(" << lit << ")"<< endl; + Kind k; + int primDir; + Rational lm, rm, dm; + Node lp, rp, dp; + DeltaRational sep; + bool successful = decomposeLiteral(lit, k, primDir, lm, lp, rm, rp, dm, dp, sep); + if(!successful) { return make_pair(false, Node::null()); } + + if(dp.getKind() == CONST_RATIONAL){ + Node eval = Rewriter::rewrite(lit); + Assert(eval.getKind() == kind::CONST_BOOLEAN); + // if true, true is an acceptable explaination + // if false, the node is uninterpreted and eval can be forgotten + return make_pair(eval.getConst(), eval); + } + Assert(dm != Rational(0)); + Assert(primDir == 1 || primDir == -1); + + int negPrim = -primDir; + + int secDir = (k == EQUAL || k == DISTINCT) ? negPrim: 0; + int negSecDir = (k == EQUAL || k == DISTINCT) ? primDir: 0; + + // primDir*[lm*( lp )] k primDir*[ [rm*( rp )] + sep ] + // primDir*[lm*( lp ) - rm*( rp ) ] k primDir*sep + // primDir*[dm * dp] k primDir*sep + + std::pair bestPrimLeft, bestNegPrimRight, bestPrimDiff, tmp; + std::pair bestSecLeft, bestNegSecRight, bestSecDiff; + bestPrimLeft.first = Node::null(); bestNegPrimRight.first = Node::null(); bestPrimDiff.first = Node::null(); + bestSecLeft.first = Node::null(); bestNegSecRight.first = Node::null(); bestSecDiff.first = Node::null(); + + + + ArithEntailmentCheckParameters::const_iterator alg, alg_end; + for( alg = params.begin(), alg_end = params.end(); alg != alg_end; ++alg ){ + const inferbounds::InferBoundAlgorithm& ibalg = *alg; + + Debug("arith::entailCheck") << "entailmentCheck trying " << (inferbounds::Algorithms) ibalg.getAlgorithm() << endl; + switch(ibalg.getAlgorithm()){ + case inferbounds::None: + break; + case inferbounds::Lookup: + case inferbounds::RowSum: + { + typedef void (TheoryArithPrivate::*EntailmentCheckFunc)(std::pair&, int, TNode) const; + + EntailmentCheckFunc ecfunc = + (ibalg.getAlgorithm() == inferbounds::Lookup) + ? (&TheoryArithPrivate::entailmentCheckBoundLookup) + : (&TheoryArithPrivate::entailmentCheckRowSum); + + (*this.*ecfunc)(tmp, primDir * lm.sgn(), lp); + setToMin(primDir * lm.sgn(), bestPrimLeft, tmp); + + (*this.*ecfunc)(tmp, negPrim * rm.sgn(), rp); + setToMin(negPrim * rm.sgn(), bestNegPrimRight, tmp); + + (*this.*ecfunc)(tmp, secDir * lm.sgn(), lp); + setToMin(secDir * lm.sgn(), bestSecLeft, tmp); + + (*this.*ecfunc)(tmp, negSecDir * rm.sgn(), rp); + setToMin(negSecDir * rm.sgn(), bestNegSecRight, tmp); + + (*this.*ecfunc)(tmp, primDir * dm.sgn(), dp); + setToMin(primDir * dm.sgn(), bestPrimDiff, tmp); + + (*this.*ecfunc)(tmp, secDir * dm.sgn(), dp); + setToMin(secDir * dm.sgn(), bestSecDiff, tmp); + } + break; + case inferbounds::Simplex: + { + // primDir * diffm * diff < c or primDir * diffm * diff > c + tmp = entailmentCheckSimplex(primDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); + setToMin(primDir * dm.sgn(), bestPrimDiff, tmp); + + tmp = entailmentCheckSimplex(secDir * dm.sgn(), dp, ibalg, out.getSimplexSideEffects()); + setToMin(secDir * dm.sgn(), bestSecDiff, tmp); + } + break; + default: + Unhandled(); + } + + // turn bounds on prim * left and -prim * right into bounds on prim * diff + if(!bestPrimLeft.first.isNull() && !bestNegPrimRight.first.isNull()){ + // primDir*lm* lp <= primDir*lm*L + // -primDir*rm* rp <= -primDir*rm*R + // primDir*lm* lp -primDir*rm* rp <= primDir*lm*L - primDir*rm*R + // primDir [lm* lp -rm* rp] <= primDir[lm*L - *rm*R] + // primDir [dm * dp] <= primDir[lm*L - *rm*R] + // primDir [dm * dp] <= primDir * dm * ([lm*L - *rm*R]/dm) + tmp.second = ((bestPrimLeft.second * lm) - (bestNegPrimRight.second * rm)) / dm; + tmp.first = (bestPrimLeft.first).andNode(bestNegPrimRight.first); + setToMin(primDir, bestPrimDiff, tmp); + } + + // turn bounds on sec * left and sec * right into bounds on sec * diff + if(secDir != 0 && !bestSecLeft.first.isNull() && !bestNegSecRight.first.isNull()){ + // secDir*lm* lp <= secDir*lm*L + // -secDir*rm* rp <= -secDir*rm*R + // secDir*lm* lp -secDir*rm* rp <= secDir*lm*L - secDir*rm*R + // secDir [lm* lp -rm* rp] <= secDir[lm*L - *rm*R] + // secDir [dm * dp] <= secDir[lm*L - *rm*R] + // secDir [dm * dp] <= secDir * dm * ([lm*L - *rm*R]/dm) + tmp.second = ((bestSecLeft.second * lm) - (bestNegSecRight.second * rm)) / dm; + tmp.first = (bestSecLeft.first).andNode(bestNegSecRight.first); + setToMin(secDir, bestSecDiff, tmp); + } + + switch(k){ + case LEQ: + if(!bestPrimDiff.first.isNull()){ + DeltaRational d = (bestPrimDiff.second * dm); + if((primDir > 0 && d <= sep) || (primDir < 0 && d >= sep) ){ + Debug("arith::entailCheck") << "entailmentCheck found " + << primDir << "*" << dm << "*(" << dp<<")" + << " <= " << primDir << "*" << dm << "*" << bestPrimDiff.second + << " <= " << primDir << "*" << sep << endl + << " by " << bestPrimDiff.first << endl; + Assert(bestPrimDiff.second * (Rational(primDir)* dm) <= (sep * Rational(primDir))); + return make_pair(true, bestPrimDiff.first); + } + } + break; + case EQUAL: + if(!bestPrimDiff.first.isNull() && !bestSecDiff.first.isNull()){ + // Is primDir [dm * dp] == primDir * sep entailed? + // Iff [dm * dp] == sep entailed? + // Iff dp == sep / dm entailed? + // Iff dp <= sep / dm and dp >= sep / dm entailed? + + // primDir [dm * dp] <= primDir * dm * U + // secDir [dm * dp] <= secDir * dm * L + + // Suppose primDir * dm > 0 + // then secDir * dm < 0 + // dp >= (secDir * L) / secDir * dm + // dp >= (primDir * L) / primDir * dm + // + // dp <= U / dm + // dp >= L / dm + // dp == sep / dm entailed iff U == L == sep + // Suppose primDir * dm < 0 + // then secDir * dm > 0 + // dp >= U / dm + // dp <= L / dm + // dp == sep / dm entailed iff U == L == sep + if(bestPrimDiff.second == bestSecDiff.second){ + if(bestPrimDiff.second == sep){ + return make_pair(true, (bestPrimDiff.first).andNode(bestSecDiff.first)); + } + } + } + // intentionally fall through to DISTINCT case! + // entailments of negations are eager exit cases for EQUAL + case DISTINCT: + if(!bestPrimDiff.first.isNull()){ + // primDir [dm * dp] <= primDir * dm * U < primDir * sep + if((primDir > 0 && (bestPrimDiff.second * dm < sep)) || + (primDir < 0 && (bestPrimDiff.second * dm > sep))){ + // entailment of negation + if(k == DISTINCT){ + return make_pair(true, bestPrimDiff.first); + }else{ + Assert(k == EQUAL); + return make_pair(false, Node::null()); + } + } + } + if(!bestSecDiff.first.isNull()){ + // If primDir [dm * dp] > primDir * sep, then this is not entailed. + // If primDir [dm * dp] >= primDir * dm * L > primDir * sep + // -primDir * dm * L < -primDir * sep + // secDir * dm * L < secDir * sep + if((secDir > 0 && (bestSecDiff.second * dm < sep)) || + (secDir < 0 && (bestSecDiff.second * dm > sep))){ + if(k == DISTINCT){ + return make_pair(true, bestSecDiff.first); + }else{ + Assert(k == EQUAL); + return make_pair(false, Node::null()); + } + } + } + + break; + default: + Unreachable(); + break; + } + } + return make_pair(false, Node::null()); +} + +bool TheoryArithPrivate::decomposeTerm(Node term, Rational& m, Node& p, Rational& c){ + Node t = Rewriter::rewrite(term); + if(!Polynomial::isMember(t)){ + return false; + } +#warning "DO NOT LET INTO TRUNK!" + ContainsTermITEVisitor ctv; + if(ctv.containsTermITE(t)){ + return false; + } + + Polynomial poly = Polynomial::parsePolynomial(t); + if(poly.isConstant()){ + c = poly.getHead().getConstant().getValue(); + p = mkRationalNode(Rational(0)); + m = Rational(1); + return true; + }else if(poly.containsConstant()){ + c = poly.getHead().getConstant().getValue(); + poly = poly.getTail(); + }else{ + c = Rational(0); + } + Assert(!poly.isConstant()); + Assert(!poly.containsConstant()); + + const bool intVars = poly.allIntegralVariables(); + + if(intVars){ + m = Rational(1); + if(!poly.isIntegral()){ + Integer denom = poly.denominatorLCM(); + m /= denom; + poly = poly * denom; + } + Integer g = poly.gcd(); + m *= g; + poly = poly * Rational(1,g); + Assert(poly.isIntegral()); + Assert(poly.leadingCoefficientIsPositive()); + }else{ + Assert(!intVars); + m = poly.getHead().getConstant().getValue(); + poly = poly * m.inverse(); + Assert(poly.leadingCoefficientIsAbsOne()); + } + p = poly.getNode(); + return true; +} + +void TheoryArithPrivate::setToMin(int sgn, std::pair& min, const std::pair& e){ + if(sgn != 0){ + if(min.first.isNull() && !e.first.isNull()){ + min = e; + }else if(!min.first.isNull() && !e.first.isNull()){ + if(sgn > 0 && min.second > e.second){ + min = e; + }else if(sgn < 0 && min.second < e.second){ + min = e; + } + } + } +} + +// std::pair TheoryArithPrivate::entailmentUpperCheck(const Rational& lm, Node lp, const Rational& rm, Node rp, const DeltaRational& sep, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out){ + +// Rational negRM = -rm; +// Node diff = NodeManager::currentNM()->mkNode(MULT, mkRationalConstan(lm), lp) + (negRM * rp); + +// Rational diffm; +// Node diffp; +// decompose(diff, diffm, diffNode); + + +// std::pair bestUbLeft, bestLbRight, bestUbDiff, tmp; +// bestUbLeft = bestLbRight = bestUbDiff = make_pair(Node::Null(), DeltaRational()); + +// return make_pair(false, Node::null()); +// } + +/** + * Decomposes a literal into the form: + * dir*[lm*( lp )] k dir*[ [rm*( rp )] + sep ] + * dir*[dm* dp] k dir *sep + * dir is either 1 or -1 + */ +bool TheoryArithPrivate::decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm, Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep){ + bool negated = (lit.getKind() == kind::NOT); + TNode atom = negated ? lit[0] : lit; + + TNode left = atom[0]; + TNode right = atom[1]; + + // left : lm*( lp ) + lc + // right: rm*( rp ) + rc + Rational lc, rc; + bool success = decomposeTerm(left, lm, lp, lc); + if(!success){ return false; } + success = decomposeTerm(right, rm, rp, rc); + if(!success){ return false; } + + Node diff = Rewriter::rewrite(NodeManager::currentNM()->mkNode(kind::MINUS, left, right)); + Rational dc; + success = decomposeTerm(diff, dm, dp, dc); + Assert(success); + + // reduce the kind of the to not include literals + // GT, NOT LEQ + // GEQ, NOT LT + // LT, NOT GEQ + // LEQ, NOT LT + Kind atomKind = atom.getKind(); + Kind normKind = negated ? negateKind(atomKind) : atomKind; + + if(normKind == GEQ || normKind == GT){ + dir = -1; + normKind = (normKind == GEQ) ? LEQ : LT; + }else{ + dir = 1; + } + + Debug("arith::decomp") << "arith::decomp " + << lit << "(" << normKind << "*" << dir << ")"<< endl + << " left:" << lc << " + " << lm << "*(" << lp << ") : " <& tmp, int sgn, TNode tp) const { + tmp.first = Node::null(); + if(sgn == 0){ return; } + + Assert(Polynomial::isMember(tp)); + if(tp.getKind() == CONST_RATIONAL){ + tmp.first = mkBoolNode(true); + tmp.second = DeltaRational(tp.getConst()); + }else if(d_partialModel.hasArithVar(tp)){ + Assert(tp.getKind() != CONST_RATIONAL); + ArithVar v = d_partialModel.asArithVar(tp); + Assert(v != ARITHVAR_SENTINEL); + ConstraintP c = (sgn > 0) + ? d_partialModel.getUpperBoundConstraint(v) + : d_partialModel.getLowerBoundConstraint(v); + if(c != NullConstraint){ + tmp.first = c->externalExplainByAssertions(); + tmp.second = c->getValue(); + } + } +} + +void TheoryArithPrivate::entailmentCheckRowSum(std::pair& tmp, int sgn, TNode tp) const { + tmp.first = Node::null(); + if(sgn == 0){ return; } + if(tp.getKind() != PLUS){ return; } + Assert(Polynomial::isMember(tp)); + + tmp.second = DeltaRational(0); + NodeBuilder<> nb(kind::AND); + + Polynomial p = Polynomial::parsePolynomial(tp); + for(Polynomial::iterator i = p.begin(), iend = p.end(); i != iend; ++i) { + Monomial m = *i; + Node x = m.getVarList().getNode(); + if(d_partialModel.hasArithVar(x)){ + ArithVar v = d_partialModel.asArithVar(x); + const Rational& coeff = m.getConstant().getValue(); + int dir = sgn * coeff.sgn(); + ConstraintP c = (dir > 0) + ? d_partialModel.getUpperBoundConstraint(v) + : d_partialModel.getLowerBoundConstraint(v); + if(c != NullConstraint){ + tmp.second += c->getValue() * coeff; + c->externalExplainByAssertions(nb); + }else{ + //failed + return; + } + }else{ + // failed + return; + } + } + // success + tmp.first = nb; +} + +std::pair TheoryArithPrivate::entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& param, InferBoundsResult& result){ + + if((sgn == 0) || !(d_qflraStatus == Result::SAT && d_errorSet.noSignals()) || tp.getKind() == CONST_RATIONAL){ + return make_pair(Node::null(), DeltaRational()); + } + + Assert(d_qflraStatus == Result::SAT); + Assert(d_errorSet.noSignals()); + Assert(param.getAlgorithm() == inferbounds::Simplex); + + // TODO Move me into a new file + + enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; + ResultState finalState = Unset; + + int maxRounds = param.getSimplexRounds().just() + ? param.getSimplexRounds().constValue() + : -1; + + Maybe threshold; + // TODO: get this from the parameters + + // setup term + Polynomial p = Polynomial::parsePolynomial(tp); + vector variables; + vector coefficients; + asVectors(p, coefficients, variables); + if(sgn < 0){ + for(size_t i=0, N=coefficients.size(); i < N; ++i){ + coefficients[i] = -coefficients[i]; + } + } + // implicitly an upperbound + Node skolem = mkRealSkolem("tmpVar$$"); + ArithVar optVar = requestArithVar(skolem, false, true); + d_tableau.addRow(optVar, coefficients, variables); + RowIndex ridx = d_tableau.basicToRowIndex(optVar); + + DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); + d_partialModel.setAssignment(optVar, newAssignment); + d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); + + // Setup simplex + d_partialModel.stopQueueingBoundCounts(); + UpdateTrackingCallback utcb(&d_linEq); + d_partialModel.processBoundsQueue(utcb); + d_linEq.startTrackingBoundCounts(); + + // maximize optVar via primal Simplex + int rounds = 0; + while(finalState == Unset){ + ++rounds; + if(maxRounds >= 0 && rounds > maxRounds){ + finalState = ExhaustedRounds; + break; + } + + // select entering by bland's rule + // TODO improve upon bland's + ArithVar entering = ARITHVAR_SENTINEL; + const Tableau::Entry* enteringEntry = NULL; + for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ + const Tableau::Entry& entry = *ri; + ArithVar v = entry.getColVar(); + if(v != optVar){ + int sgn = entry.getCoefficient().sgn(); + Assert(sgn != 0); + bool candidate = (sgn > 0) + ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) + : (d_partialModel.cmpAssignmentLowerBound(v) != 0); + if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ + entering = v; + enteringEntry = &entry; + } + } + } + if(entering == ARITHVAR_SENTINEL){ + finalState = Inferred; + break; + } + Assert(entering != ARITHVAR_SENTINEL); + Assert(enteringEntry != NULL); + + int esgn = enteringEntry->getCoefficient().sgn(); + Assert(esgn != 0); + + // select leaving and ratio + ArithVar leaving = ARITHVAR_SENTINEL; + DeltaRational minRatio; + const Tableau::Entry* pivotEntry = NULL; + + // Special case check the upper/lowerbound on entering + ConstraintP cOnEntering = (esgn > 0) + ? d_partialModel.getUpperBoundConstraint(entering) + : d_partialModel.getLowerBoundConstraint(entering); + if(cOnEntering != NullConstraint){ + leaving = entering; + minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); + } + for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ + const Tableau::Entry& centry = *ci; + ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); + int csgn = centry.getCoefficient().sgn(); + int basicDir = csgn * esgn; + + ConstraintP bound = (basicDir > 0) + ? d_partialModel.getUpperBoundConstraint(basic) + : d_partialModel.getLowerBoundConstraint(basic); + if(bound != NullConstraint){ + DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); + DeltaRational ratio = diff/(centry.getCoefficient()); + bool selected = false; + if(leaving == ARITHVAR_SENTINEL){ + selected = true; + }else{ + int cmp = ratio.compare(minRatio); + if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ + selected = (cmp != 0) || + ((leaving != entering) && (basic < leaving)); + } + } + if(selected){ + leaving = basic; + minRatio = ratio; + pivotEntry = ¢ry; + } + } + } + + + if(leaving == ARITHVAR_SENTINEL){ + finalState = NoBound; + break; + }else if(leaving == entering){ + d_linEq.update(entering, minRatio); + }else{ + DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); + d_linEq.pivotAndUpdate(leaving, entering, newLeaving); + // no conflicts clear signals + Assert(d_errorSet.noSignals()); + } + + if(threshold.just()){ + if(d_partialModel.getAssignment(optVar) >= threshold.constValue()){ + finalState = ReachedThreshold; + break; + } + } + }; + + result = InferBoundsResult(tp, sgn > 0); + + // tear down term + switch(finalState){ + case Inferred: + { + NodeBuilder<> nb(kind::AND); + for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ + const Tableau::Entry& e =*ri; + ArithVar colVar = e.getColVar(); + if(colVar != optVar){ + const Rational& q = e.getCoefficient(); + Assert(q.sgn() != 0); + ConstraintP c = (q.sgn() > 0) + ? d_partialModel.getUpperBoundConstraint(colVar) + : d_partialModel.getLowerBoundConstraint(colVar); + c->externalExplainByAssertions(nb); + } + } + Assert(nb.getNumChildren() >= 1); + Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; + result.setBound(d_partialModel.getAssignment(optVar), exp); + result.setIsOptimal(); + break; + } + case NoBound: + break; + case ReachedThreshold: + result.setReachedThreshold(); + break; + case ExhaustedRounds: + result.setBudgetExhausted(); + break; + case Unset: + default: + Unreachable(); + break; + }; + + d_linEq.stopTrackingRowIndex(ridx); + d_tableau.removeBasicRow(optVar); + releaseArithVar(optVar); + + d_linEq.stopTrackingBoundCounts(); + d_partialModel.startQueueingBoundCounts(); + + if(result.foundBound()){ + return make_pair(result.getExplanation(), result.getValue()); + }else{ + return make_pair(Node::null(), DeltaRational()); + } +} + +// InferBoundsResult TheoryArithPrivate::inferUpperBoundSimplex(TNode t, const inferbounds::InferBoundAlgorithm& param){ +// Assert(param.findUpperBound()); + +// if(!(d_qflraStatus == Result::SAT && d_errorSet.noSignals())){ +// InferBoundsResult inconsistent; +// inconsistent.setInconsistent(); +// return inconsistent; +// } + +// Assert(d_qflraStatus == Result::SAT); +// Assert(d_errorSet.noSignals()); + +// // TODO Move me into a new file + +// enum ResultState {Unset, Inferred, NoBound, ReachedThreshold, ExhaustedRounds}; +// ResultState finalState = Unset; + +// int maxRounds = 0; +// switch(param.getParamKind()){ +// case InferBoundsParameters::Unbounded: +// maxRounds = -1; +// break; +// case InferBoundsParameters::NumVars: +// maxRounds = d_partialModel.getNumberOfVariables() * param.getSimplexRoundParameter(); +// break; +// case InferBoundsParameters::Direct: +// maxRounds = param.getSimplexRoundParameter(); +// break; +// default: maxRounds = 0; break; +// } + +// // setup term +// Polynomial p = Polynomial::parsePolynomial(t); +// vector variables; +// vector coefficients; +// asVectors(p, coefficients, variables); + +// Node skolem = mkRealSkolem("tmpVar$$"); +// ArithVar optVar = requestArithVar(skolem, false, true); +// d_tableau.addRow(optVar, coefficients, variables); +// RowIndex ridx = d_tableau.basicToRowIndex(optVar); + +// DeltaRational newAssignment = d_linEq.computeRowValue(optVar, false); +// d_partialModel.setAssignment(optVar, newAssignment); +// d_linEq.trackRowIndex(d_tableau.basicToRowIndex(optVar)); + +// // Setup simplex +// d_partialModel.stopQueueingBoundCounts(); +// UpdateTrackingCallback utcb(&d_linEq); +// d_partialModel.processBoundsQueue(utcb); +// d_linEq.startTrackingBoundCounts(); + +// // maximize optVar via primal Simplex +// int rounds = 0; +// while(finalState == Unset){ +// ++rounds; +// if(maxRounds >= 0 && rounds > maxRounds){ +// finalState = ExhaustedRounds; +// break; +// } + +// // select entering by bland's rule +// // TODO improve upon bland's +// ArithVar entering = ARITHVAR_SENTINEL; +// const Tableau::Entry* enteringEntry = NULL; +// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ +// const Tableau::Entry& entry = *ri; +// ArithVar v = entry.getColVar(); +// if(v != optVar){ +// int sgn = entry.getCoefficient().sgn(); +// Assert(sgn != 0); +// bool candidate = (sgn > 0) +// ? (d_partialModel.cmpAssignmentUpperBound(v) != 0) +// : (d_partialModel.cmpAssignmentLowerBound(v) != 0); +// if(candidate && (entering == ARITHVAR_SENTINEL || entering > v)){ +// entering = v; +// enteringEntry = &entry; +// } +// } +// } +// if(entering == ARITHVAR_SENTINEL){ +// finalState = Inferred; +// break; +// } +// Assert(entering != ARITHVAR_SENTINEL); +// Assert(enteringEntry != NULL); + +// int esgn = enteringEntry->getCoefficient().sgn(); +// Assert(esgn != 0); + +// // select leaving and ratio +// ArithVar leaving = ARITHVAR_SENTINEL; +// DeltaRational minRatio; +// const Tableau::Entry* pivotEntry = NULL; + +// // Special case check the upper/lowerbound on entering +// ConstraintP cOnEntering = (esgn > 0) +// ? d_partialModel.getUpperBoundConstraint(entering) +// : d_partialModel.getLowerBoundConstraint(entering); +// if(cOnEntering != NullConstraint){ +// leaving = entering; +// minRatio = d_partialModel.getAssignment(entering) - cOnEntering->getValue(); +// } +// for(Tableau::ColIterator ci = d_tableau.colIterator(entering); !ci.atEnd(); ++ci){ +// const Tableau::Entry& centry = *ci; +// ArithVar basic = d_tableau.rowIndexToBasic(centry.getRowIndex()); +// int csgn = centry.getCoefficient().sgn(); +// int basicDir = csgn * esgn; + +// ConstraintP bound = (basicDir > 0) +// ? d_partialModel.getUpperBoundConstraint(basic) +// : d_partialModel.getLowerBoundConstraint(basic); +// if(bound != NullConstraint){ +// DeltaRational diff = d_partialModel.getAssignment(basic) - bound->getValue(); +// DeltaRational ratio = diff/(centry.getCoefficient()); +// bool selected = false; +// if(leaving == ARITHVAR_SENTINEL){ +// selected = true; +// }else{ +// int cmp = ratio.compare(minRatio); +// if((csgn > 0) ? (cmp <= 0) : (cmp >= 0)){ +// selected = (cmp != 0) || +// ((leaving != entering) && (basic < leaving)); +// } +// } +// if(selected){ +// leaving = basic; +// minRatio = ratio; +// pivotEntry = ¢ry; +// } +// } +// } + + +// if(leaving == ARITHVAR_SENTINEL){ +// finalState = NoBound; +// break; +// }else if(leaving == entering){ +// d_linEq.update(entering, minRatio); +// }else{ +// DeltaRational newLeaving = minRatio * (pivotEntry->getCoefficient()); +// d_linEq.pivotAndUpdate(leaving, entering, newLeaving); +// // no conflicts clear signals +// Assert(d_errorSet.noSignals()); +// } + +// if(param.useThreshold()){ +// if(d_partialModel.getAssignment(optVar) >= param.getThreshold()){ +// finalState = ReachedThreshold; +// break; +// } +// } +// }; + +// InferBoundsResult result(t, param.findUpperBound()); + +// // tear down term +// switch(finalState){ +// case Inferred: +// { +// NodeBuilder<> nb(kind::AND); +// for(Tableau::RowIterator ri = d_tableau.ridRowIterator(ridx); !ri.atEnd(); ++ri){ +// const Tableau::Entry& e =*ri; +// ArithVar colVar = e.getColVar(); +// if(colVar != optVar){ +// const Rational& q = e.getCoefficient(); +// Assert(q.sgn() != 0); +// ConstraintP c = (q.sgn() > 0) +// ? d_partialModel.getUpperBoundConstraint(colVar) +// : d_partialModel.getLowerBoundConstraint(colVar); +// c->externalExplainByAssertions(nb); +// } +// } +// Assert(nb.getNumChildren() >= 1); +// Node exp = (nb.getNumChildren() >= 2) ? (Node) nb : nb[0]; +// result.setBound(d_partialModel.getAssignment(optVar), exp); +// result.setIsOptimal(); +// break; +// } +// case NoBound: +// break; +// case ReachedThreshold: +// result.setReachedThreshold(); +// break; +// case ExhaustedRounds: +// result.setBudgetExhausted(); +// break; +// case Unset: +// default: +// Unreachable(); +// break; +// }; + +// d_linEq.stopTrackingRowIndex(ridx); +// d_tableau.removeBasicRow(optVar); +// releaseArithVar(optVar); + +// d_linEq.stopTrackingBoundCounts(); +// d_partialModel.startQueueingBoundCounts(); + +// return result; +// } + }/* CVC4::theory::arith namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/arith/theory_arith_private.h b/src/theory/arith/theory_arith_private.h index 68e839ef8..5e7943e5e 100644 --- a/src/theory/arith/theory_arith_private.h +++ b/src/theory/arith/theory_arith_private.h @@ -64,6 +64,7 @@ #include "theory/arith/arith_utilities.h" #include "theory/arith/delta_rational.h" +#include "theory/arith/infer_bounds.h" #include "theory/arith/partial_model.h" #include "theory/arith/matrix.h" @@ -92,6 +93,13 @@ class BranchCutInfo; class TreeLog; class ApproximateStatistics; +class ArithEntailmentCheckParameters; +class ArithEntailmentCheckSideEffects; +namespace inferbounds { + class InferBoundAlgorithm; +} +class InferBoundsResult; + /** * Implementation of QF_LRA. * Based upon: @@ -146,7 +154,42 @@ public: void releaseArithVar(ArithVar v); void signal(ArithVar v){ d_errorSet.signalVariable(v); } + private: + // t does not contain constants + void entailmentCheckBoundLookup(std::pair& tmp, int sgn, TNode tp) const; + void entailmentCheckRowSum(std::pair& tmp, int sgn, TNode tp) const; + + std::pair entailmentCheckSimplex(int sgn, TNode tp, const inferbounds::InferBoundAlgorithm& p, InferBoundsResult& out); + + //InferBoundsResult inferBound(TNode term, const InferBoundsParameters& p); + //InferBoundsResult inferUpperBoundLookup(TNode t, const InferBoundsParameters& p); + //InferBoundsResult inferUpperBoundSimplex(TNode t, const SimplexInferBoundsParameters& p); + + /** + * Infers either a new upper/lower bound on term in the real relaxation. + * Either: + * - term is malformed (see below) + * - a maximum/minimum is found with the result being a pair + * -- where + * -- term dr is implies by exp + * -- is <= if inferring an upper bound, >= otherwise + * -- exp is in terms of the assertions to the theory. + * - No upper or lower bound is inferrable in the real relaxation. + * -- Returns <0, Null()> + * - the maximum number of rounds was exhausted: + * -- Returns where v is the current feasible value of term + * - Threshold reached: + * -- If theshold != NULL, and a feasible value is found to exceed threshold + * -- Simplex stops and returns + */ + //std::pair inferBound(TNode term, bool lb, int maxRounds = -1, const DeltaRational* threshold = NULL); + +private: + static bool decomposeTerm(Node term, Rational& m, Node& p, Rational& c); + static bool decomposeLiteral(Node lit, Kind& k, int& dir, Rational& lm, Node& lp, Rational& rm, Node& rp, Rational& dm, Node& dp, DeltaRational& sep); + static void setToMin(int sgn, std::pair& min, const std::pair& e); + /** * The map between arith variables to nodes. */ @@ -427,6 +470,10 @@ public: Node getModelValue(TNode var); + + std::pair entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out); + + private: /** The constant zero. */ diff --git a/src/theory/quantifiers/instantiation_engine.cpp b/src/theory/quantifiers/instantiation_engine.cpp index c8a08dad9..06858cf92 100644 --- a/src/theory/quantifiers/instantiation_engine.cpp +++ b/src/theory/quantifiers/instantiation_engine.cpp @@ -208,6 +208,7 @@ void InstantiationEngine::check( Theory::Effort e ){ clSet = double(clock())/double(CLOCKS_PER_SEC); Trace("inst-engine") << "---Instantiation Engine Round, effort = " << e << "---" << std::endl; } + ++(d_statistics.d_instantiation_rounds); bool quantActive = false; Debug("quantifiers") << "quantifiers: check: asserted quantifiers size" << d_quantEngine->getModel()->getNumAssertedQuantifiers() << std::endl; @@ -438,7 +439,8 @@ InstantiationEngine::Statistics::Statistics(): d_instantiations_guess("InstantiationEngine::Instantiations_Guess", 0), d_instantiations_cbqi_arith("InstantiationEngine::Instantiations_Cbqi_Arith", 0), d_instantiations_cbqi_arith_minus("InstantiationEngine::Instantiations_Cbqi_Arith_Minus", 0), - d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0) + d_instantiations_cbqi_datatypes("InstantiationEngine::Instantiations_Cbqi_Datatypes", 0), + d_instantiation_rounds("InstantiationEngine::Rounds", 0 ) { StatisticsRegistry::registerStat(&d_instantiations_user_patterns); StatisticsRegistry::registerStat(&d_instantiations_auto_gen); @@ -447,6 +449,7 @@ InstantiationEngine::Statistics::Statistics(): StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith); StatisticsRegistry::registerStat(&d_instantiations_cbqi_arith_minus); StatisticsRegistry::registerStat(&d_instantiations_cbqi_datatypes); + StatisticsRegistry::registerStat(&d_instantiation_rounds); } InstantiationEngine::Statistics::~Statistics(){ @@ -457,4 +460,5 @@ InstantiationEngine::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith); StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus); StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes); + StatisticsRegistry::unregisterStat(&d_instantiation_rounds); } diff --git a/src/theory/quantifiers/instantiation_engine.h b/src/theory/quantifiers/instantiation_engine.h index 53777d362..a460f1164 100644 --- a/src/theory/quantifiers/instantiation_engine.h +++ b/src/theory/quantifiers/instantiation_engine.h @@ -149,6 +149,7 @@ public: IntStat d_instantiations_cbqi_arith; IntStat d_instantiations_cbqi_arith_minus; IntStat d_instantiations_cbqi_datatypes; + IntStat d_instantiation_rounds; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index e733764f0..f4acfb926 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -126,6 +126,8 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default what effort to apply conflict find mechanism option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" when to invoke conflict find mechanism for quantifiers +option qcfTConstraint --qcf-tconstraint bool :read-write :default false + enable entailment checks for t-constraints in qcf algorithm option quantRewriteRules --rewrite-rules bool :default true use rewrite rules module diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index e27d438be..2f399be33 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -91,24 +91,44 @@ void QuantInfo::initialize( Node q, Node qn ) { d_mg = new MatchGen( this, qn ); if( d_mg->isValid() ){ - for( unsigned j=q[0].getNumChildren(); jisValid() ){ - d_mg->setInvalid(); - break; - }else{ - std::vector< int > bvars; - d_var_mg[j]->determineVariableOrder( this, bvars ); - } + /* + for( unsigned j=0; jsetInvalid(); + break; } } - + */ if( d_mg->isValid() ){ - std::vector< int > bvars; - d_mg->determineVariableOrder( this, bvars ); + for( unsigned j=q[0].getNumChildren(); jisValid() ){ + Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl; + d_mg->setInvalid(); + break; + }else{ + std::vector< int > bvars; + d_var_mg[j]->determineVariableOrder( this, bvars ); + } + } + } + if( d_mg->isValid() ){ + std::vector< int > bvars; + d_mg->determineVariableOrder( this, bvars ); + } } + }else{ + Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl; } Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl; } @@ -131,20 +151,24 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) for( unsigned i=1; i<=2; i++ ){ flatten( n[i], beneathQuant ); } + registerNode( n[0], false, pol, beneathQuant ); + }else if( options::qcfTConstraint() ){ + //a theory-specific predicate + for( unsigned i=0; id_parent = qcf; - //qcf->d_child[i] = qcfc; - registerNode( n[i], newHasPol, newPol, beneathQuant ); + }else{ + for( unsigned i=0; id_parent = qcf; + //qcf->d_child[i] = qcfc; + registerNode( n[i], newHasPol, newPol, beneathQuant ); + } } } } @@ -152,6 +176,10 @@ void QuantInfo::registerNode( Node n, bool hasPol, bool pol, bool beneathQuant ) void QuantInfo::flatten( Node n, bool beneathQuant ) { Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl; if( n.hasBoundVar() ){ + if( n.getKind()==BOUND_VARIABLE ){ + d_inMatchConstraint[n] = true; + } + //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){ if( d_var_num.find( n )==d_var_num.end() ){ Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl; d_var_num[n] = d_vars.size(); @@ -165,9 +193,6 @@ void QuantInfo::flatten( Node n, bool beneathQuant ) { flatten( n[i], beneathQuant ); } } - if( !beneathQuant ){ - d_nbeneathQuant[n] = true; - } }else{ Trace("qcf-qregister-debug2") << "...already processed" << std::endl; } @@ -183,6 +208,7 @@ void QuantInfo::reset_round( QuantConflictFind * p ) { d_match_term[i] = TNode::null(); } d_curr_var_deq.clear(); + d_tconstraints.clear(); //add built-in variable constraints for( unsigned r=0; r<2; r++ ){ for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin(); @@ -270,6 +296,8 @@ bool QuantInfo::getCurrentCanBeEqual( QuantConflictFind * p, int v, TNode n, boo }else if( chDiseq && !isVar( n ) && !isVar( cv ) ){ //they must actually be disequal if we are looking for conflicts if( !p->areDisequal( n, cv ) ){ + //TODO : check for entailed disequal + return false; } } @@ -462,6 +490,53 @@ bool QuantInfo::isMatchSpurious( QuantConflictFind * p ) { return false; } +bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) { + if( !d_tconstraints.empty() ){ + //check constraints + for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ + //apply substitution to the tconstraint + Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(), + p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(), + terms.begin(), terms.end() ); + cons = it->second ? cons : cons.negate(); + if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){ + return true; + } + } + } + return false; +} + +bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) { + Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl; + Node rew = Rewriter::rewrite( lit ); + if( rew==p->d_false ){ + Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl; + return false; + }else if( rew!=p->d_true ){ + //if checking for conflicts, we must be sure that the constraint is entailed + if( chEnt ){ + //check if it is entailed + Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl; + std::pair et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew ); + ++(p->d_statistics.d_entailment_checks); + Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl; + if( !et.first ){ + Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl; + return false; + }else{ + return true; + } + }else{ + Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl; + return true; + } + }else{ + Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl; + return true; + } +} + bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) { //assign values for variables that were unassigned (usually not necessary, but handles corner cases) bool doFail = false; @@ -470,27 +545,124 @@ bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assign doFail = true; success = false; }else{ - d_unassigned.clear(); - d_unassigned_tn.clear(); - std::vector< int > unassigned[2]; - std::vector< TypeNode > unassigned_tn[2]; - for( int i=0; i=0; i-- ){ + int index = d_tsym_vars[i]; + TNode v = getCurrentValue( d_vars[index] ); + int slv_v = -1; + if( v==d_vars[index] ){ + slv_v = index; + } + Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl; + if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){ + Kind k = d_vars[index].getKind(); + std::vector< TNode > children; + for( unsigned j=0; jd_effort!=QuantConflictFind::effort_conflict ){ + break; + } + }else{ + Node z = p->getZero( k ); + if( !z.isNull() ){ + Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl; + assigned.push_back( vn ); + if( !setMatch( p, vn, z ) ){ + success = false; + break; + } + } + } + }else{ + Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl; + children.push_back( vv ); + } + }else{ + Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl; + children.push_back( d_vars[index][j] ); + } + } + if( success ){ + if( slv_v!=-1 ){ + Node lhs; + if( children.empty() ){ + lhs = p->getZero( k ); + }else if( children.size()==1 ){ + lhs = children[0]; + }else{ + lhs = NodeManager::currentNM()->mkNode( k, children ); + } + Node sum; + if( v==d_vars[index] ){ + sum = lhs; + }else{ + if( p->d_effort==QuantConflictFind::effort_conflict ){ + Kind kn = k; + if( d_vars[index].getKind()==PLUS ){ + kn = MINUS; + } + if( kn!=k ){ + sum = NodeManager::currentNM()->mkNode( kn, v, lhs ); + } + } + } + if( !sum.isNull() ){ + assigned.push_back( slv_v ); + Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl; + if( !setMatch( p, slv_v, sum ) ){ + success = false; + } + p->d_tempCache.push_back( sum ); + } + }else{ + //must show that constraint is met + Node sum = NodeManager::currentNM()->mkNode( k, children ); + Node eq = sum.eqNode( v ); + if( !entailmentTest( p, eq ) ){ + success = false; + } + p->d_tempCache.push_back( sum ); + } + } + } + + if( !success ){ + break; + } + } + if( success ){ + //check what is left to assign + d_unassigned.clear(); + d_unassigned_tn.clear(); + std::vector< int > unassigned[2]; + std::vector< TypeNode > unassigned_tn[2]; + for( int i=0; i& assign }while( success && isMatchSpurious( p ) ); } if( success ){ + for( unsigned i=0; i " << d_match[ui] << std::endl; + } + } return true; }else{ for( unsigned i=0; i::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){ + Trace(c) << " " << it->first << " -> " << it->second << std::endl; + } + } } -//void QuantInfo::addFuncParent( int v, Node f, int arg ) { -// if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){ -// d_f_parent[v][f].push_back( arg ); -// } -//} - -MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ - Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl; +MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){ + Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl; std::vector< Node > qni_apps; d_qni_size = 0; if( isVar ){ Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() ); - if( isHandledUfTerm( n ) ){ - d_qni_var_num[0] = qi->getVarNum( n ); - d_qni_size++; - d_type = typ_var; - d_type_not = false; - d_n = n; - //Node f = getOperator( n ); - for( unsigned j=0; jisVar( nn ) ){ - int v = qi->d_var_num[nn]; - Trace("qcf-qregister-debug") << " is var #" << v << std::endl; - d_qni_var_num[d_qni_size] = v; - //qi->addFuncParent( v, f, j ); - }else{ - Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl; - d_qni_gterm[d_qni_size] = nn; - } - d_qni_size++; - } - }else if( n.getKind()==ITE ){ + if( n.getKind()==ITE ){ d_type = typ_ite_var; d_type_not = false; d_n = n; @@ -678,8 +835,26 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ d_type = typ_invalid; } }else{ - //for now, unknown term - d_type = typ_invalid; + d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym; + d_qni_var_num[0] = qi->getVarNum( n ); + d_qni_size++; + d_type_not = false; + d_n = n; + //Node f = getOperator( n ); + for( unsigned j=0; jisVar( nn ) ){ + int v = qi->d_var_num[nn]; + Trace("qcf-qregister-debug") << " is var #" << v << std::endl; + d_qni_var_num[d_qni_size] = v; + //qi->addFuncParent( v, f, j ); + }else{ + Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl; + d_qni_gterm[d_qni_size] = nn; + } + d_qni_size++; + } } }else{ if( n.hasBoundVar() ){ @@ -693,10 +868,9 @@ MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){ if( isHandledBoolConnective( d_n ) ){ //non-literals d_type = typ_formula; - bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL; for( unsigned i=0; iisVar( d_n ) ); + d_type = typ_pred; + }else if( d_n.getKind()==BOUND_VARIABLE ){ + Assert( d_n.getType().isBoolean() ); + d_type = typ_bool_var; + }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){ + for( unsigned i=0; iisVar( d_n[i] ) ){ Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl; } Assert( qi->isVar( d_n[i] ) ); + if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){ + d_qni_var_num[i+1] = qi->d_var_num[d_n[i]]; + } }else{ d_qni_gterm[i] = d_n[i]; } } - d_type = typ_eq; - }else if( isHandledUfTerm( d_n ) ){ - Assert( qi->isVar( d_n ) ); - d_type = typ_pred; - }else if( d_n.getKind()==BOUND_VARIABLE ){ - d_type = typ_bool_var; - }else{ - Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl; + d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint; + Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl; } } }else{ @@ -900,7 +1077,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { //set up processing matches if( d_type==typ_invalid ){ - //do nothing : return success once? + //do nothing }else if( d_type==typ_ground ){ if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){ d_child_counter = 0; @@ -933,6 +1110,15 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { d_qn.push_back( qni ); } d_matched_basis = false; + }else if( d_type==typ_tsym || d_type==typ_tconstraint ){ + for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){ + int repVar = qi->getCurrentRepVar( it->second ); + if( qi->d_match[repVar].isNull() ){ + Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl; + d_qni_bound[it->first] = repVar; + } + } + d_qn.push_back( NULL ); }else if( d_type==typ_pred || d_type==typ_eq ){ //add initial constraint Node nn[2]; @@ -1031,7 +1217,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_wasSet = false; return false; } - }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){ + }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var || d_type==typ_tconstraint || d_type==typ_tsym ){ bool success = false; bool terminate = false; do { @@ -1043,6 +1229,18 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { d_binding = true; d_binding_it = d_qni_bound.begin(); doReset = true; + //for tconstraint, add constraint + if( d_type==typ_tconstraint ){ + std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n ); + if( it==qi->d_tconstraints.end() ){ + qi->d_tconstraints[d_n] = d_tgt; + //store that we added this constraint + d_qni_bound_cons[0] = d_n; + }else if( d_tgt!=it->second ){ + success = false; + terminate = true; + } + } }else{ Debug("qcf-match-debug") << " - Matching failed" << std::endl; success = false; @@ -1128,6 +1326,13 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { } d_qni_bound.clear(); } + if( d_type==typ_tconstraint ){ + //remove constraint if applicable + if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){ + qi->d_tconstraints.erase( d_n ); + d_qni_bound_cons.clear(); + } + } /* if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){ d_matched_basis = true; @@ -1869,7 +2074,9 @@ void QuantConflictFind::check( Theory::Effort level ) { if( d_performCheck ){ ++(d_statistics.d_inst_rounds); double clSet = 0; + int prevEt = 0; if( Trace.isOn("qcf-engine") ){ + prevEt = d_statistics.d_entailment_checks.getData(); clSet = double(clock())/double(CLOCKS_PER_SEC); Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl; } @@ -1980,31 +2187,37 @@ void QuantConflictFind::check( Theory::Effort level ) { */ std::vector< Node > terms; qi->getMatch( terms ); - if( Debug.isOn("qcf-check-inst") ){ - //if( e==effort_conflict ){ - Node inst = d_quantEngine->getInstantiation( q, terms ); - Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; - Assert( evaluate( inst )!=1 ); - Assert( evaluate( inst )==-1 || e>effort_conflict ); - //} - } - if( d_quantEngine->addInstantiation( q, terms ) ){ - Trace("qcf-check") << " ... Added instantiation" << std::endl; - ++addedLemmas; - if( e==effort_conflict ){ - d_quant_order.insert( d_quant_order.begin(), q ); - d_conflict.set( true ); - ++(d_statistics.d_conflict_inst); - break; - }else if( e==effort_prop_eq ){ - ++(d_statistics.d_prop_inst); + if( !qi->isTConstraintSpurious( this, terms ) ){ + if( Debug.isOn("qcf-check-inst") ){ + //if( e==effort_conflict ){ + Node inst = d_quantEngine->getInstantiation( q, terms ); + Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl; + Assert( evaluate( inst )!=1 ); + Assert( evaluate( inst )==-1 || e>effort_conflict ); + //} + } + if( d_quantEngine->addInstantiation( q, terms ) ){ + Trace("qcf-check") << " ... Added instantiation" << std::endl; + Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl; + qi->debugPrintMatch("qcf-inst"); + Trace("qcf-inst") << std::endl; + ++addedLemmas; + if( e==effort_conflict ){ + d_quant_order.insert( d_quant_order.begin(), q ); + d_conflict.set( true ); + ++(d_statistics.d_conflict_inst); + break; + }else if( e==effort_prop_eq ){ + ++(d_statistics.d_prop_inst); + } + }else{ + Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; + //Assert( false ); } - }else{ - Trace("qcf-check") << " ... Failed to add instantiation" << std::endl; - //Assert( false ); } //clean up assigned qi->revertMatch( assigned ); + d_tempCache.clear(); }else{ Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl; } @@ -2030,6 +2243,8 @@ void QuantConflictFind::check( Theory::Effort level ) { Trace("qcf-engine") << ", addedLemmas = " << addedLemmas; } Trace("qcf-engine") << std::endl; + int currEt = d_statistics.d_entailment_checks.getData(); + Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl; } } Trace("qcf-check2") << "QCF : finished check : " << level << std::endl; @@ -2275,17 +2490,35 @@ void QuantConflictFind::debugPrintQuantBody( const char * c, Node q, Node n, boo QuantConflictFind::Statistics::Statistics(): d_inst_rounds("QuantConflictFind::Inst_Rounds", 0), d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ), - d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ) + d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ), + d_entailment_checks("QuantConflictFind::Entailment_Checks",0) { StatisticsRegistry::registerStat(&d_inst_rounds); StatisticsRegistry::registerStat(&d_conflict_inst); StatisticsRegistry::registerStat(&d_prop_inst); + StatisticsRegistry::registerStat(&d_entailment_checks); } QuantConflictFind::Statistics::~Statistics(){ StatisticsRegistry::unregisterStat(&d_inst_rounds); StatisticsRegistry::unregisterStat(&d_conflict_inst); StatisticsRegistry::unregisterStat(&d_prop_inst); + StatisticsRegistry::unregisterStat(&d_entailment_checks); } +TNode QuantConflictFind::getZero( Kind k ) { + std::map< Kind, Node >::iterator it = d_zero.find( k ); + if( it==d_zero.end() ){ + Node nn; + if( k==PLUS ){ + nn = NodeManager::currentNM()->mkConst( Rational(0) ); + } + d_zero[k] = nn; + return nn; + }else{ + return it->second; + } +} + + } diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 71e967653..64ece7ed0 100755 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -84,11 +84,13 @@ public: typ_var, typ_ite_var, typ_bool_var, + typ_tconstraint, + typ_tsym, }; void debugPrintType( const char * c, short typ, bool isTrace = false ); public: MatchGen() : d_type( typ_invalid ){} - MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false ); + MatchGen( QuantInfo * qi, Node n, bool isVar = false ); bool d_tgt; bool d_tgt_orig; bool d_wasSet; @@ -128,7 +130,8 @@ public: ~QuantInfo() { delete d_mg; } std::vector< TNode > d_vars; std::map< TNode, int > d_var_num; - std::map< TNode, bool > d_nbeneathQuant; + std::vector< int > d_tsym_vars; + std::map< TNode, bool > d_inMatchConstraint; std::map< int, std::vector< Node > > d_var_constraint[2]; int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; } bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); } @@ -146,6 +149,7 @@ public: std::vector< TNode > d_match; std::vector< TNode > d_match_term; std::map< int, std::map< TNode, int > > d_curr_var_deq; + std::map< Node, bool > d_tconstraints; int getCurrentRepVar( int v ); TNode getCurrentValue( TNode n ); TNode getCurrentExpValue( TNode n ); @@ -154,6 +158,8 @@ public: int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove ); bool setMatch( QuantConflictFind * p, int v, TNode n ); bool isMatchSpurious( QuantConflictFind * p ); + bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ); + bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true ); bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false ); void revertMatch( std::vector< int >& assigned ); void debugPrintMatch( const char * c ); @@ -174,6 +180,9 @@ private: context::CDO< bool > d_conflict; bool d_performCheck; std::vector< Node > d_quant_order; + std::map< Kind, Node > d_zero; + //for storing nodes created during t-constraint solving (prevents memory leaks) + std::vector< Node > d_tempCache; private: std::map< Node, Node > d_op_node; int d_fid_count; @@ -182,6 +191,7 @@ private: public: //for ground terms Node d_true; Node d_false; + TNode getZero( Kind k ); private: Node evaluateTerm( Node n ); int evaluate( Node n, bool pref = false, bool hasPref = false ); @@ -271,6 +281,7 @@ public: IntStat d_inst_rounds; IntStat d_conflict_inst; IntStat d_prop_inst; + IntStat d_entailment_checks; Statistics(); ~Statistics(); }; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 41108bc2a..757a76baa 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -207,7 +207,7 @@ public: Node getSkolemizedBody( Node f ); //miscellaneous -private: +public: /** map from universal quantifiers to the list of variables */ std::map< Node, std::vector< Node > > d_vars; /** free variable for instantiation constant type */ diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index c52ee936a..f65e48ec2 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -228,6 +228,32 @@ Theory::PPAssertStatus Theory::ppAssert(TNode in, SubstitutionMap& outSubstituti return PP_ASSERT_STATUS_UNSOLVED; } +std::pair Theory::entailmentCheck(TNode lit, + const EntailmentCheckParameters* params, + EntailmentCheckSideEffects* out){ + return make_pair(false, Node::null()); +} + +EntailmentCheckParameters::EntailmentCheckParameters(TheoryId tid) + : d_tid(tid) { +} + +EntailmentCheckParameters::~EntailmentCheckParameters(){} + +TheoryId EntailmentCheckParameters::getTheoryId() const { + return d_tid; +} + +EntailmentCheckSideEffects::EntailmentCheckSideEffects(TheoryId tid) + : d_tid(tid) +{} + +TheoryId EntailmentCheckSideEffects::getTheoryId() const { + return d_tid; +} + +EntailmentCheckSideEffects::~EntailmentCheckSideEffects() { +} }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory.h b/src/theory/theory.h index c86aa17de..972abe3d8 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -52,6 +52,9 @@ class QuantifiersEngine; class TheoryModel; class SubstitutionMap; +class EntailmentCheckParameters; +class EntailmentCheckSideEffects; + namespace rrinst { class CandidateGenerator; }/* CVC4::theory::rrinst namespace */ @@ -808,6 +811,63 @@ public: * in a queriable form. As this is */ std::hash_set currentlySharedTerms() const; + + /** + * This allows the theory to be queried for whether a literal, lit, is + * entailed by the theory. This returns a pair of a Boolean and a node E. + * + * If the Boolean is true, then E is a formula that entails lit and E is propositionally + * entailed by the assertions to the theory. + * + * If the Boolean is false, it is "unknown" if lit is entailed and E may be + * any node. + * + * The literal lit is either an atom a or (not a), which must belong to the theory: + * There is some TheoryOfMode m s.t. Theory::theoryOf(m, a) == this->getId(). + * + * There are NO assumptions that a or the subterms of a have been + * preprocessed in any form. This includes ppRewrite, rewriting, + * preregistering, registering, definition expansion or ITE removal! + * + * Theories are free to limit the amount of effort they use and so may + * always opt to return "unknown". Both "unknown" and "not entailed", + * may return for E a non-boolean Node (e.g. Node::null()). (There is no explicit output + * for the negation of lit is entailed.) + * + * If lit is theory valid, the return result may be the Boolean constant + * true for E. + * + * If lit is entailed by multiple assertions on the theory's getFact() + * queue, a_1, a_2, ... and a_k, this may return E=(and a_1 a_2 ... a_k) or + * another theory entailed explanation E=(and (and a_1 a_2) (and a3 a_4) ... a_k) + * + * If lit is entailed by a single assertion on the theory's getFact() + * queue, say a, this may return E=a. + * + * The theory may always return false! + * + * The search is controlled by the parameter params. For default behavior, + * this may be left NULL. + * + * Theories that want parameters extend the virtual EntailmentCheckParameters + * class. Users ask the theory for an appropriate subclass from the theory + * and configure that. How this is implemented is on a per theory basis. + * + * The search may provide additional output to guide the user of + * this function. This output is stored in a EntailmentCheckSideEffects* + * output parameter. The implementation of this is theory specific. For + * no output, this is NULL. + * + * Theories may not touch their output stream during an entailment check. + * + * @param lit a literal belonging to the theory. + * @param params the control parameters for the entailment check. + * @param out a theory specific output object of the entailment search. + * @return a pair s.t. if b is true, then a formula E such that + * E |= lit in the theory. + */ + virtual std::pair entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL); + };/* class Theory */ std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level); @@ -852,6 +912,26 @@ inline std::ostream& operator << (std::ostream& out, theory::Theory::PPAssertSta return out; } +class EntailmentCheckParameters { +private: + TheoryId d_tid; +protected: + EntailmentCheckParameters(TheoryId tid); +public: + TheoryId getTheoryId() const; + virtual ~EntailmentCheckParameters(); +};/* class EntailmentCheckParameters */ + +class EntailmentCheckSideEffects { +private: + TheoryId d_tid; +protected: + EntailmentCheckSideEffects(TheoryId tid); +public: + TheoryId getTheoryId() const; + virtual ~EntailmentCheckSideEffects(); +};/* class EntailmentCheckSideEffects */ + }/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index 33ff18126..18968e897 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -1658,3 +1658,15 @@ void TheoryEngine::checkTheoryAssertionsWithModel() { } } } + +std::pair TheoryEngine::entailmentCheck(theory::TheoryOfMode mode, TNode lit, const EntailmentCheckParameters* params, EntailmentCheckSideEffects* seffects) { + TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit; + theory::TheoryId tid = theory::Theory::theoryOf(mode, atom); + theory::Theory* th = theoryOf(tid); + + Assert(th != NULL); + Assert(params == NULL || tid == params->getTheoryId()); + Assert(seffects == NULL || tid == seffects->getTheoryId()); + + return th->entailmentCheck(lit, params, seffects); +} diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 9a987c9d7..8bc67616f 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -83,6 +83,9 @@ namespace theory { namespace eq { class EqualityEngine; } + + class EntailmentCheckParameters; + class EntailmentCheckSideEffects; }/* CVC4::theory namespace */ class DecisionEngine; class RemoveITE; @@ -755,6 +758,12 @@ public: */ Node getModelValue(TNode var); + /** + * Forwards an entailmentCheck according to the given theoryOfMode mode. + * See theory.h for documentation on entailmentCheck(). + */ + std::pair entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL); + private: /** Default visitor for pre-registration */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 383f27688..bd23b48c9 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -57,3 +57,26 @@ void Integer::readInt(const cln::cl_read_flags& flags, const std::string& s, uns throw std::invalid_argument(ss.str()); } } + +bool Integer::fitsSignedInt() const { + // TODO improve performance + return d_value <= std::numeric_limits::max() && + d_value >= std::numeric_limits::min(); +} + +bool Integer::fitsUnsignedInt() const { + // TODO improve performance + return sgn() >= 0 && d_value <= std::numeric_limits::max(); +} + +signed int Integer::getSignedInt() const { + // ensure there isn't overflow + CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + return cln::cl_I_to_int(d_value); +} + +unsigned int Integer::getUnsignedInt() const { + // ensure there isn't overflow + CheckArgument(fitsUnsignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + return cln::cl_I_to_uint(d_value); +} diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 05d820dbc..8b56c4b19 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -415,6 +415,16 @@ public: return d_value == -1; } + /** fits the C "signed int" primitive */ + bool fitsSignedInt() const; + + /** fits the C "unsigned int" primitive */ + bool fitsUnsignedInt() const; + + int getSignedInt() const; + + unsigned int getUnsignedInt() const; + long getLong() const { // ensure there isn't overflow CheckArgument(d_value <= std::numeric_limits::max(), this, diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index f2a888340..bb6166523 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -36,3 +36,32 @@ Integer::Integer(const char* s, unsigned base) Integer::Integer(const std::string& s, unsigned base) : d_value(s, base) {} + + +bool Integer::fitsSignedInt() const { + return d_value.fits_sint_p(); +} + +bool Integer::fitsUnsignedInt() const { + return d_value.fits_uint_p(); +} + +signed int Integer::getSignedInt() const { + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits::max(), this, + "Overflow detected in Integer::getSignedInt()"); + CheckArgument(d_value >= std::numeric_limits::min(), this, + "Overflow detected in Integer::getSignedInt()"); + CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getSignedInt()"); + return (signed int) d_value.get_si(); +} + +unsigned int Integer::getUnsignedInt() const { + // ensure there isn't overflow + CheckArgument(d_value <= std::numeric_limits::max(), this, + "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(d_value >= std::numeric_limits::min(), this, + "Overflow detected in Integer::getUnsignedInt()"); + CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()"); + return (unsigned int) d_value.get_ui(); +} diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index a39de7996..68d335aec 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -22,6 +22,7 @@ #include #include +#include #include "util/gmp_util.h" #include "util/exception.h" @@ -417,7 +418,13 @@ public: return d_value.get_str(base); } - //friend std::ostream& operator<<(std::ostream& os, const Integer& n); + bool fitsSignedInt() const; + + bool fitsUnsignedInt() const; + + signed int getSignedInt() const; + + unsigned int getUnsignedInt() const; long getLong() const { long si = d_value.get_si(); diff --git a/src/util/maybe.h b/src/util/maybe.h index e90953e0b..b1c81f76e 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -75,6 +75,7 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe& m){ if(m.nothing()){ out << "Nothing"; }else{ + out << "Just "; out << m.constValue(); } out << "}"; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 9f4998fd8..b21311da1 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -36,15 +36,15 @@ TESTS = \ smtlib384a03.smt2 \ smtlib46f14a.smt2 \ smtlibf957ea.smt2 \ - gauss_init_0030.fof.smt2 + gauss_init_0030.fof.smt2 \ + qcft-javafe.filespace.TreeWalker.006.smt2 \ + qcft-smtlib3dbc51.smt2 \ + symmetric_unsat_7.smt2 \ + javafe.ast.StmtVec.009.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine # set3.smt2 -# removed because it now reports unknown -# symmetric_unsat_7.smt2 \ -# - # removed because they take more than 20s # ex1.smt2 \ @@ -57,12 +57,11 @@ TESTS = \ # javafe.ast.WhileStmt.447.smt2 \ # javafe.tc.CheckCompilationUnit.001.smt2 \ # javafe.tc.FlowInsensitiveChecks.682.smt2 \ -# array-unsat-simp3.smt2 \ +# array-unsat-simp3.smt2 # EXTRA_DIST = $(TESTS) \ - bug291.smt2.expect \ - array-unsat-simp3.smt2.expect + bug291.smt2.expect #if CVC4_BUILD_PROFILE_COMPETITION #else diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 index a16c9395d..9dade2073 100644 --- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 +++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --full-saturate-quant +; EXPECT: unsat (set-logic AUFLIA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") @@ -18,5 +20,4 @@ (assert (not (= i1 i2))) (assert (not (= (store_uf (store_uf a1 i1 e1) i2 e2) (store_uf (store_uf a1 i2 e2) i1 e1)))) (check-sat) -(get-info :reason-unknown) (exit) diff --git a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect index 2bd8349de..b4ea773f0 100644 --- a/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect +++ b/test/regress/regress0/quantifiers/array-unsat-simp3.smt2.expect @@ -1,2 +1 @@ -% EXPECT: unknown -% EXPECT: (:reason-unknown incomplete) +% EXPECT: unsat diff --git a/test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 b/test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 new file mode 100644 index 000000000..2a5eb34a7 --- /dev/null +++ b/test/regress/regress0/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 @@ -0,0 +1,432 @@ +; COMMAND-LINE: --qcf-tconstraint +; EXPECT: unsat +(set-logic AUFLIA) +(set-info :source | + Simplify front end test suite. + This benchmark was translated by Michal Moskal. +|) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-fun EC_134.22_134.22 () Int) +(declare-fun integralOr (Int Int) Int) +(declare-fun this_95.46_87.8_0_95.46 () Int) +(declare-fun EC_183.16_183.16 () Int) +(declare-fun arrayShapeMore (Int Int) Int) +(declare-fun integralAnd (Int Int) Int) +(declare-fun T_.TYPE () Int) +(declare-fun EC_156.1_0_158.5_0_159.22_159.22 () Int) +(declare-fun intFirst () Int) +(declare-fun after_192.22_192.22 () Int) +(declare-fun T_javafe.filespace.HashTree () Int) +(declare-fun lookAhead_4.43.19 () Int) +(declare-fun after_90.24_87.8_0_90.24_5.89.17 () Int) +(declare-fun eClosedTime (Int) Int) +(declare-fun int_m9223372036854775808 () Int) +(declare-fun C_87.8 () Int) +(declare-fun int_m2147483648 () Int) +(declare-fun T_java.lang.Comparable () Int) +(declare-fun arrayPosition (Int) Int) +(declare-fun treeName_186.1 () Int) +(declare-fun remainingNodes_loopold_48.26 () Int) +(declare-fun after_189.12_189.12 () Int) +(declare-fun this_159.11_156.1_0_158.5_0_159.11 () Int) +(declare-fun select1 (Int Int) Int) +(declare-fun select2 (Int Int Int) Int) +(declare-fun EC_192.22_192.22 () Int) +(declare-fun L_158.5 () Int) +(declare-fun T_java.util.EscjavaKeyValue () Int) +(declare-fun elems_1_ () Int) +(declare-fun c_loopold_133.5 () Int) +(declare-fun T_long () Int) +(declare-fun EC_121.8_121.8 () Int) +(declare-fun EC_65.1_65.1 () Int) +(declare-fun moreElements_192.1_0_193.28_5.89.17 () Int) +(declare-fun after_121.8_121.8 () Int) +(declare-fun T_javafe.filespace.LookAheadEnum () Int) +(declare-fun lockLE (Int Int) Bool) +(declare-fun classLiteral (Int) Int) +(declare-fun lockLT (Int Int) Bool) +(declare-fun T_javafe.filespace.Tree () Int) +(declare-fun elems_2_ () Int) +(declare-fun EC_189.12_189.12 () Int) +(declare-fun T_float () Int) +(declare-fun alloc () Int) +(declare-fun T_java.io.OutputStream () Int) +(declare-fun EC_87.8_0_89.24_89.24 () Int) +(declare-fun S_194.56 () Int) +(declare-fun asChild (Int Int) Int) +(declare-fun CONCVARSYM (Int) Int) +(declare-fun T_int () Int) +(declare-fun after_65.1_65.1 () Int) +(declare-fun int_2147483647 () Int) +(declare-fun RES_130.35 () Int) +(declare-fun remainingNodes_48.26_1_ () Int) +(declare-fun int_9223372036854775807 () Int) +(declare-fun this () Int) +(declare-fun T_byte () Int) +(declare-fun T_java.lang.System () Int) +(declare-fun store1 (Int Int Int) Int) +(declare-fun store2 (Int Int Int Int) Int) +(declare-fun RES_loopold () Int) +(declare-fun remainingNodes_48.26_2_ () Int) +(declare-fun max (Int) Int) +(declare-fun elems_156.1_0_158.5_0_1_ () Int) +(declare-fun moreElements_pre_5.58.29 () Int) +(declare-fun moreElements_87.8_0_90.24_5.89.17 () Int) +(declare-fun objectToBeConstructed () Int) +(declare-fun T_java.util.Map () Int) +(declare-fun tmp4_156.1_0_158.5_0_163.8 () Int) +(declare-fun T_javafe.filespace.TreeWalker () Int) +(declare-fun after_189.25_189.25 () Int) +(declare-fun integralDiv (Int Int) Int) +(declare-fun i_156.1_0_158.5_0_158.33 () Int) +(declare-fun after_135.35_134.1_0_135.35_5.89.17 () Int) +(declare-fun EC_130.36_130.36 () Int) +(declare-fun RES_121.33_121.33 () Int) +(declare-fun moreElements_loopold_5.58.29 () Int) +(declare-fun RES_134.22_134.22 () Int) +(declare-fun list_210.13 () Int) +(declare-fun EC_189.25_189.25 () Int) +(declare-fun T_java.lang.Class () Int) +(declare-fun T_java.lang.Object () Int) +(declare-fun tmp_156.1_0_158.5_0_161.6 () Int) +(declare-fun remainingChildren_pre_39.26 () Int) +(declare-fun EC_192.1_1_192.45_192.45 () Int) +(declare-fun RES_192.1_1_192.45_192.45 () Int) +(declare-fun RES_156.1_0_158.5_0_160.18_160.18 () Int) +(declare-fun longLast () Int) +(declare-fun termConditional (Int Int Int) Int) +(declare-fun T_java.util.Dictionary () Int) +(declare-fun C_156.1 () Int) +(declare-fun bool_false () Int) +(declare-fun RES_192.22_192.22 () Int) +(declare-fun T_javafe.filespace.FileTree () Int) +(declare-fun alloc_loopold () Int) +(declare-fun Smt.true () Int) +(declare-fun returnsNull_5.79.29 () Int) +(declare-fun c_134.1_0_135.20 () Int) +(declare-fun asLockSet (Int) Int) +(declare-fun integralMod (Int Int) Int) +(declare-fun RES_67.21_67.21 () Int) +(declare-fun RES_156.1_0_158.5_0_159.11_159.11 () Int) +(declare-fun Smt.false () Int) +(declare-fun typeof (Int) Int) +(declare-fun int_18446744073709551615 () Int) +(declare-fun RES_189.12_189.12 () Int) +(declare-fun this_160.18_156.1_0_158.5_0_160.18 () Int) +(declare-fun EC_134.1_0_134.36_134.36 () Int) +(declare-fun RES_89.23 () Int) +(declare-fun RES_134.1_0_134.36_134.36 () Int) +(declare-fun RES_87.8_0_93.28_93.28 () Int) +(declare-fun elementType_5.74.27 () Int) +(declare-fun stringCat (Int Int) Int) +(declare-fun remainingChildren_39.26_1_ () Int) +(declare-fun RES_87.8_0_95.46_95.46 () Int) +(declare-fun lookAheadValid_4.40.20 () Int) +(declare-fun T_boolean () Int) +(declare-fun longFirst () Int) +(declare-fun elems_loopold_156.1_0 () Int) +(declare-fun T_java.util.Hashtable () Int) +(declare-fun elems_loopold () Int) +(declare-fun T_java.util.Properties () Int) +(declare-fun L_87.8 () Int) +(declare-fun RES_68.21_68.21 () Int) +(declare-fun RES_65.1_65.1 () Int) +(declare-fun arrayFresh (Int Int Int Int Int Int Int) Bool) +(declare-fun RES () Int) +(declare-fun elementType_pre_5.74.27 () Int) +(declare-fun L_156.1 () Int) +(declare-fun intLast () Int) +(declare-fun RES_130.36_130.36 () Int) +(declare-fun RES_87.8_0_90.24_90.24 () Int) +(declare-fun arrayType () Int) +(declare-fun RES_189.25_189.25 () Int) +(declare-fun boolEq (Int Int) Bool) +(declare-fun EC_134.1_0_135.35_135.35 () Int) +(declare-fun after_193.28_192.1_0_193.28_5.89.17 () Int) +(declare-fun RES_134.1_0_135.35_135.35 () Int) +(declare-fun T_129.49 () Int) +(declare-fun arrayLength (Int) Int) +(declare-fun cast (Int Int) Int) +(declare-fun nextChild_87.8_0_95.5 () Int) +(declare-fun elementType_71.16 () Int) +(declare-fun asElems (Int) Int) +(declare-fun T_javafe.filespace.PreloadedTree () Int) +(declare-fun moreElements_5.58.29 () Int) +(declare-fun T_char () Int) +(declare-fun EC_192.1_0_194.16_194.16 () Int) +(declare-fun owner_pre_6.35.28 () Int) +(declare-fun RES_156.1_0_158.5_0_159.22_159.22 () Int) +(declare-fun EC_140.1_140.1 () Int) +(declare-fun divides (Int Int) Int) +(declare-fun returnsNull_72.16 () Int) +(declare-fun remainingChildren_39.26 () Int) +(declare-fun remainingNodes_68.1 () Int) +(declare-fun T_javafe.filespace.TreeWalker_ArrayEnum () Int) +(declare-fun arg0_194.16_192.1_0_194.16_17.. () Int) +(declare-fun InRange (Int Int) Bool) +(declare-fun moreElements_87.8_0_95.46_5.89.17 () Int) +(declare-fun sorted_157.13 () Int) +(declare-fun moreElements_134.1_0_135.35_5.89.17 () Int) +(declare-fun out_pre_16.83.49 () Int) +(declare-fun elementType_69.24 () Int) +(declare-fun RES_121.8_121.8 () Int) +(declare-fun lookAheadValid_pre_4.40.20 () Int) +(declare-fun refEQ (Int Int) Int) +(declare-fun EC_loopold () Int) +(declare-fun EC_157.5 () Int) +(declare-fun remainingNodes_pre_48.26 () Int) +(declare-fun EC_156.1_0_158.5_0_160.18_160.18 () Int) +(declare-fun subtree_192.1_0_193.5 () Int) +(declare-fun is (Int Int) Int) +(declare-fun i_loopold_156.1_0_158.14 () Int) +(declare-fun integralEQ (Int Int) Int) +(declare-fun RES_87.8_0_89.24_89.24 () Int) +(declare-fun boolNE (Int Int) Bool) +(declare-fun EC_134.1_1_134.36_134.36 () Int) +(declare-fun RES_134.1_1_134.36_134.36 () Int) +(declare-fun T_java.io.FilterOutputStream () Int) +(declare-fun remainingNodes_48.26 () Int) +(declare-fun tmp0_new_Tree___130.25 () Int) +(declare-fun isNewArray (Int) Int) +(declare-fun L_192.1 () Int) +(declare-fun elems_pre () Int) +(declare-fun T_63.27 () Int) +(declare-fun intShiftL (Int Int) Int) +(declare-fun nonnullelements (Int Int) Bool) +(declare-fun multiply (Int Int) Int) +(declare-fun integralGE (Int Int) Int) +(declare-fun lookAhead_pre_4.43.19 () Int) +(declare-fun T_short () Int) +(declare-fun EC_67.21_67.21 () Int) +(declare-fun alloc_pre () Int) +(declare-fun integralGT (Int Int) Int) +(declare-fun EC () Int) +(declare-fun boolAnd (Int Int) Bool) +(declare-fun EC_156.1_0_158.5_0_159.11_159.11 () Int) +(declare-fun EC_1_ () Int) +(declare-fun EC_192.1_0_194.32_194.32 () Int) +(declare-fun RES_192.1_0_194.32_194.32 () Int) +(declare-fun arrayShapeOne (Int) Int) +(declare-fun T_double () Int) +(declare-fun out_16.83.49 () Int) +(declare-fun owner_6.35.28 () Int) +(declare-fun longShiftL (Int Int) Int) +(declare-fun list_pre_210.13 () Int) +(declare-fun T_java.io.Serializable () Int) +(declare-fun boolOr (Int Int) Bool) +(declare-fun L_134.1 () Int) +(declare-fun int_4294967295 () Int) +(declare-fun modulo (Int Int) Int) +(declare-fun EC_87.8_0_93.28_93.28 () Int) +(declare-fun EC_2_ () Int) +(declare-fun EC_130.35 () Int) +(declare-fun elems_134.1_0 () Int) +(declare-fun T_120.50 () Int) +(declare-fun returnsNull_pre_5.79.29 () Int) +(declare-fun EC_152.6 () Int) +(declare-fun EC_87.8_0_95.46_95.46 () Int) +(declare-fun EC_182.16 () Int) +(declare-fun after_95.46_87.8_0_95.46_5.89.17 () Int) +(declare-fun null () Int) +(declare-fun args_181.36 () Int) +(declare-fun EC_152.6_1_ () Int) +(declare-fun T_java.lang.String () Int) +(declare-fun asField (Int Int) Int) +(declare-fun a_150.36 () Int) +(declare-fun EC_68.21_68.21 () Int) +(declare-fun T_java.io.File () Int) +(declare-fun after_68.21_68.21 () Int) +(declare-fun boolImplies (Int Int) Bool) +(declare-fun sorted_157.13_1_ () Int) +(declare-fun integralLE (Int Int) Int) +(declare-fun RES_1_ () Int) +(declare-fun tmp0_remainingNodes_69.9 () Int) +(declare-fun elems_156.1_0_158.5_0 () Int) +(declare-fun integralLT (Int Int) Int) +(declare-fun this_93.28_87.8_0_93.28 () Int) +(declare-fun T_java.util.Enumeration () Int) +(declare-fun vAllocTime (Int) Int) +(declare-fun EC_192.1_0_193.28_193.28 () Int) +(declare-fun sorted_157.13_2_ () Int) +(declare-fun this_89.24_87.8_0_89.24 () Int) +(declare-fun T_java.lang.Cloneable () Int) +(declare-fun RES_192.1_0_193.28_193.28 () Int) +(declare-fun RES_2_ () Int) +(declare-fun boolNot (Int) Bool) +(declare-fun refNE (Int Int) Int) +(declare-fun integralXor (Int Int) Int) +(declare-fun classDown (Int Int) Int) +(declare-fun EC_loopold_156.1_0 () Int) +(declare-fun sorted_loopold_156.1_0_157.13 () Int) +(declare-fun this_90.24_87.8_0_90.24 () Int) +(declare-fun integralNE (Int Int) Int) +(declare-fun T_java.io.PrintStream () Int) +(declare-fun EC_87.8_0_90.24_90.24 () Int) +(declare-fun arrayParent (Int) Int) +(declare-fun elemtype (Int) Int) +(declare-fun fClosedTime (Int) Int) +(declare-fun alloc_1_ () Int) +(declare-fun EC_192.1_0_192.45_192.45 () Int) +(declare-fun array (Int) Int) +(declare-fun RES_192.1_0_192.45_192.45 () Int) +(declare-fun LS () Int) +(declare-fun remainingChildren_67.1 () Int) +(declare-fun ecReturn () Int) +(declare-fun isAllocated (Int Int) Bool) +(declare-fun alloc_2_ () Int) +(declare-fun elems () Int) +(declare-fun subtypes (Int Int) Bool) +(declare-fun T_javafe.filespace.EmptyEnum () Int) +(declare-fun EC_182.16_1_ () Int) +(declare-fun EC_121.33_121.33 () Int) +(assert (subtypes T_java.io.OutputStream T_java.lang.Object)) +(assert (= T_java.io.OutputStream (asChild T_java.io.OutputStream T_java.lang.Object))) +(assert (subtypes T_java.io.FilterOutputStream T_java.io.OutputStream)) +(assert (= T_java.io.FilterOutputStream (asChild T_java.io.FilterOutputStream T_java.io.OutputStream))) +(assert (subtypes T_javafe.filespace.TreeWalker T_javafe.filespace.LookAheadEnum)) +(assert (= T_javafe.filespace.TreeWalker (asChild T_javafe.filespace.TreeWalker T_javafe.filespace.LookAheadEnum))) +(assert (forall ((?t Int)) (! (= (subtypes ?t T_javafe.filespace.TreeWalker) (= ?t T_javafe.filespace.TreeWalker)) :pattern ((subtypes ?t T_javafe.filespace.TreeWalker)) ))) +(assert (subtypes T_javafe.filespace.FileTree T_javafe.filespace.PreloadedTree)) +(assert (= T_javafe.filespace.FileTree (asChild T_javafe.filespace.FileTree T_javafe.filespace.PreloadedTree))) +(assert (subtypes T_javafe.filespace.LookAheadEnum T_java.lang.Object)) +(assert (= T_javafe.filespace.LookAheadEnum (asChild T_javafe.filespace.LookAheadEnum T_java.lang.Object))) +(assert (subtypes T_javafe.filespace.LookAheadEnum T_java.util.Enumeration)) +(assert (subtypes T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.LookAheadEnum)) +(assert (= T_javafe.filespace.TreeWalker_ArrayEnum (asChild T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.LookAheadEnum))) +(assert (subtypes T_javafe.filespace.HashTree T_javafe.filespace.Tree)) +(assert (= T_javafe.filespace.HashTree (asChild T_javafe.filespace.HashTree T_javafe.filespace.Tree))) +(assert (subtypes T_java.lang.System T_java.lang.Object)) +(assert (= T_java.lang.System (asChild T_java.lang.System T_java.lang.Object))) +(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.System) (= ?t T_java.lang.System)) :pattern ((subtypes ?t T_java.lang.System)) ))) +(assert (subtypes T_java.util.EscjavaKeyValue T_java.lang.Object)) +(assert (subtypes T_java.util.Properties T_java.util.Hashtable)) +(assert (= T_java.util.Properties (asChild T_java.util.Properties T_java.util.Hashtable))) +(assert (subtypes T_javafe.filespace.Tree T_java.lang.Object)) +(assert (= T_javafe.filespace.Tree (asChild T_javafe.filespace.Tree T_java.lang.Object))) +(assert (subtypes T_java.lang.String T_java.lang.Object)) +(assert (= T_java.lang.String (asChild T_java.lang.String T_java.lang.Object))) +(assert (forall ((?t Int)) (! (= (subtypes ?t T_java.lang.String) (= ?t T_java.lang.String)) :pattern ((subtypes ?t T_java.lang.String)) ))) +(assert (subtypes T_java.lang.String T_java.io.Serializable)) +(assert (subtypes T_java.lang.String T_java.lang.Comparable)) +(assert (subtypes T_java.util.Enumeration T_java.lang.Object)) +(assert (subtypes T_java.lang.Comparable T_java.lang.Object)) +(assert (subtypes T_java.util.Map T_java.lang.Object)) +(assert (subtypes T_java.util.Map T_java.util.EscjavaKeyValue)) +(assert (subtypes T_java.util.Dictionary T_java.lang.Object)) +(assert (= T_java.util.Dictionary (asChild T_java.util.Dictionary T_java.lang.Object))) +(assert (subtypes T_java.util.Dictionary T_java.util.EscjavaKeyValue)) +(assert (subtypes T_java.io.Serializable T_java.lang.Object)) +(assert (subtypes T_java.io.PrintStream T_java.io.FilterOutputStream)) +(assert (= T_java.io.PrintStream (asChild T_java.io.PrintStream T_java.io.FilterOutputStream))) +(assert (subtypes T_javafe.filespace.PreloadedTree T_javafe.filespace.HashTree)) +(assert (= T_javafe.filespace.PreloadedTree (asChild T_javafe.filespace.PreloadedTree T_javafe.filespace.HashTree))) +(assert (subtypes T_java.util.Hashtable T_java.util.Dictionary)) +(assert (= T_java.util.Hashtable (asChild T_java.util.Hashtable T_java.util.Dictionary))) +(assert (subtypes T_java.util.Hashtable T_java.util.Map)) +(assert (subtypes T_java.util.Hashtable T_java.lang.Cloneable)) +(assert (subtypes T_java.util.Hashtable T_java.io.Serializable)) +(assert (subtypes T_java.lang.Cloneable T_java.lang.Object)) +(assert (subtypes T_javafe.filespace.EmptyEnum T_java.lang.Object)) +(assert (= T_javafe.filespace.EmptyEnum (asChild T_javafe.filespace.EmptyEnum T_java.lang.Object))) +(assert (subtypes T_javafe.filespace.EmptyEnum T_java.util.Enumeration)) +(assert (subtypes T_java.io.File T_java.lang.Object)) +(assert (= T_java.io.File (asChild T_java.io.File T_java.lang.Object))) +(assert (subtypes T_java.io.File T_java.io.Serializable)) +(assert (subtypes T_java.io.File T_java.lang.Comparable)) +(assert (distinct arrayType T_boolean T_char T_byte T_short T_int T_long T_float T_double T_.TYPE T_java.io.OutputStream T_java.io.FilterOutputStream T_javafe.filespace.TreeWalker T_javafe.filespace.FileTree T_javafe.filespace.LookAheadEnum T_javafe.filespace.TreeWalker_ArrayEnum T_javafe.filespace.HashTree T_java.lang.System T_java.util.EscjavaKeyValue T_java.util.Properties T_javafe.filespace.Tree T_java.lang.String T_java.util.Enumeration T_java.lang.Comparable T_java.util.Map T_java.util.Dictionary T_java.io.Serializable T_java.io.PrintStream T_javafe.filespace.PreloadedTree T_java.util.Hashtable T_java.lang.Cloneable T_javafe.filespace.EmptyEnum T_java.io.File T_java.lang.Object)) +(assert (= Smt.true (is out_16.83.49 T_java.io.PrintStream))) +(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 63)) (<= 1 (longShiftL 1 ?n))) :pattern ((longShiftL 1 ?n)) ))) +(assert (forall ((?n Int)) (! (=> (and (<= 0 ?n) (< ?n 31)) (<= 1 (intShiftL 1 ?n))) :pattern ((intShiftL 1 ?n)) ))) +(assert (forall ((?x Int) (?y Int)) (! (=> (and (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralXor ?x ?y))) :pattern ((integralXor ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralDiv ?x ?y))) (=> (and (<= 0 ?x) (< 0 ?y)) (and (<= 0 ?v_0) (<= ?v_0 ?x)))) :pattern ((integralDiv ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (integralOr ?x ?y))) (=> (and (<= 0 ?x) (<= 0 ?y)) (and (<= ?x ?v_0) (<= ?y ?v_0)))) :pattern ((integralOr ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?y) (<= (integralAnd ?x ?y) ?y)) :pattern ((integralAnd ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (=> (<= 0 ?x) (<= (integralAnd ?x ?y) ?x)) :pattern ((integralAnd ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (=> (or (<= 0 ?x) (<= 0 ?y)) (<= 0 (integralAnd ?x ?y))) :pattern ((integralAnd ?x ?y)) ))) +(assert (forall ((?t Int)) (! (let ((?v_0 (classLiteral ?t))) (and (not (= ?v_0 null)) (= Smt.true (is ?v_0 T_java.lang.Class)) (isAllocated ?v_0 alloc))) :pattern ((classLiteral ?t)) ))) +(assert (forall ((?x Int) (?e Int)) (= (nonnullelements ?x ?e) (and (not (= ?x null)) (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i (arrayLength ?x))) (not (= (select1 (select1 ?e ?x) ?i) null)))))))) +(assert (forall ((?b Int) (?x Int) (?y Int)) (! (=> (not (= ?b Smt.true)) (= (termConditional ?b ?x ?y) ?y)) :pattern ((termConditional ?b ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (termConditional Smt.true ?x ?y) ?x) :pattern ((termConditional Smt.true ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (refNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((refNE ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (refEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((refEQ ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (integralNE ?x ?y) Smt.true) (not (= ?x ?y))) :pattern ((integralNE ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLT ?x ?y) Smt.true) (< ?x ?y)) :pattern ((integralLT ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (integralLE ?x ?y) Smt.true) (<= ?x ?y)) :pattern ((integralLE ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGT ?x ?y) Smt.true) (> ?x ?y)) :pattern ((integralGT ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (integralGE ?x ?y) Smt.true) (>= ?x ?y)) :pattern ((integralGE ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (let ((?v_0 (stringCat ?x ?y))) (and (not (= ?v_0 null)) (subtypes (typeof ?v_0) T_java.lang.String))) :pattern ((stringCat ?x ?y)) ))) +(assert (forall ((?x Int) (?y Int)) (! (= (= (integralEQ ?x ?y) Smt.true) (= ?x ?y)) :pattern ((integralEQ ?x ?y)) ))) +(assert (forall ((?a Int) (?b Int)) (= (boolOr ?a ?b) (or (= ?a Smt.true) (= ?b Smt.true))))) +(assert (forall ((?a Int)) (= (boolNot ?a) (not (= ?a Smt.true))))) +(assert (forall ((?a Int) (?b Int)) (= (boolNE ?a ?b) (not (= (= ?a Smt.true) (= ?b Smt.true)))))) +(assert (forall ((?a Int) (?b Int)) (= (boolImplies ?a ?b) (=> (= ?a Smt.true) (= ?b Smt.true))))) +(assert (forall ((?a Int) (?b Int)) (= (boolEq ?a ?b) (= (= ?a Smt.true) (= ?b Smt.true))))) +(assert (forall ((?a Int) (?b Int)) (= (boolAnd ?a ?b) (and (= ?a Smt.true) (= ?b Smt.true))))) +(assert (forall ((?x Int) (?y Int)) (let ((?v_0 (multiply ?x ?y))) (= (multiply (integralDiv ?v_0 ?y) ?y) ?v_0)))) +(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?j ?i) ?j) (integralMod ?i ?j)))) +(assert (forall ((?i Int) (?j Int)) (= (integralMod (+ ?i ?j) ?j) (integralMod ?i ?j)))) +(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< ?j 0) (and (< ?j ?v_0) (<= ?v_0 0)))) :pattern ((integralMod ?i ?j)) ))) +(assert (forall ((?i Int) (?j Int)) (! (let ((?v_0 (integralMod ?i ?j))) (=> (< 0 ?j) (and (<= 0 ?v_0) (< ?v_0 ?j)))) :pattern ((integralMod ?i ?j)) ))) +(assert (forall ((?i Int) (?j Int)) (! (= (+ (multiply (integralDiv ?i ?j) ?j) (integralMod ?i ?j)) ?i) :pattern ((integralMod ?i ?j)) :pattern ((integralDiv ?i ?j)) ))) +(assert (forall ((?s Int)) (! (=> (= Smt.true (isNewArray ?s)) (subtypes (typeof ?s) arrayType)) :pattern ((isNewArray ?s)) ))) +(assert (forall ((?t Int)) (! (subtypes (array ?t) arrayType) :pattern ((array ?t)) ))) +(assert (= arrayType (asChild arrayType T_java.lang.Object))) +(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (= (select1 (select1 ?e ?a) ?i) ?v) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeOne ?n) ?T ?v)) ))) +(assert (forall ((?a Int) (?a0 Int) (?b0 Int) (?e Int) (?n Int) (?s Int) (?T Int) (?v Int)) (! (= (arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v) (and (<= ?a0 (vAllocTime ?a)) (isAllocated ?a ?b0) (not (= ?a null)) (= (typeof ?a) ?T) (= (arrayLength ?a) ?n) (forall ((?i Int)) (! (let ((?v_0 (select1 (select1 ?e ?a) ?i))) (and (arrayFresh ?v_0 ?a0 ?b0 ?e ?s (elemtype ?T) ?v) (= (arrayParent ?v_0) ?a) (= (arrayPosition ?v_0) ?i))) :pattern ((select1 (select1 ?e ?a) ?i)) )))) :pattern ((arrayFresh ?a ?a0 ?b0 ?e (arrayShapeMore ?n ?s) ?T ?v)) ))) +(assert (forall ((?a Int)) (! (let ((?v_0 (arrayLength ?a))) (and (<= 0 ?v_0) (= Smt.true (is ?v_0 T_int)))) :pattern ((arrayLength ?a)) ))) +(assert (forall ((?x Int)) (! (=> (subtypes (typeof ?x) T_java.lang.Object) (lockLE null ?x)) :pattern ((lockLE null ?x)) :pattern ((lockLT null ?x)) :pattern ((lockLE ?x null)) :pattern ((lockLT ?x null)) ))) +(assert (forall ((?S Int) (?mu Int)) (let ((?v_0 (asLockSet ?S))) (=> (= (select1 ?v_0 ?mu) Smt.true) (lockLE ?mu (max ?v_0)))))) +(assert (forall ((?x Int) (?y Int)) (= (lockLT ?x ?y) (< ?x ?y)))) +(assert (forall ((?x Int) (?y Int)) (= (lockLE ?x ?y) (<= ?x ?y)))) +(assert (forall ((?S Int)) (! (= (select1 (asLockSet ?S) null) Smt.true) :pattern ((asLockSet ?S)) ))) +(assert (forall ((?S Int)) (let ((?v_0 (asLockSet ?S))) (= (select1 ?v_0 (max ?v_0)) Smt.true)))) +(assert (forall ((?a Int) (?e Int) (?i Int) (?a0 Int)) (! (=> (and (< (eClosedTime ?e) ?a0) (isAllocated ?a ?a0)) (isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) :pattern ((isAllocated (select1 (select1 ?e ?a) ?i) ?a0)) ))) +(assert (forall ((?x Int) (?f Int) (?a0 Int)) (! (=> (and (< (fClosedTime ?f) ?a0) (isAllocated ?x ?a0)) (isAllocated (select1 ?f ?x) ?a0)) :pattern ((isAllocated (select1 ?f ?x) ?a0)) ))) +(assert (forall ((?x Int) (?a0 Int)) (= (isAllocated ?x ?a0) (< (vAllocTime ?x) ?a0)))) +(assert (forall ((?e Int) (?a Int) (?i Int)) (! (= Smt.true (is (select1 (select1 (asElems ?e) ?a) ?i) (elemtype (typeof ?a)))) :pattern ((select1 (select1 (asElems ?e) ?a) ?i)) ))) +(assert (forall ((?f Int) (?t Int) (?x Int)) (! (= Smt.true (is (select1 (asField ?f ?t) ?x) ?t)) :pattern ((select1 (asField ?f ?t) ?x)) ))) +(assert (forall ((?x Int) (?t Int)) (! (=> (subtypes ?t T_java.lang.Object) (= (= Smt.true (is ?x ?t)) (or (= ?x null) (subtypes (typeof ?x) ?t)))) :pattern ((subtypes ?t T_java.lang.Object) (is ?x ?t)) ))) +(assert (< intLast longLast)) +(assert (< 1000000 intLast)) +(assert (< intFirst (- 1000000))) +(assert (< longFirst intFirst)) +(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_long)) (and (<= longFirst ?x) (<= ?x longLast))) :pattern ((is ?x T_long)) ))) +(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_int)) (and (<= intFirst ?x) (<= ?x intLast))) :pattern ((is ?x T_int)) ))) +(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_short)) (and (<= (- 32768) ?x) (<= ?x 32767))))) +(assert (forall ((?x Int)) (= (= Smt.true (is ?x T_byte)) (and (<= (- 128) ?x) (<= ?x 127))))) +(assert (forall ((?x Int)) (! (= (= Smt.true (is ?x T_char)) (and (<= 0 ?x) (<= ?x 65535))) :pattern ((is ?x T_char)) ))) +(assert (distinct bool_false Smt.true)) +(assert (forall ((?x Int) (?t Int)) (! (=> (= Smt.true (is ?x ?t)) (= (cast ?x ?t) ?x)) :pattern ((cast ?x ?t)) ))) +(assert (forall ((?x Int) (?t Int)) (! (= Smt.true (is (cast ?x ?t) ?t)) :pattern ((cast ?x ?t)) ))) +(assert (forall ((?t0 Int) (?t1 Int)) (! (let ((?v_0 (elemtype ?t0))) (= (subtypes ?t0 (array ?t1)) (and (= ?t0 (array ?v_0)) (subtypes ?v_0 ?t1)))) :pattern ((subtypes ?t0 (array ?t1))) ))) +(assert (forall ((?t Int)) (! (= (elemtype (array ?t)) ?t) :pattern ((elemtype (array ?t))) ))) +(assert (forall ((?t Int)) (! (subtypes (array ?t) T_java.lang.Cloneable) :pattern ((array ?t)) ))) +(assert (subtypes T_java.lang.Cloneable T_java.lang.Object)) +(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (let ((?v_0 (asChild ?t1 ?t2))) (=> (subtypes ?t0 ?v_0) (= (classDown ?t2 ?t0) ?v_0))))) +(assert (forall ((?t Int)) (! (=> (subtypes T_double ?t) (= ?t T_double)) :pattern ((subtypes T_double ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_float ?t) (= ?t T_float)) :pattern ((subtypes T_float ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_long ?t) (= ?t T_long)) :pattern ((subtypes T_long ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_int ?t) (= ?t T_int)) :pattern ((subtypes T_int ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_short ?t) (= ?t T_short)) :pattern ((subtypes T_short ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_byte ?t) (= ?t T_byte)) :pattern ((subtypes T_byte ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_char ?t) (= ?t T_char)) :pattern ((subtypes T_char ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes T_boolean ?t) (= ?t T_boolean)) :pattern ((subtypes T_boolean ?t)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_double) (= ?t T_double)) :pattern ((subtypes ?t T_double)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_float) (= ?t T_float)) :pattern ((subtypes ?t T_float)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_long) (= ?t T_long)) :pattern ((subtypes ?t T_long)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_int) (= ?t T_int)) :pattern ((subtypes ?t T_int)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_short) (= ?t T_short)) :pattern ((subtypes ?t T_short)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_byte) (= ?t T_byte)) :pattern ((subtypes ?t T_byte)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_char) (= ?t T_char)) :pattern ((subtypes ?t T_char)) ))) +(assert (forall ((?t Int)) (! (=> (subtypes ?t T_boolean) (= ?t T_boolean)) :pattern ((subtypes ?t T_boolean)) ))) +(assert (forall ((?t0 Int) (?t1 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) (= ?t0 ?t1)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t0)) ))) +(assert (forall ((?t0 Int) (?t1 Int) (?t2 Int)) (! (=> (and (subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) (subtypes ?t0 ?t2)) :pattern ((subtypes ?t0 ?t1) (subtypes ?t1 ?t2)) ))) +(assert (subtypes T_java.lang.Object T_java.lang.Object)) +(assert (forall ((?t Int)) (! (subtypes ?t ?t) :pattern ((subtypes ?t ?t)) ))) +(assert (forall ((?m Int) (?i Int) (?j Int) (?x Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?m ?i ?x) ?j) (select1 ?m ?j))))) +(assert (forall ((?m Int) (?i Int) (?x Int)) (= (select1 (store1 ?m ?i ?x) ?i) ?x))) +(assert (let ((?v_0 (not (= args_181.36 null)))) (let ((?v_1 (not ?v_0)) (?v_3 (arrayLength args_181.36))) (let ((?v_61 (not (= ?v_3 1)))) (let ((?v_29 (not ?v_61)) (?v_8 (= Smt.true Smt.true)) (?v_2 (<= 0 0)) (?v_4 (< 0 ?v_3)) (?v_30 (= treeName_186.1 (select1 (select1 elems args_181.36) 0))) (?v_5 (not (= treeName_186.1 null))) (?v_31 (< alloc after_189.25_189.25)) (?v_6 (not (= RES_189.25_189.25 null))) (?v_32 (not (isAllocated RES_189.25_189.25 alloc))) (?v_33 (= Smt.true (is RES_189.25_189.25 T_java.io.File))) (?v_34 (isAllocated RES_189.25_189.25 after_189.25_189.25)) (?v_35 (= EC_189.25_189.25 ecReturn)) (?v_36 (= (select1 owner_6.35.28 RES_189.25_189.25) null)) (?v_37 (= (typeof RES_189.25_189.25) T_java.io.File)) (?v_38 (< after_189.25_189.25 after_189.12_189.12)) (?v_7 (not (= RES_189.12_189.12 null))) (?v_39 (not (isAllocated RES_189.12_189.12 after_189.25_189.25))) (?v_40 (= Smt.true (is RES_189.12_189.12 T_javafe.filespace.FileTree))) (?v_41 (isAllocated RES_189.12_189.12 after_189.12_189.12)) (?v_42 (= EC_189.12_189.12 ecReturn)) (?v_43 (= (select1 owner_6.35.28 RES_189.12_189.12) null)) (?v_44 (= (typeof RES_189.12_189.12) T_javafe.filespace.FileTree)) (?v_45 (< after_189.12_189.12 after_192.22_192.22)) (?v_9 (not (= RES_192.22_192.22 null))) (?v_46 (not (isAllocated RES_192.22_192.22 after_189.12_189.12))) (?v_47 (= Smt.true (is RES_192.22_192.22 T_javafe.filespace.TreeWalker))) (?v_48 (isAllocated RES_192.22_192.22 after_192.22_192.22)) (?v_49 (= EC_192.22_192.22 ecReturn)) (?v_50 (= (select1 owner_6.35.28 RES_192.22_192.22) null)) (?v_51 (= (typeof RES_192.22_192.22) T_javafe.filespace.TreeWalker)) (?v_52 (= EC_192.22_192.22 EC_loopold)) (?v_53 (= moreElements_5.58.29 moreElements_loopold_5.58.29))) (let ((?v_12 (not ?v_9)) (?v_17 (= Smt.true (is RES_192.1_0_192.45_192.45 T_boolean))) (?v_10 (= EC_192.1_0_192.45_192.45 ecReturn)) (?v_11 (= Smt.true RES_192.1_0_192.45_192.45)) (?v_13 (= Smt.true (select1 moreElements_5.58.29 RES_192.22_192.22)))) (let ((?v_18 (=> ?v_10 (= ?v_11 ?v_13))) (?v_19 (= moreElements_192.1_0_193.28_5.89.17 (store1 moreElements_5.58.29 RES_192.22_192.22 after_193.28_192.1_0_193.28_5.89.17))) (?v_20 (= moreElements_192.1_0_193.28_5.89.17 (asField moreElements_192.1_0_193.28_5.89.17 T_boolean))) (?v_21 (= Smt.true (is RES_192.1_0_193.28_193.28 T_java.lang.Object))) (?v_22 (isAllocated RES_192.1_0_193.28_193.28 after_192.22_192.22)) (?v_14 (= EC_192.1_0_193.28_193.28 ecReturn)) (?v_15 (= RES_192.1_0_193.28_193.28 null))) (let ((?v_23 (=> ?v_14 (or (subtypes (typeof RES_192.1_0_193.28_193.28) (select1 elementType_5.74.27 RES_192.22_192.22)) ?v_15))) (?v_24 (=> (and ?v_14 (not (= Smt.true (select1 returnsNull_5.79.29 RES_192.22_192.22)))) (not ?v_15))) (?v_25 (forall ((?brokenObj_11_ Int)) (let ((?v_65 (= Smt.true (select1 lookAheadValid_4.40.20 ?brokenObj_11_))) (?v_66 (not (= (select1 lookAhead_4.43.19 ?brokenObj_11_) null)))) (=> (and (= Smt.true (is ?brokenObj_11_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_11_ null)) (=> ?v_65 (= (= Smt.true (select1 moreElements_5.58.29 ?brokenObj_11_)) ?v_66)) ?v_65) (= (= Smt.true (select1 moreElements_192.1_0_193.28_5.89.17 ?brokenObj_11_)) ?v_66))))) (?v_16 (= Smt.true (is RES_192.1_0_193.28_193.28 T_javafe.filespace.Tree))) (?v_26 (= subtree_192.1_0_193.5 (cast RES_192.1_0_193.28_193.28 T_javafe.filespace.Tree))) (?v_27 (not (= subtree_192.1_0_193.5 null))) (?v_54 (= Smt.true (is RES_192.1_0_194.32_194.32 T_java.lang.String))) (?v_55 (isAllocated RES_192.1_0_194.32_194.32 after_192.22_192.22)) (?v_28 (= EC_192.1_0_194.32_194.32 ecReturn))) (let ((?v_56 (=> ?v_28 (not (= RES_192.1_0_194.32_194.32 null)))) (?v_57 (= arg0_194.16_192.1_0_194.16_17.. (stringCat RES_192.1_0_194.32_194.32 S_194.56))) (?v_58 (= EC_192.1_0_194.16_194.16 ecReturn)) (?v_59 (= EC_192.1_1_192.45_192.45 ecReturn)) (?v_60 (= Smt.true RES_192.1_1_192.45_192.45))) (let ((?v_62 (or (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 (not ?v_11)) (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 ?v_9 ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 ?v_16 ?v_26 ?v_27 ?v_54 ?v_55 ?v_28 ?v_56 ?v_57 ?v_58 ?v_8 ?v_9 (= Smt.true (is RES_192.1_1_192.45_192.45 T_boolean)) ?v_59 (=> ?v_59 (= ?v_60 (= Smt.true (select1 moreElements_192.1_0_193.28_5.89.17 RES_192.22_192.22)))) (not ?v_60)))) (?v_63 (= L_192.1 L_192.1)) (?v_64 (= EC_182.16 ecReturn))) (not (=> (and (distinct ecReturn L_192.1) (not (= S_194.56 null)) (= (typeof S_194.56) T_java.lang.String)) (=> (and (= elementType_pre_5.74.27 elementType_5.74.27) (= elementType_5.74.27 (asField elementType_5.74.27 T_.TYPE)) (= owner_pre_6.35.28 owner_6.35.28) (= owner_6.35.28 (asField owner_6.35.28 T_java.lang.Object)) (< (fClosedTime owner_6.35.28) alloc) (= list_pre_210.13 list_210.13) (= list_210.13 (asField list_210.13 (array T_java.lang.Object))) (< (fClosedTime list_210.13) alloc) (= lookAheadValid_pre_4.40.20 lookAheadValid_4.40.20) (= lookAheadValid_4.40.20 (asField lookAheadValid_4.40.20 T_boolean)) (= remainingNodes_pre_48.26 remainingNodes_48.26) (= remainingNodes_48.26 (asField remainingNodes_48.26 T_java.util.Enumeration)) (< (fClosedTime remainingNodes_48.26) alloc) (= out_pre_16.83.49 out_16.83.49) (= Smt.true (is out_16.83.49 T_java.io.PrintStream)) (isAllocated out_16.83.49 alloc) (not (= out_16.83.49 null)) (= lookAhead_pre_4.43.19 lookAhead_4.43.19) (= lookAhead_4.43.19 (asField lookAhead_4.43.19 T_java.lang.Object)) (< (fClosedTime lookAhead_4.43.19) alloc) (= returnsNull_pre_5.79.29 returnsNull_5.79.29) (= returnsNull_5.79.29 (asField returnsNull_5.79.29 T_boolean)) (= moreElements_pre_5.58.29 moreElements_5.58.29) (= moreElements_5.58.29 (asField moreElements_5.58.29 T_boolean)) (= remainingChildren_pre_39.26 remainingChildren_39.26) (= remainingChildren_39.26 (asField remainingChildren_39.26 T_java.util.Enumeration)) (< (fClosedTime remainingChildren_39.26) alloc) (= elems_pre elems) (= elems (asElems elems)) (< (eClosedTime elems) alloc) (= LS (asLockSet LS)) (= alloc_pre alloc)) (not (and (= Smt.true (is args_181.36 (array T_java.lang.String))) (isAllocated args_181.36 alloc) (nonnullelements args_181.36 elems) (forall ((?brokenObj Int)) (=> (and (= Smt.true (is ?brokenObj T_javafe.filespace.TreeWalker)) (not (= ?brokenObj null))) (= (select1 elementType_5.74.27 (select1 remainingChildren_39.26 ?brokenObj)) T_javafe.filespace.Tree))) (forall ((?brokenObj_1_ Int)) (=> (and (= Smt.true (is ?brokenObj_1_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_1_ null))) (not (= (select1 remainingChildren_39.26 ?brokenObj_1_) null)))) (forall ((?brokenObj_2_ Int)) (=> (and (= Smt.true (is ?brokenObj_2_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_2_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 ?brokenObj_2_))))) (forall ((?brokenObj_3_ Int)) (=> (and (= Smt.true (is ?brokenObj_3_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_3_ null))) (= (select1 elementType_5.74.27 (select1 remainingNodes_48.26 ?brokenObj_3_)) T_javafe.filespace.Tree))) (forall ((?brokenObj_4_ Int)) (=> (and (= Smt.true (is ?brokenObj_4_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_4_ null)) (= Smt.true (select1 lookAheadValid_4.40.20 ?brokenObj_4_))) (= (= Smt.true (select1 moreElements_5.58.29 ?brokenObj_4_)) (not (= (select1 lookAhead_4.43.19 ?brokenObj_4_) null))))) (forall ((?brokenObj_5_ Int)) (=> (and (= Smt.true (is ?brokenObj_5_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_5_ null))) (not (= (select1 remainingNodes_48.26 ?brokenObj_5_) null)))) (forall ((?brokenObj_6_ Int)) (=> (and (= Smt.true (is ?brokenObj_6_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_6_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 (select1 remainingChildren_39.26 ?brokenObj_6_)))))) (forall ((?brokenObj_7_ Int)) (=> (and (= Smt.true (is ?brokenObj_7_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_7_ null))) (= (select1 elementType_5.74.27 ?brokenObj_7_) T_javafe.filespace.Tree))) (forall ((?brokenObj_8_ Int)) (let ((?v_67 (select1 lookAhead_4.43.19 ?brokenObj_8_))) (=> (and (= Smt.true (is ?brokenObj_8_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_8_ null))) (or (subtypes (typeof ?v_67) (select1 elementType_5.74.27 ?brokenObj_8_)) (= ?v_67 null))))) (forall ((?brokenObj_9_ Int)) (=> (and (= Smt.true (is ?brokenObj_9_ T_javafe.filespace.TreeWalker)) (not (= ?brokenObj_9_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 (select1 remainingNodes_48.26 ?brokenObj_9_)))))) (forall ((?brokenObj_10_ Int)) (=> (and (= Smt.true (is ?brokenObj_10_ T_javafe.filespace.LookAheadEnum)) (not (= ?brokenObj_10_ null))) (not (= Smt.true (select1 returnsNull_5.79.29 ?brokenObj_10_))))) (or ?v_1 (and ?v_0 ?v_29 ?v_8 (or ?v_1 (and ?v_0 (or (not ?v_2) (and ?v_2 (or (not ?v_4) (and ?v_4 ?v_30 (or (not ?v_5) (and ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 (or (not ?v_6) (and ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 (or (not ?v_7) (and ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 (or (and ?v_8 (or ?v_12 (and ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 (or ?v_12 (and ?v_9 (or (not ?v_13) (and ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 (or (not ?v_16) (and ?v_16 ?v_26 (not ?v_27)))))))))) (and ?v_8 ?v_9 ?v_17 ?v_10 ?v_18 ?v_11 ?v_9 ?v_13 ?v_19 ?v_20 ?v_21 ?v_22 ?v_14 ?v_23 ?v_24 ?v_25 ?v_16 ?v_26 ?v_27 ?v_54 ?v_55 ?v_28 ?v_56 ?v_57 ?v_58 ?v_8 ?v_12))))))))))))))) (and (or (and ?v_0 ?v_29 ?v_8 ?v_0 ?v_2 ?v_4 ?v_30 ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 ?v_62 ?v_63 (= EC L_192.1) ?v_64) (and ?v_0 (or (and ?v_61 ?v_8 (= EC_183.16_183.16 ecReturn) ?v_8 (= EC_182.16_1_ ecReturn)) (and ?v_29 ?v_8 ?v_0 ?v_2 ?v_4 ?v_30 ?v_5 ?v_31 ?v_6 ?v_32 ?v_33 ?v_34 ?v_35 ?v_36 ?v_37 ?v_6 ?v_38 ?v_7 ?v_39 ?v_40 ?v_41 ?v_42 ?v_43 ?v_44 ?v_7 ?v_45 ?v_9 ?v_46 ?v_47 ?v_48 ?v_49 ?v_50 ?v_51 ?v_52 ?v_53 ?v_62 (not ?v_63) (= EC_182.16_1_ L_192.1))) (= EC_182.16 EC_182.16_1_))) (not ?v_64)))))))))))))))))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2 b/test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2 new file mode 100644 index 000000000..6874c522e --- /dev/null +++ b/test/regress/regress0/quantifiers/qcft-smtlib3dbc51.smt2 @@ -0,0 +1,233 @@ +; COMMAND-LINE: --qcf-tconstraint +; EXPECT: unsat +(set-logic AUFLIRA) +(set-info :source |http://proval.lri.fr/why-benchmarks |) +(set-info :smt-lib-version 2.0) +(set-info :category "industrial") +(set-info :status unsat) +(declare-sort Unit 0) +(declare-sort c_unique 0) +(declare-sort c_ssorted 0) +(declare-sort c_type 0) +(declare-sort c_Boolean 0) +(declare-fun c_sort (c_type c_unique) c_ssorted) +(declare-fun c_Boolean_true () c_Boolean) +(declare-fun c_Boolean_false () c_Boolean) +(assert (forall ((?b_22_1 c_Boolean)) (or (= c_Boolean_true ?b_22_1) (= c_Boolean_false ?b_22_1)))) +(assert (not (= c_Boolean_true c_Boolean_false))) +(declare-fun int2U (Int) c_unique) +(declare-fun ss2Int (c_ssorted) Int) +(declare-fun real2U (Real) c_unique) +(declare-fun ss2Real (c_ssorted) Real) +(declare-fun bool2U (c_Boolean) c_unique) +(declare-fun ss2Bool (c_ssorted) c_Boolean) +(declare-fun c_int () c_type) +(declare-fun c_bool () c_type) +(declare-fun c_real () c_type) +(declare-fun c_unit () c_type) +(declare-fun c_ref (c_unique) c_unique) +(assert (forall ((?t_21_2 c_type)) (forall ((?x_20_3 c_unique)) (forall ((?y_19_4 c_unique)) (=> (= (c_sort ?t_21_2 ?x_20_3) (c_sort ?t_21_2 ?y_19_4)) (= ?x_20_3 ?y_19_4)))))) +(assert (forall ((?x_18_5 Int)) (= (ss2Int (c_sort c_int (int2U ?x_18_5))) ?x_18_5))) +(assert (forall ((?x_17_6 Int)) (forall ((?y_16_7 Int)) (=> (= (int2U ?x_17_6) (int2U ?y_16_7)) (= ?x_17_6 ?y_16_7))))) +(assert (forall ((?x_15_8 Real)) (forall ((?y_14_9 Real)) (=> (= (real2U ?x_15_8) (real2U ?y_14_9)) (= ?x_15_8 ?y_14_9))))) +(assert (forall ((?x_13_10 c_Boolean)) (forall ((?y_12_11 c_Boolean)) (=> (= (bool2U ?x_13_10) (bool2U ?y_12_11)) (= ?x_13_10 ?y_12_11))))) +(assert (forall ((?x_11_12 c_ssorted)) (forall ((?y_10_13 c_ssorted)) (=> (= (ss2Int ?x_11_12) (ss2Int ?y_10_13)) (= ?x_11_12 ?y_10_13))))) +(assert (forall ((?x_9_14 c_ssorted)) (forall ((?y_8_15 c_ssorted)) (=> (= (ss2Real ?x_9_14) (ss2Real ?y_8_15)) (= ?x_9_14 ?y_8_15))))) +(assert (forall ((?x_7_16 c_ssorted)) (forall ((?y_6_17 c_ssorted)) (=> (= (ss2Bool ?x_7_16) (ss2Bool ?y_6_17)) (= ?x_7_16 ?y_6_17))))) +(assert (forall ((?x_5_18 Real)) (= (ss2Real (c_sort c_real (real2U ?x_5_18))) ?x_5_18))) +(assert (forall ((?x_4_19 c_Boolean)) (= (ss2Bool (c_sort c_bool (bool2U ?x_4_19))) ?x_4_19))) +(assert (forall ((?x_3_20 c_unique)) (= (int2U (ss2Int (c_sort c_int ?x_3_20))) ?x_3_20))) +(assert (forall ((?x_2_21 c_unique)) (= (real2U (ss2Real (c_sort c_real ?x_2_21))) ?x_2_21))) +(assert (forall ((?x_1_22 c_unique)) (= (bool2U (ss2Bool (c_sort c_bool ?x_1_22))) ?x_1_22))) +(declare-fun eq_int (Int Int) Bool) +(declare-fun neq_int (Int Int) Bool) +(declare-fun lt_int_bool (Int Int) c_Boolean) +(declare-fun le_int_bool (Int Int) c_Boolean) +(declare-fun gt_int_bool (Int Int) c_Boolean) +(declare-fun ge_int_bool (Int Int) c_Boolean) +(declare-fun eq_int_bool (Int Int) c_Boolean) +(declare-fun neq_int_bool (Int Int) c_Boolean) +(assert (forall ((?x_40_23 Int)) (forall ((?y_39_24 Int)) (= (= (lt_int_bool ?x_40_23 ?y_39_24) c_Boolean_true) (< ?x_40_23 ?y_39_24))))) +(assert (forall ((?x_42_25 Int)) (forall ((?y_41_26 Int)) (= (= (le_int_bool ?x_42_25 ?y_41_26) c_Boolean_true) (<= ?x_42_25 ?y_41_26))))) +(assert (forall ((?x_44_27 Int)) (forall ((?y_43_28 Int)) (= (= (gt_int_bool ?x_44_27 ?y_43_28) c_Boolean_true) (> ?x_44_27 ?y_43_28))))) +(assert (forall ((?x_46_29 Int)) (forall ((?y_45_30 Int)) (= (= (ge_int_bool ?x_46_29 ?y_45_30) c_Boolean_true) (>= ?x_46_29 ?y_45_30))))) +(assert (forall ((?x_48_31 Int)) (forall ((?y_47_32 Int)) (= (= (eq_int_bool ?x_48_31 ?y_47_32) c_Boolean_true) (= ?x_48_31 ?y_47_32))))) +(assert (forall ((?x_50_33 Int)) (forall ((?y_49_34 Int)) (= (= (neq_int_bool ?x_50_33 ?y_49_34) c_Boolean_true) (not (= ?x_50_33 ?y_49_34)))))) +(declare-fun add_real (Real Real) Real) +(declare-fun sub_real (Real Real) Real) +(declare-fun mul_real (Real Real) Real) +(declare-fun div_real (Real Real) Real) +(declare-fun pow_real (Real Real) Real) +(declare-fun neg_real (Real) Real) +(declare-fun abs_real (Real) Real) +(declare-fun sqrt_real (Real) Real) +(declare-fun real_of_int (Int) Real) +(declare-fun int_of_real (Real) Int) +(declare-fun lt_real (Real Real) Bool) +(declare-fun le_real (Real Real) Bool) +(declare-fun gt_real (Real Real) Bool) +(declare-fun ge_real (Real Real) Bool) +(declare-fun eq_real (Real Real) Bool) +(declare-fun neq_real (Real Real) Bool) +(declare-fun eq_bool (c_Boolean c_Boolean) Bool) +(declare-fun neq_bool (c_Boolean c_Boolean) Bool) +(declare-fun eq_unit (c_ssorted c_ssorted) Bool) +(declare-fun neq_unit (c_ssorted c_ssorted) Bool) +(declare-fun smtlib__ite (c_Boolean c_ssorted c_ssorted) c_unique) +(assert (forall ((?t_1_76_35 c_type)) (forall ((?x_75_36 c_unique)) (forall ((?y_74_37 c_unique)) (= (smtlib__ite c_Boolean_true (c_sort ?t_1_76_35 ?x_75_36) (c_sort ?t_1_76_35 ?y_74_37)) ?x_75_36))))) +(assert (forall ((?t_2_79_38 c_type)) (forall ((?x_78_39 c_unique)) (forall ((?y_77_40 c_unique)) (= (smtlib__ite c_Boolean_false (c_sort ?t_2_79_38 ?x_78_39) (c_sort ?t_2_79_38 ?y_77_40)) ?y_77_40))))) +(declare-fun bw_compl (Int) Int) +(declare-fun bw_and (Int Int) Int) +(declare-fun bw_xor (Int Int) Int) +(declare-fun bw_or (Int Int) Int) +(declare-fun lsl (Int Int) Int) +(declare-fun lsr (Int Int) Int) +(declare-fun non_int (Int) Int) +(declare-fun type_pointer (c_type) c_type) +(declare-fun type_addr (c_type) c_type) +(declare-fun type_alloc_table () c_type) +(declare-fun block_length (c_ssorted c_ssorted) Int) +(declare-fun base_addr (c_ssorted) c_unique) +(declare-fun offset (c_ssorted) Int) +(declare-fun shift (c_ssorted Int) c_unique) +(declare-fun sub_pointer (c_ssorted c_ssorted) Int) +(declare-fun lt_pointer (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_3_88_41 c_type)) (forall ((?p1_87_42 c_unique)) (forall ((?p2_86_43 c_unique)) (let ((?v_0 (type_pointer ?t_3_88_41))) (let ((?v_1 (c_sort ?v_0 ?p1_87_42)) (?v_2 (c_sort ?v_0 ?p2_86_43))) (= (lt_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (< (offset ?v_1) (offset ?v_2)))))))))) +(declare-fun le_pointer (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_4_91_44 c_type)) (forall ((?p1_90_45 c_unique)) (forall ((?p2_89_46 c_unique)) (let ((?v_0 (type_pointer ?t_4_91_44))) (let ((?v_1 (c_sort ?v_0 ?p1_90_45)) (?v_2 (c_sort ?v_0 ?p2_89_46))) (= (le_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (<= (offset ?v_1) (offset ?v_2)))))))))) +(declare-fun gt_pointer (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_5_94_47 c_type)) (forall ((?p1_93_48 c_unique)) (forall ((?p2_92_49 c_unique)) (let ((?v_0 (type_pointer ?t_5_94_47))) (let ((?v_1 (c_sort ?v_0 ?p1_93_48)) (?v_2 (c_sort ?v_0 ?p2_92_49))) (= (gt_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (> (offset ?v_1) (offset ?v_2)))))))))) +(declare-fun ge_pointer (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_6_97_50 c_type)) (forall ((?p1_96_51 c_unique)) (forall ((?p2_95_52 c_unique)) (let ((?v_0 (type_pointer ?t_6_97_50))) (let ((?v_1 (c_sort ?v_0 ?p1_96_51)) (?v_2 (c_sort ?v_0 ?p2_95_52))) (= (ge_pointer ?v_1 ?v_2) (and (= (base_addr ?v_1) (base_addr ?v_2)) (>= (offset ?v_1) (offset ?v_2)))))))))) +(declare-fun valid (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_7_104_53 c_type)) (forall ((?a_103_54 c_unique)) (forall ((?p_102_55 c_unique)) (let ((?v_2 (c_sort type_alloc_table ?a_103_54)) (?v_0 (c_sort (type_pointer ?t_7_104_53) ?p_102_55))) (let ((?v_1 (offset ?v_0))) (= (valid ?v_2 ?v_0) (and (<= 0 ?v_1) (< ?v_1 (block_length ?v_2 ?v_0)))))))))) +(declare-fun valid_index (c_ssorted c_ssorted Int) Bool) +(assert (forall ((?t_8_108_56 c_type)) (forall ((?a_107_57 c_unique)) (forall ((?p_106_58 c_unique)) (forall ((?i_105_59 Int)) (let ((?v_2 (c_sort type_alloc_table ?a_107_57)) (?v_0 (c_sort (type_pointer ?t_8_108_56) ?p_106_58))) (let ((?v_1 (+ (offset ?v_0) ?i_105_59))) (= (valid_index ?v_2 ?v_0 ?i_105_59) (and (<= 0 ?v_1) (< ?v_1 (block_length ?v_2 ?v_0))))))))))) +(declare-fun valid_range (c_ssorted c_ssorted Int Int) Bool) +(assert (forall ((?t_9_113_60 c_type)) (forall ((?a_112_61 c_unique)) (forall ((?p_111_62 c_unique)) (forall ((?i_110_63 Int)) (forall ((?j_109_64 Int)) (let ((?v_2 (c_sort type_alloc_table ?a_112_61)) (?v_0 (c_sort (type_pointer ?t_9_113_60) ?p_111_62))) (let ((?v_1 (offset ?v_0))) (= (valid_range ?v_2 ?v_0 ?i_110_63 ?j_109_64) (and (<= 0 (+ ?v_1 ?i_110_63)) (< (+ ?v_1 ?j_109_64) (block_length ?v_2 ?v_0)))))))))))) +(assert (forall ((?t_10_116_65 c_type)) (forall ((?p_115_66 c_unique)) (forall ((?i_114_67 Int)) (let ((?v_0 (type_pointer ?t_10_116_65))) (let ((?v_1 (c_sort ?v_0 ?p_115_66))) (= (offset (c_sort ?v_0 (shift ?v_1 ?i_114_67))) (+ (offset ?v_1) ?i_114_67)))))))) +(assert (forall ((?t_11_118_68 c_type)) (forall ((?p_117_69 c_unique)) (= (shift (c_sort (type_pointer ?t_11_118_68) ?p_117_69) 0) ?p_117_69)))) +(assert (forall ((?t_12_122_70 c_type)) (forall ((?p_121_71 c_unique)) (forall ((?i_120_72 Int)) (forall ((?j_119_73 Int)) (let ((?v_0 (type_pointer ?t_12_122_70))) (let ((?v_1 (c_sort ?v_0 ?p_121_71))) (= (shift (c_sort ?v_0 (shift ?v_1 ?i_120_72)) ?j_119_73) (shift ?v_1 (+ ?i_120_72 ?j_119_73)))))))))) +(assert (forall ((?t_13_125_74 c_type)) (forall ((?p_124_75 c_unique)) (forall ((?i_123_76 Int)) (let ((?v_0 (type_pointer ?t_13_125_74))) (let ((?v_1 (c_sort ?v_0 ?p_124_75))) (= (base_addr (c_sort ?v_0 (shift ?v_1 ?i_123_76))) (base_addr ?v_1)))))))) +(assert (forall ((?t_14_129_77 c_type)) (forall ((?a_128_78 c_unique)) (forall ((?p_127_79 c_unique)) (forall ((?i_126_80 Int)) (let ((?v_1 (c_sort type_alloc_table ?a_128_78)) (?v_0 (type_pointer ?t_14_129_77))) (let ((?v_2 (c_sort ?v_0 ?p_127_79))) (= (block_length ?v_1 (c_sort ?v_0 (shift ?v_2 ?i_126_80))) (block_length ?v_1 ?v_2))))))))) +(assert (forall ((?t_15_133_81 c_type)) (forall ((?a_132_82 c_unique)) (forall ((?p1_131_83 c_unique)) (forall ((?p2_130_84 c_unique)) (let ((?v_0 (type_pointer ?t_15_133_81))) (let ((?v_1 (c_sort ?v_0 ?p1_131_83)) (?v_3 (c_sort ?v_0 ?p2_130_84)) (?v_2 (c_sort type_alloc_table ?a_132_82))) (=> (= (base_addr ?v_1) (base_addr ?v_3)) (= (block_length ?v_2 ?v_1) (block_length ?v_2 ?v_3)))))))))) +(assert (forall ((?t_16_136_85 c_type)) (forall ((?p1_135_86 c_unique)) (forall ((?p2_134_87 c_unique)) (let ((?v_0 (type_pointer ?t_16_136_85))) (let ((?v_1 (c_sort ?v_0 ?p1_135_86)) (?v_2 (c_sort ?v_0 ?p2_134_87))) (=> (and (= (base_addr ?v_1) (base_addr ?v_2)) (= (offset ?v_1) (offset ?v_2))) (= ?p1_135_86 ?p2_134_87)))))))) +(assert (forall ((?t_17_139_88 c_type)) (forall ((?p1_138_89 c_unique)) (forall ((?p2_137_90 c_unique)) (let ((?v_0 (type_pointer ?t_17_139_88))) (let ((?v_1 (c_sort ?v_0 ?p1_138_89)) (?v_2 (c_sort ?v_0 ?p2_137_90))) (=> (= ?p1_138_89 ?p2_137_90) (and (= (base_addr ?v_1) (base_addr ?v_2)) (= (offset ?v_1) (offset ?v_2)))))))))) +(assert (forall ((?t_18_144_91 c_type)) (forall ((?p1_143_92 c_unique)) (forall ((?p2_142_93 c_unique)) (forall ((?i_141_94 Int)) (forall ((?j_140_95 Int)) (let ((?v_0 (type_pointer ?t_18_144_91))) (let ((?v_1 (c_sort ?v_0 ?p1_143_92)) (?v_2 (c_sort ?v_0 ?p2_142_93))) (=> (not (= (base_addr ?v_1) (base_addr ?v_2))) (not (= (shift ?v_1 ?i_141_94) (shift ?v_2 ?j_140_95)))))))))))) +(assert (forall ((?t_19_149_96 c_type)) (forall ((?p1_148_97 c_unique)) (forall ((?p2_147_98 c_unique)) (forall ((?i_146_99 Int)) (forall ((?j_145_100 Int)) (let ((?v_0 (type_pointer ?t_19_149_96))) (let ((?v_1 (c_sort ?v_0 ?p1_148_97)) (?v_2 (c_sort ?v_0 ?p2_147_98))) (=> (not (= (+ (offset ?v_1) ?i_146_99) (+ (offset ?v_2) ?j_145_100))) (not (= (shift ?v_1 ?i_146_99) (shift ?v_2 ?j_145_100)))))))))))) +(assert (forall ((?t_20_154_101 c_type)) (forall ((?p1_153_102 c_unique)) (forall ((?p2_152_103 c_unique)) (forall ((?i_151_104 Int)) (forall ((?j_150_105 Int)) (let ((?v_0 (type_pointer ?t_20_154_101))) (let ((?v_1 (c_sort ?v_0 ?p1_153_102)) (?v_2 (c_sort ?v_0 ?p2_152_103))) (=> (= (base_addr ?v_1) (base_addr ?v_2)) (=> (= (+ (offset ?v_1) ?i_151_104) (+ (offset ?v_2) ?j_150_105)) (= (shift ?v_1 ?i_151_104) (shift ?v_2 ?j_150_105)))))))))))) +(assert (forall ((?t_21_158_106 c_type)) (forall ((?a_157_107 c_unique)) (forall ((?p_156_108 c_unique)) (forall ((?i_155_109 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_157_107)) (?v_1 (type_pointer ?t_21_158_106))) (let ((?v_2 (c_sort ?v_1 ?p_156_108))) (=> (valid_index ?v_0 ?v_2 ?i_155_109) (valid ?v_0 (c_sort ?v_1 (shift ?v_2 ?i_155_109))))))))))) +(assert (forall ((?t_22_164_110 c_type)) (forall ((?a_163_111 c_unique)) (forall ((?p_162_112 c_unique)) (forall ((?i_161_113 Int)) (forall ((?j_160_114 Int)) (forall ((?k_159_115 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_163_111)) (?v_1 (type_pointer ?t_22_164_110))) (let ((?v_2 (c_sort ?v_1 ?p_162_112))) (=> (valid_range ?v_0 ?v_2 ?i_161_113 ?j_160_114) (=> (and (<= ?i_161_113 ?k_159_115) (<= ?k_159_115 ?j_160_114)) (valid ?v_0 (c_sort ?v_1 (shift ?v_2 ?k_159_115)))))))))))))) +(assert (forall ((?t_23_169_116 c_type)) (forall ((?a_168_117 c_unique)) (forall ((?p_167_118 c_unique)) (forall ((?i_166_119 Int)) (forall ((?j_165_120 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_168_117)) (?v_1 (c_sort (type_pointer ?t_23_169_116) ?p_167_118))) (=> (valid_range ?v_0 ?v_1 ?i_166_119 ?j_165_120) (=> (and (<= ?i_166_119 0) (<= 0 ?j_165_120)) (valid ?v_0 ?v_1)))))))))) +(assert (forall ((?t_24_175_121 c_type)) (forall ((?a_174_122 c_unique)) (forall ((?p_173_123 c_unique)) (forall ((?i_172_124 Int)) (forall ((?j_171_125 Int)) (forall ((?k_170_126 Int)) (let ((?v_0 (c_sort type_alloc_table ?a_174_122)) (?v_1 (c_sort (type_pointer ?t_24_175_121) ?p_173_123))) (=> (valid_range ?v_0 ?v_1 ?i_172_124 ?j_171_125) (=> (and (<= ?i_172_124 ?k_170_126) (<= ?k_170_126 ?j_171_125)) (valid_index ?v_0 ?v_1 ?k_170_126))))))))))) +(assert (forall ((?t_25_178_127 c_type)) (forall ((?p1_177_128 c_unique)) (forall ((?p2_176_129 c_unique)) (let ((?v_0 (type_pointer ?t_25_178_127))) (let ((?v_1 (c_sort ?v_0 ?p1_177_128)) (?v_2 (c_sort ?v_0 ?p2_176_129))) (=> (= (base_addr ?v_1) (base_addr ?v_2)) (= (sub_pointer ?v_1 ?v_2) (- (offset ?v_1) (offset ?v_2)))))))))) +(declare-fun type_memory (c_type c_type) c_type) +(declare-fun acc (c_ssorted c_ssorted) c_unique) +(declare-fun upd (c_ssorted c_ssorted c_ssorted) c_unique) +(assert (forall ((?t_27_212_130 c_type)) (forall ((?t_26_211_131 c_type)) (forall ((?m_210_132 c_unique)) (forall ((?p_209_133 c_unique)) (forall ((?a_208_134 c_unique)) (let ((?v_0 (type_memory ?t_26_211_131 ?t_27_212_130)) (?v_1 (c_sort (type_pointer ?t_27_212_130) ?p_209_133))) (= (acc (c_sort ?v_0 (upd (c_sort ?v_0 ?m_210_132) ?v_1 (c_sort ?t_26_211_131 ?a_208_134))) ?v_1) ?a_208_134)))))))) +(assert (forall ((?t_29_218_135 c_type)) (forall ((?t_28_217_136 c_type)) (forall ((?m_216_137 c_unique)) (forall ((?p1_215_138 c_unique)) (forall ((?p2_214_139 c_unique)) (forall ((?a_213_140 c_unique)) (let ((?v_0 (type_memory ?t_28_217_136 ?t_29_218_135))) (let ((?v_2 (c_sort ?v_0 ?m_216_137)) (?v_1 (type_pointer ?t_29_218_135))) (let ((?v_3 (c_sort ?v_1 ?p2_214_139))) (=> (not (= ?p1_215_138 ?p2_214_139)) (= (acc (c_sort ?v_0 (upd ?v_2 (c_sort ?v_1 ?p1_215_138) (c_sort ?t_28_217_136 ?a_213_140))) ?v_3) (acc ?v_2 ?v_3))))))))))))) +(assert (not (= c_Boolean_false c_Boolean_true))) +(declare-fun type_pset (c_type) c_type) +(declare-fun pset_empty () c_unique) +(declare-fun pset_singleton (c_ssorted) c_unique) +(declare-fun pset_star (c_ssorted c_ssorted) c_unique) +(declare-fun pset_all (c_ssorted) c_unique) +(declare-fun pset_range (c_ssorted Int Int) c_unique) +(declare-fun pset_range_left (c_ssorted Int) c_unique) +(declare-fun pset_range_right (c_ssorted Int) c_unique) +(declare-fun pset_acc_all (c_ssorted c_ssorted) c_unique) +(declare-fun pset_acc_range (c_ssorted c_ssorted Int Int) c_unique) +(declare-fun pset_acc_range_left (c_ssorted c_ssorted Int) c_unique) +(declare-fun pset_acc_range_right (c_ssorted c_ssorted Int) c_unique) +(declare-fun pset_union (c_ssorted c_ssorted) c_unique) +(declare-fun not_in_pset (c_ssorted c_ssorted) Bool) +(declare-fun not_assigns (c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?t_31_225_141 c_type)) (forall ((?t_30_224_142 c_type)) (forall ((?a_223_143 c_unique)) (forall ((?m1_222_144 c_unique)) (forall ((?m2_221_145 c_unique)) (forall ((?l_220_146 c_unique)) (let ((?v_0 (type_memory ?t_30_224_142 ?t_31_225_141))) (= (not_assigns (c_sort type_alloc_table ?a_223_143) (c_sort ?v_0 ?m1_222_144) (c_sort ?v_0 ?m2_221_145) (c_sort (type_pset ?t_31_225_141) ?l_220_146)) (forall ((?p_219_147 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_31_225_141) ?p_219_147))) (=> (valid (c_sort type_alloc_table ?a_223_143) ?v_1) (=> (not_in_pset ?v_1 (c_sort (type_pset ?t_31_225_141) ?l_220_146)) (= (acc (c_sort ?v_0 ?m2_221_145) ?v_1) (acc (c_sort ?v_0 ?m1_222_144) ?v_1))))))))))))))) +(assert (forall ((?t_32_227_148 c_type)) (forall ((?p_226_149 c_unique)) (not_in_pset (c_sort (type_pointer ?t_32_227_148) ?p_226_149) (c_sort (type_pset ?t_32_227_148) pset_empty))))) +(assert (forall ((?t_33_230_150 c_type)) (forall ((?p1_229_151 c_unique)) (forall ((?p2_228_152 c_unique)) (let ((?v_0 (type_pointer ?t_33_230_150))) (=> (not (= ?p1_229_151 ?p2_228_152)) (not_in_pset (c_sort ?v_0 ?p1_229_151) (c_sort (type_pset ?t_33_230_150) (pset_singleton (c_sort ?v_0 ?p2_228_152)))))))))) +(assert (forall ((?t_34_233_153 c_type)) (forall ((?p1_232_154 c_unique)) (forall ((?p2_231_155 c_unique)) (let ((?v_0 (type_pointer ?t_34_233_153))) (=> (not_in_pset (c_sort ?v_0 ?p1_232_154) (c_sort (type_pset ?t_34_233_153) (pset_singleton (c_sort ?v_0 ?p2_231_155)))) (not (= ?p1_232_154 ?p2_231_155)))))))) +(assert (forall ((?t_35_235_156 c_type)) (forall ((?p_234_157 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_35_235_156) ?p_234_157))) (not (not_in_pset ?v_0 (c_sort (type_pset ?t_35_235_156) (pset_singleton ?v_0)))))))) +(assert (forall ((?t_36_239_158 c_type)) (forall ((?l1_238_159 c_unique)) (forall ((?l2_237_160 c_unique)) (forall ((?p_236_161 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_36_239_158) ?p_236_161)) (?v_1 (type_pset ?t_36_239_158))) (let ((?v_2 (c_sort ?v_1 ?l1_238_159)) (?v_3 (c_sort ?v_1 ?l2_237_160))) (=> (and (not_in_pset ?v_0 ?v_2) (not_in_pset ?v_0 ?v_3)) (not_in_pset ?v_0 (c_sort ?v_1 (pset_union ?v_2 ?v_3))))))))))) +(assert (forall ((?t_37_243_162 c_type)) (forall ((?l1_242_163 c_unique)) (forall ((?l2_241_164 c_unique)) (forall ((?p_240_165 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_37_243_162) ?p_240_165)) (?v_0 (type_pset ?t_37_243_162))) (let ((?v_2 (c_sort ?v_0 ?l1_242_163))) (=> (not_in_pset ?v_1 (c_sort ?v_0 (pset_union ?v_2 (c_sort ?v_0 ?l2_241_164)))) (not_in_pset ?v_1 ?v_2))))))))) +(assert (forall ((?t_38_247_166 c_type)) (forall ((?l1_246_167 c_unique)) (forall ((?l2_245_168 c_unique)) (forall ((?p_244_169 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_38_247_166) ?p_244_169)) (?v_0 (type_pset ?t_38_247_166))) (let ((?v_2 (c_sort ?v_0 ?l2_245_168))) (=> (not_in_pset ?v_1 (c_sort ?v_0 (pset_union (c_sort ?v_0 ?l1_246_167) ?v_2))) (not_in_pset ?v_1 ?v_2))))))))) +(assert (forall ((?t_40_253_170 c_type)) (forall ((?t_39_252_171 c_type)) (forall ((?l_251_172 c_unique)) (forall ((?m_250_173 c_unique)) (forall ((?p_249_174 c_unique)) (let ((?v_0 (type_pointer ?t_40_253_170))) (=> (forall ((?p1_248_175 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_39_252_171) ?p1_248_175))) (=> (= ?p_249_174 (acc (c_sort (type_memory ?v_0 ?t_39_252_171) ?m_250_173) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_39_252_171) ?l_251_172))))) (not_in_pset (c_sort ?v_0 ?p_249_174) (c_sort (type_pset ?t_40_253_170) (pset_star (c_sort (type_pset ?t_39_252_171) ?l_251_172) (c_sort (type_memory ?v_0 ?t_39_252_171) ?m_250_173)))))))))))) +(assert (forall ((?t_42_259_176 c_type)) (forall ((?t_41_258_177 c_type)) (forall ((?l_257_178 c_unique)) (forall ((?m_256_179 c_unique)) (forall ((?p_255_180 c_unique)) (let ((?v_0 (type_pointer ?t_42_259_176))) (=> (not_in_pset (c_sort ?v_0 ?p_255_180) (c_sort (type_pset ?t_42_259_176) (pset_star (c_sort (type_pset ?t_41_258_177) ?l_257_178) (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179)))) (forall ((?p1_254_181 c_unique)) (let ((?v_1 (c_sort (type_pointer ?t_41_258_177) ?p1_254_181))) (=> (= ?p_255_180 (acc (c_sort (type_memory ?v_0 ?t_41_258_177) ?m_256_179) ?v_1)) (not_in_pset ?v_1 (c_sort (type_pset ?t_41_258_177) ?l_257_178))))))))))))) +(assert (forall ((?t_43_263_182 c_type)) (forall ((?p_262_183 c_unique)) (forall ((?l_261_184 c_unique)) (let ((?v_0 (type_pset ?t_43_263_182))) (=> (forall ((?p1_260_185 c_unique)) (let ((?v_1 (type_pointer ?t_43_263_182))) (let ((?v_2 (c_sort ?v_1 ?p1_260_185))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_261_184))) (not (= (base_addr (c_sort ?v_1 ?p_262_183)) (base_addr ?v_2))))))) (not_in_pset (c_sort (type_pointer ?t_43_263_182) ?p_262_183) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_261_184)))))))))) +(assert (forall ((?t_44_267_186 c_type)) (forall ((?p_266_187 c_unique)) (forall ((?l_265_188 c_unique)) (let ((?v_0 (type_pset ?t_44_267_186))) (=> (not_in_pset (c_sort (type_pointer ?t_44_267_186) ?p_266_187) (c_sort ?v_0 (pset_all (c_sort ?v_0 ?l_265_188)))) (forall ((?p1_264_189 c_unique)) (let ((?v_1 (type_pointer ?t_44_267_186))) (let ((?v_2 (c_sort ?v_1 ?p1_264_189))) (=> (not (not_in_pset ?v_2 (c_sort ?v_0 ?l_265_188))) (not (= (base_addr (c_sort ?v_1 ?p_266_187)) (base_addr ?v_2))))))))))))) +(assert (forall ((?t_45_274_190 c_type)) (forall ((?p_273_191 c_unique)) (forall ((?l_272_192 c_unique)) (forall ((?a_271_193 Int)) (forall ((?b_270_194 Int)) (let ((?v_0 (type_pset ?t_45_274_190))) (=> (forall ((?p1_269_195 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) (c_sort ?v_0 ?l_272_192)) (forall ((?i_268_196 Int)) (=> (and (<= ?a_271_193 ?i_268_196) (<= ?i_268_196 ?b_270_194)) (not (= ?p_273_191 (shift (c_sort (type_pointer ?t_45_274_190) ?p1_269_195) ?i_268_196))))))) (not_in_pset (c_sort (type_pointer ?t_45_274_190) ?p_273_191) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_272_192) ?a_271_193 ?b_270_194))))))))))) +(assert (forall ((?t_46_281_197 c_type)) (forall ((?p_280_198 c_unique)) (forall ((?l_279_199 c_unique)) (forall ((?a_278_200 Int)) (forall ((?b_277_201 Int)) (let ((?v_0 (type_pset ?t_46_281_197))) (=> (not_in_pset (c_sort (type_pointer ?t_46_281_197) ?p_280_198) (c_sort ?v_0 (pset_range (c_sort ?v_0 ?l_279_199) ?a_278_200 ?b_277_201))) (forall ((?p1_276_202 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_46_281_197) ?p1_276_202) (c_sort ?v_0 ?l_279_199))) (forall ((?i_275_203 Int)) (=> (and (<= ?a_278_200 ?i_275_203) (<= ?i_275_203 ?b_277_201)) (not (= (shift (c_sort (type_pointer ?t_46_281_197) ?p1_276_202) ?i_275_203) ?p_280_198)))))))))))))) +(assert (forall ((?t_47_287_204 c_type)) (forall ((?p_286_205 c_unique)) (forall ((?l_285_206 c_unique)) (forall ((?a_284_207 Int)) (let ((?v_0 (type_pset ?t_47_287_204))) (=> (forall ((?p1_283_208 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_47_287_204) ?p1_283_208) (c_sort ?v_0 ?l_285_206)) (forall ((?i_282_209 Int)) (=> (<= ?i_282_209 ?a_284_207) (not (= ?p_286_205 (shift (c_sort (type_pointer ?t_47_287_204) ?p1_283_208) ?i_282_209))))))) (not_in_pset (c_sort (type_pointer ?t_47_287_204) ?p_286_205) (c_sort ?v_0 (pset_range_left (c_sort ?v_0 ?l_285_206) ?a_284_207)))))))))) +(assert (forall ((?t_48_293_210 c_type)) (forall ((?p_292_211 c_unique)) (forall ((?l_291_212 c_unique)) (forall ((?a_290_213 Int)) (let ((?v_0 (type_pset ?t_48_293_210))) (=> (not_in_pset (c_sort (type_pointer ?t_48_293_210) ?p_292_211) (c_sort ?v_0 (pset_range_left (c_sort ?v_0 ?l_291_212) ?a_290_213))) (forall ((?p1_289_214 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_48_293_210) ?p1_289_214) (c_sort ?v_0 ?l_291_212))) (forall ((?i_288_215 Int)) (=> (<= ?i_288_215 ?a_290_213) (not (= (shift (c_sort (type_pointer ?t_48_293_210) ?p1_289_214) ?i_288_215) ?p_292_211))))))))))))) +(assert (forall ((?t_49_299_216 c_type)) (forall ((?p_298_217 c_unique)) (forall ((?l_297_218 c_unique)) (forall ((?a_296_219 Int)) (let ((?v_0 (type_pset ?t_49_299_216))) (=> (forall ((?p1_295_220 c_unique)) (or (not_in_pset (c_sort (type_pointer ?t_49_299_216) ?p1_295_220) (c_sort ?v_0 ?l_297_218)) (forall ((?i_294_221 Int)) (=> (<= ?a_296_219 ?i_294_221) (not (= ?p_298_217 (shift (c_sort (type_pointer ?t_49_299_216) ?p1_295_220) ?i_294_221))))))) (not_in_pset (c_sort (type_pointer ?t_49_299_216) ?p_298_217) (c_sort ?v_0 (pset_range_right (c_sort ?v_0 ?l_297_218) ?a_296_219)))))))))) +(assert (forall ((?t_50_305_222 c_type)) (forall ((?p_304_223 c_unique)) (forall ((?l_303_224 c_unique)) (forall ((?a_302_225 Int)) (let ((?v_0 (type_pset ?t_50_305_222))) (=> (not_in_pset (c_sort (type_pointer ?t_50_305_222) ?p_304_223) (c_sort ?v_0 (pset_range_right (c_sort ?v_0 ?l_303_224) ?a_302_225))) (forall ((?p1_301_226 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_50_305_222) ?p1_301_226) (c_sort ?v_0 ?l_303_224))) (forall ((?i_300_227 Int)) (=> (<= ?a_302_225 ?i_300_227) (not (= (shift (c_sort (type_pointer ?t_50_305_222) ?p1_301_226) ?i_300_227) ?p_304_223))))))))))))) +(assert (forall ((?t_52_312_228 c_type)) (forall ((?t_51_311_229 c_type)) (forall ((?p_310_230 c_unique)) (forall ((?l_309_231 c_unique)) (forall ((?m_308_232 c_unique)) (let ((?v_0 (type_pointer ?t_51_311_229))) (=> (forall ((?p1_307_233 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_52_312_228) ?p1_307_233) (c_sort (type_pset ?t_52_312_228) ?l_309_231))) (forall ((?i_306_234 Int)) (let ((?v_1 (type_pointer ?t_52_312_228))) (not (= ?p_310_230 (acc (c_sort (type_memory ?v_0 ?t_52_312_228) ?m_308_232) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_307_233) ?i_306_234))))))))) (not_in_pset (c_sort ?v_0 ?p_310_230) (c_sort (type_pset ?t_51_311_229) (pset_acc_all (c_sort (type_pset ?t_52_312_228) ?l_309_231) (c_sort (type_memory ?v_0 ?t_52_312_228) ?m_308_232)))))))))))) +(assert (forall ((?t_54_319_235 c_type)) (forall ((?t_53_318_236 c_type)) (forall ((?p_317_237 c_unique)) (forall ((?l_316_238 c_unique)) (forall ((?m_315_239 c_unique)) (let ((?v_0 (type_pointer ?t_53_318_236))) (=> (not_in_pset (c_sort ?v_0 ?p_317_237) (c_sort (type_pset ?t_53_318_236) (pset_acc_all (c_sort (type_pset ?t_54_319_235) ?l_316_238) (c_sort (type_memory ?v_0 ?t_54_319_235) ?m_315_239)))) (forall ((?p1_314_240 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_54_319_235) ?p1_314_240) (c_sort (type_pset ?t_54_319_235) ?l_316_238))) (forall ((?i_313_241 Int)) (let ((?v_1 (type_pointer ?t_54_319_235))) (not (= (acc (c_sort (type_memory ?v_0 ?t_54_319_235) ?m_315_239) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_314_240) ?i_313_241))) ?p_317_237)))))))))))))) +(assert (forall ((?t_56_328_242 c_type)) (forall ((?t_55_327_243 c_type)) (forall ((?p_326_244 c_unique)) (forall ((?l_325_245 c_unique)) (forall ((?m_324_246 c_unique)) (forall ((?a_323_247 Int)) (forall ((?b_322_248 Int)) (let ((?v_0 (type_pointer ?t_55_327_243))) (=> (forall ((?p1_321_249 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_56_328_242) ?p1_321_249) (c_sort (type_pset ?t_56_328_242) ?l_325_245))) (forall ((?i_320_250 Int)) (let ((?v_1 (type_pointer ?t_56_328_242))) (=> (and (<= ?a_323_247 ?i_320_250) (<= ?i_320_250 ?b_322_248)) (not (= ?p_326_244 (acc (c_sort (type_memory ?v_0 ?t_56_328_242) ?m_324_246) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_321_249) ?i_320_250)))))))))) (not_in_pset (c_sort ?v_0 ?p_326_244) (c_sort (type_pset ?t_55_327_243) (pset_acc_range (c_sort (type_pset ?t_56_328_242) ?l_325_245) (c_sort (type_memory ?v_0 ?t_56_328_242) ?m_324_246) ?a_323_247 ?b_322_248))))))))))))) +(assert (forall ((?t_58_337_251 c_type)) (forall ((?t_57_336_252 c_type)) (forall ((?p_335_253 c_unique)) (forall ((?l_334_254 c_unique)) (forall ((?m_333_255 c_unique)) (forall ((?a_332_256 Int)) (forall ((?b_331_257 Int)) (let ((?v_0 (type_pointer ?t_57_336_252))) (=> (not_in_pset (c_sort ?v_0 ?p_335_253) (c_sort (type_pset ?t_57_336_252) (pset_acc_range (c_sort (type_pset ?t_58_337_251) ?l_334_254) (c_sort (type_memory ?v_0 ?t_58_337_251) ?m_333_255) ?a_332_256 ?b_331_257))) (forall ((?p1_330_258 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_58_337_251) ?p1_330_258) (c_sort (type_pset ?t_58_337_251) ?l_334_254))) (forall ((?i_329_259 Int)) (let ((?v_1 (type_pointer ?t_58_337_251))) (=> (and (<= ?a_332_256 ?i_329_259) (<= ?i_329_259 ?b_331_257)) (not (= (acc (c_sort (type_memory ?v_0 ?t_58_337_251) ?m_333_255) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_330_258) ?i_329_259))) ?p_335_253))))))))))))))))) +(assert (forall ((?t_60_345_260 c_type)) (forall ((?t_59_344_261 c_type)) (forall ((?p_343_262 c_unique)) (forall ((?l_342_263 c_unique)) (forall ((?m_341_264 c_unique)) (forall ((?a_340_265 Int)) (let ((?v_0 (type_pointer ?t_59_344_261))) (=> (forall ((?p1_339_266 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_60_345_260) ?p1_339_266) (c_sort (type_pset ?t_60_345_260) ?l_342_263))) (forall ((?i_338_267 Int)) (let ((?v_1 (type_pointer ?t_60_345_260))) (=> (<= ?i_338_267 ?a_340_265) (not (= ?p_343_262 (acc (c_sort (type_memory ?v_0 ?t_60_345_260) ?m_341_264) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_339_266) ?i_338_267)))))))))) (not_in_pset (c_sort ?v_0 ?p_343_262) (c_sort (type_pset ?t_59_344_261) (pset_acc_range_left (c_sort (type_pset ?t_60_345_260) ?l_342_263) (c_sort (type_memory ?v_0 ?t_60_345_260) ?m_341_264) ?a_340_265)))))))))))) +(assert (forall ((?t_62_353_268 c_type)) (forall ((?t_61_352_269 c_type)) (forall ((?p_351_270 c_unique)) (forall ((?l_350_271 c_unique)) (forall ((?m_349_272 c_unique)) (forall ((?a_348_273 Int)) (let ((?v_0 (type_pointer ?t_61_352_269))) (=> (not_in_pset (c_sort ?v_0 ?p_351_270) (c_sort (type_pset ?t_61_352_269) (pset_acc_range_left (c_sort (type_pset ?t_62_353_268) ?l_350_271) (c_sort (type_memory ?v_0 ?t_62_353_268) ?m_349_272) ?a_348_273))) (forall ((?p1_347_274 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_62_353_268) ?p1_347_274) (c_sort (type_pset ?t_62_353_268) ?l_350_271))) (forall ((?i_346_275 Int)) (let ((?v_1 (type_pointer ?t_62_353_268))) (=> (<= ?i_346_275 ?a_348_273) (not (= (acc (c_sort (type_memory ?v_0 ?t_62_353_268) ?m_349_272) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_347_274) ?i_346_275))) ?p_351_270)))))))))))))))) +(assert (forall ((?t_64_361_276 c_type)) (forall ((?t_63_360_277 c_type)) (forall ((?p_359_278 c_unique)) (forall ((?l_358_279 c_unique)) (forall ((?m_357_280 c_unique)) (forall ((?a_356_281 Int)) (let ((?v_0 (type_pointer ?t_63_360_277))) (=> (forall ((?p1_355_282 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_64_361_276) ?p1_355_282) (c_sort (type_pset ?t_64_361_276) ?l_358_279))) (forall ((?i_354_283 Int)) (let ((?v_1 (type_pointer ?t_64_361_276))) (=> (<= ?a_356_281 ?i_354_283) (not (= ?p_359_278 (acc (c_sort (type_memory ?v_0 ?t_64_361_276) ?m_357_280) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_355_282) ?i_354_283)))))))))) (not_in_pset (c_sort ?v_0 ?p_359_278) (c_sort (type_pset ?t_63_360_277) (pset_acc_range_right (c_sort (type_pset ?t_64_361_276) ?l_358_279) (c_sort (type_memory ?v_0 ?t_64_361_276) ?m_357_280) ?a_356_281)))))))))))) +(assert (forall ((?t_66_369_284 c_type)) (forall ((?t_65_368_285 c_type)) (forall ((?p_367_286 c_unique)) (forall ((?l_366_287 c_unique)) (forall ((?m_365_288 c_unique)) (forall ((?a_364_289 Int)) (let ((?v_0 (type_pointer ?t_65_368_285))) (=> (not_in_pset (c_sort ?v_0 ?p_367_286) (c_sort (type_pset ?t_65_368_285) (pset_acc_range_right (c_sort (type_pset ?t_66_369_284) ?l_366_287) (c_sort (type_memory ?v_0 ?t_66_369_284) ?m_365_288) ?a_364_289))) (forall ((?p1_363_290 c_unique)) (=> (not (not_in_pset (c_sort (type_pointer ?t_66_369_284) ?p1_363_290) (c_sort (type_pset ?t_66_369_284) ?l_366_287))) (forall ((?i_362_291 Int)) (let ((?v_1 (type_pointer ?t_66_369_284))) (=> (<= ?a_364_289 ?i_362_291) (not (= (acc (c_sort (type_memory ?v_0 ?t_66_369_284) ?m_365_288) (c_sort ?v_1 (shift (c_sort ?v_1 ?p1_363_290) ?i_362_291))) ?p_367_286)))))))))))))))) +(assert (forall ((?t_68_376_292 c_type)) (forall ((?t_67_375_293 c_type)) (forall ((?a_374_294 c_unique)) (forall ((?l_373_295 c_unique)) (forall ((?m1_372_296 c_unique)) (forall ((?m2_371_297 c_unique)) (forall ((?m3_370_298 c_unique)) (let ((?v_1 (c_sort type_alloc_table ?a_374_294)) (?v_0 (type_memory ?t_68_376_292 ?t_67_375_293))) (let ((?v_4 (c_sort ?v_0 ?m1_372_296)) (?v_2 (c_sort ?v_0 ?m2_371_297)) (?v_3 (c_sort (type_pset ?t_67_375_293) ?l_373_295)) (?v_5 (c_sort ?v_0 ?m3_370_298))) (=> (not_assigns ?v_1 ?v_4 ?v_2 ?v_3) (=> (not_assigns ?v_1 ?v_2 ?v_5 ?v_3) (not_assigns ?v_1 ?v_4 ?v_5 ?v_3))))))))))))) +(assert (forall ((?t_70_381_299 c_type)) (forall ((?t_69_380_300 c_type)) (forall ((?a_379_301 c_unique)) (forall ((?l_378_302 c_unique)) (forall ((?m_377_303 c_unique)) (let ((?v_0 (c_sort (type_memory ?t_70_381_299 ?t_69_380_300) ?m_377_303))) (not_assigns (c_sort type_alloc_table ?a_379_301) ?v_0 ?v_0 (c_sort (type_pset ?t_69_380_300) ?l_378_302))))))))) +(declare-fun valid_acc (c_ssorted) Bool) +(assert (forall ((?t_72_386_304 c_type)) (forall ((?t_71_385_305 c_type)) (forall ((?m1_384_306 c_unique)) (= (valid_acc (c_sort (type_memory (type_pointer ?t_71_385_305) ?t_72_386_304) ?m1_384_306)) (forall ((?p_383_307 c_unique)) (forall ((?a_382_308 c_unique)) (let ((?v_1 (type_pointer ?t_71_385_305)) (?v_0 (c_sort type_alloc_table ?a_382_308)) (?v_2 (c_sort (type_pointer ?t_72_386_304) ?p_383_307))) (=> (valid ?v_0 ?v_2) (valid ?v_0 (c_sort ?v_1 (acc (c_sort (type_memory ?v_1 ?t_72_386_304) ?m1_384_306) ?v_2)))))))))))) +(declare-fun valid_acc_range (c_ssorted Int) Bool) +(assert (forall ((?t_74_392_309 c_type)) (forall ((?t_73_391_310 c_type)) (forall ((?m1_390_311 c_unique)) (forall ((?size_389_312 Int)) (= (valid_acc_range (c_sort (type_memory (type_pointer ?t_73_391_310) ?t_74_392_309) ?m1_390_311) ?size_389_312) (forall ((?p_388_313 c_unique)) (forall ((?a_387_314 c_unique)) (let ((?v_1 (type_pointer ?t_73_391_310)) (?v_0 (c_sort type_alloc_table ?a_387_314)) (?v_2 (c_sort (type_pointer ?t_74_392_309) ?p_388_313))) (=> (valid ?v_0 ?v_2) (valid_range ?v_0 (c_sort ?v_1 (acc (c_sort (type_memory ?v_1 ?t_74_392_309) ?m1_390_311) ?v_2)) 0 (- ?size_389_312 1)))))))))))) +(assert (forall ((?t_76_398_315 c_type)) (forall ((?t_75_397_316 c_type)) (forall ((?m1_396_317 c_unique)) (forall ((?size_395_318 Int)) (forall ((?p_394_319 c_unique)) (forall ((?a_393_320 c_unique)) (let ((?v_1 (type_pointer ?t_75_397_316))) (let ((?v_2 (c_sort (type_memory ?v_1 ?t_76_398_315) ?m1_396_317)) (?v_0 (c_sort type_alloc_table ?a_393_320)) (?v_3 (c_sort (type_pointer ?t_76_398_315) ?p_394_319))) (=> (valid_acc_range ?v_2 ?size_395_318) (=> (valid ?v_0 ?v_3) (valid ?v_0 (c_sort ?v_1 (acc ?v_2 ?v_3)))))))))))))) +(declare-fun separation1 (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_78_404_321 c_type)) (forall ((?t_77_403_322 c_type)) (forall ((?m1_402_323 c_unique)) (forall ((?m2_401_324 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_77_403_322) ?t_78_404_321))) (= (separation1 (c_sort ?v_0 ?m1_402_323) (c_sort ?v_0 ?m2_401_324)) (forall ((?p_400_325 c_unique)) (forall ((?a_399_326 c_unique)) (let ((?v_1 (type_pointer ?t_77_403_322)) (?v_2 (c_sort (type_pointer ?t_78_404_321) ?p_400_325))) (=> (valid (c_sort type_alloc_table ?a_399_326) ?v_2) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_402_323) ?v_2))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_401_324) ?v_2)))))))))))))))) +(declare-fun separation1_range1 (c_ssorted c_ssorted Int) Bool) +(assert (forall ((?t_80_412_327 c_type)) (forall ((?t_79_411_328 c_type)) (forall ((?m1_410_329 c_unique)) (forall ((?m2_409_330 c_unique)) (forall ((?size_408_331 Int)) (let ((?v_0 (type_memory (type_pointer ?t_79_411_328) ?t_80_412_327))) (= (separation1_range1 (c_sort ?v_0 ?m1_410_329) (c_sort ?v_0 ?m2_409_330) ?size_408_331) (forall ((?p_407_332 c_unique)) (forall ((?a_406_333 c_unique)) (=> (valid (c_sort type_alloc_table ?a_406_333) (c_sort (type_pointer ?t_80_412_327) ?p_407_332)) (forall ((?i_405_334 Int)) (let ((?v_1 (type_pointer ?t_79_411_328)) (?v_2 (type_pointer ?t_80_412_327))) (let ((?v_3 (c_sort ?v_2 ?p_407_332))) (=> (and (<= 0 ?i_405_334) (< ?i_405_334 ?size_408_331)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_410_329) (c_sort ?v_2 (shift ?v_3 ?i_405_334))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_409_330) ?v_3)))))))))))))))))))) +(declare-fun separation1_range (c_ssorted Int) Bool) +(assert (forall ((?t_82_420_335 c_type)) (forall ((?t_81_419_336 c_type)) (forall ((?m_418_337 c_unique)) (forall ((?size_417_338 Int)) (= (separation1_range (c_sort (type_memory (type_pointer ?t_81_419_336) ?t_82_420_335) ?m_418_337) ?size_417_338) (forall ((?p_416_339 c_unique)) (forall ((?a_415_340 c_unique)) (=> (valid (c_sort type_alloc_table ?a_415_340) (c_sort (type_pointer ?t_82_420_335) ?p_416_339)) (forall ((?i1_414_341 Int)) (forall ((?i2_413_342 Int)) (let ((?v_0 (type_pointer ?t_81_419_336))) (let ((?v_2 (c_sort (type_memory ?v_0 ?t_82_420_335) ?m_418_337)) (?v_1 (type_pointer ?t_82_420_335))) (let ((?v_3 (c_sort ?v_1 ?p_416_339))) (=> (and (<= 0 ?i1_414_341) (< ?i1_414_341 ?size_417_338)) (=> (and (<= 0 ?i2_413_342) (< ?i2_413_342 ?size_417_338)) (=> (not (= ?i1_414_341 ?i2_413_342)) (not (= (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i1_414_341))))) (base_addr (c_sort ?v_0 (acc ?v_2 (c_sort ?v_1 (shift ?v_3 ?i2_413_342)))))))))))))))))))))))) +(declare-fun separation2 (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_84_426_343 c_type)) (forall ((?t_83_425_344 c_type)) (forall ((?m1_424_345 c_unique)) (forall ((?m2_423_346 c_unique)) (let ((?v_0 (type_memory (type_pointer ?t_83_425_344) ?t_84_426_343))) (= (separation2 (c_sort ?v_0 ?m1_424_345) (c_sort ?v_0 ?m2_423_346)) (forall ((?p1_422_347 c_unique)) (forall ((?p2_421_348 c_unique)) (let ((?v_1 (type_pointer ?t_83_425_344)) (?v_2 (type_pointer ?t_84_426_343))) (=> (not (= ?p1_422_347 ?p2_421_348)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_424_345) (c_sort ?v_2 ?p1_422_347)))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_423_346) (c_sort ?v_2 ?p2_421_348))))))))))))))))) +(declare-fun separation2_range1 (c_ssorted c_ssorted Int) Bool) +(assert (forall ((?t_86_435_349 c_type)) (forall ((?t_85_434_350 c_type)) (forall ((?m1_433_351 c_unique)) (forall ((?m2_432_352 c_unique)) (forall ((?size_431_353 Int)) (let ((?v_0 (type_memory (type_pointer ?t_85_434_350) ?t_86_435_349))) (= (separation2_range1 (c_sort ?v_0 ?m1_433_351) (c_sort ?v_0 ?m2_432_352) ?size_431_353) (forall ((?p_430_354 c_unique)) (forall ((?q_429_355 c_unique)) (forall ((?a_428_356 c_unique)) (forall ((?i_427_357 Int)) (let ((?v_1 (type_pointer ?t_85_434_350)) (?v_2 (type_pointer ?t_86_435_349))) (=> (and (<= 0 ?i_427_357) (< ?i_427_357 ?size_431_353)) (not (= (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m1_433_351) (c_sort ?v_2 (shift (c_sort ?v_2 ?p_430_354) ?i_427_357))))) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?m2_432_352) (c_sort ?v_2 ?q_429_355)))))))))))))))))))) +(declare-fun on_heap (c_ssorted c_ssorted) Bool) +(declare-fun on_stack (c_ssorted c_ssorted) Bool) +(declare-fun fresh (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_87_438_358 c_type)) (forall ((?a_437_359 c_unique)) (forall ((?p_436_360 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a_437_359)) (?v_1 (c_sort (type_pointer ?t_87_438_358) ?p_436_360))) (=> (fresh ?v_0 ?v_1) (not (valid ?v_0 ?v_1)))))))) +(assert (forall ((?t_88_442_361 c_type)) (forall ((?a_441_362 c_unique)) (forall ((?p_440_363 c_unique)) (=> (fresh (c_sort type_alloc_table ?a_441_362) (c_sort (type_pointer ?t_88_442_361) ?p_440_363)) (forall ((?i_439_364 Int)) (let ((?v_0 (type_pointer ?t_88_442_361))) (not (valid (c_sort type_alloc_table ?a_441_362) (c_sort ?v_0 (shift (c_sort ?v_0 ?p_440_363) ?i_439_364))))))))))) +(declare-fun alloc_extends (c_ssorted c_ssorted) Bool) +(assert (forall ((?t_89_446_365 c_type)) (forall ((?a1_445_366 c_unique)) (forall ((?a2_444_367 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_445_366) (c_sort type_alloc_table ?a2_444_367)) (forall ((?q_443_368 c_unique)) (let ((?v_0 (c_sort (type_pointer ?t_89_446_365) ?q_443_368))) (=> (valid (c_sort type_alloc_table ?a1_445_366) ?v_0) (valid (c_sort type_alloc_table ?a2_444_367) ?v_0))))))))) +(assert (forall ((?t_90_451_369 c_type)) (forall ((?a1_450_370 c_unique)) (forall ((?a2_449_371 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_450_370) (c_sort type_alloc_table ?a2_449_371)) (forall ((?q_448_372 c_unique)) (forall ((?i_447_373 Int)) (let ((?v_0 (c_sort (type_pointer ?t_90_451_369) ?q_448_372))) (=> (valid_index (c_sort type_alloc_table ?a1_450_370) ?v_0 ?i_447_373) (valid_index (c_sort type_alloc_table ?a2_449_371) ?v_0 ?i_447_373)))))))))) +(assert (forall ((?t_91_457_374 c_type)) (forall ((?a1_456_375 c_unique)) (forall ((?a2_455_376 c_unique)) (=> (alloc_extends (c_sort type_alloc_table ?a1_456_375) (c_sort type_alloc_table ?a2_455_376)) (forall ((?q_454_377 c_unique)) (forall ((?i_453_378 Int)) (forall ((?j_452_379 Int)) (let ((?v_0 (c_sort (type_pointer ?t_91_457_374) ?q_454_377))) (=> (valid_range (c_sort type_alloc_table ?a1_456_375) ?v_0 ?i_453_378 ?j_452_379) (valid_range (c_sort type_alloc_table ?a2_455_376) ?v_0 ?i_453_378 ?j_452_379))))))))))) +(assert (forall ((?a_458_380 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a_458_380))) (alloc_extends ?v_0 ?v_0)))) +(assert (forall ((?a1_461_381 c_unique)) (forall ((?a2_460_382 c_unique)) (forall ((?a3_459_383 c_unique)) (let ((?v_1 (c_sort type_alloc_table ?a1_461_381)) (?v_0 (c_sort type_alloc_table ?a2_460_382)) (?v_2 (c_sort type_alloc_table ?a3_459_383))) (=> (alloc_extends ?v_1 ?v_0) (=> (alloc_extends ?v_0 ?v_2) (alloc_extends ?v_1 ?v_2)))))))) +(declare-fun free_stack (c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?t_92_466_384 c_type)) (forall ((?a1_465_385 c_unique)) (forall ((?a2_464_386 c_unique)) (forall ((?a3_463_387 c_unique)) (=> (free_stack (c_sort type_alloc_table ?a1_465_385) (c_sort type_alloc_table ?a2_464_386) (c_sort type_alloc_table ?a3_463_387)) (forall ((?p_462_388 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a2_464_386)) (?v_1 (c_sort (type_pointer ?t_92_466_384) ?p_462_388))) (=> (valid ?v_0 ?v_1) (=> (on_heap ?v_0 ?v_1) (valid (c_sort type_alloc_table ?a3_463_387) ?v_1))))))))))) +(assert (forall ((?t_93_471_389 c_type)) (forall ((?a1_470_390 c_unique)) (forall ((?a2_469_391 c_unique)) (forall ((?a3_468_392 c_unique)) (=> (free_stack (c_sort type_alloc_table ?a1_470_390) (c_sort type_alloc_table ?a2_469_391) (c_sort type_alloc_table ?a3_468_392)) (forall ((?p_467_393 c_unique)) (let ((?v_0 (c_sort type_alloc_table ?a1_470_390)) (?v_1 (c_sort (type_pointer ?t_93_471_389) ?p_467_393))) (=> (valid ?v_0 ?v_1) (=> (on_stack ?v_0 ?v_1) (valid (c_sort type_alloc_table ?a3_468_392) ?v_1))))))))))) +(declare-fun null () c_unique) +(assert (forall ((?t_94_475_394 c_type)) (forall ((?a_474_395 c_unique)) (not (valid (c_sort type_alloc_table ?a_474_395) (c_sort (type_pointer ?t_94_475_394) null)))))) +(declare-fun type_global () c_type) +(declare-fun separation_anonymous_0_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?x_global_489_396 c_unique)) (forall ((?anonymous_0PM_global_488_397 c_unique)) (forall ((?tab_487_398 c_unique)) (forall ((?v_486_399 c_unique)) (forall ((?alloc_485_400 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global)) (?v_2 (c_sort ?v_1 ?tab_487_398)) (?v_3 (c_sort ?v_1 ?v_486_399))) (= (separation_anonymous_0_int (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_0 ?anonymous_0PM_global_488_397) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_485_400)) (and (not (= (base_addr ?v_2) (base_addr ?v_3))) (forall ((?index_3_484_401 Int)) (=> (and (<= 0 ?index_3_484_401) (< ?index_3_484_401 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_489_396) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_488_397) (c_sort ?v_1 (shift ?v_2 ?index_3_484_401))))))))))))))))))))) +(declare-fun separation_anonymous_0_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?x_global_498_402 c_unique)) (forall ((?u_global_497_403 c_unique)) (forall ((?t_global_496_404 c_unique)) (forall ((?s1PM_global_495_405 c_unique)) (forall ((?anonymous_0PM_global_494_406 c_unique)) (forall ((?tab_493_407 c_unique)) (forall ((?s_492_408 c_unique)) (forall ((?alloc_491_409 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_497_403)) (?v_5 (c_sort ?v_0 ?t_global_496_404)) (?v_6 (c_sort ?v_0 ?s1PM_global_495_405)) (?v_2 (c_sort ?v_1 ?tab_493_407)) (?v_3 (c_sort ?v_1 ?s_492_408))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_0_s1 (c_sort ?v_0 ?x_global_498_402) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_494_406) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_491_409)) (and (not (= ?v_4 (base_addr ?v_3))) (and (forall ((?index_6_490_410 Int)) (=> (and (<= 0 ?index_6_490_410) (< ?index_6_490_410 5)) (not (= (base_addr ?v_3) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_498_402) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_494_406) (c_sort ?v_1 (shift ?v_2 ?index_6_490_410))))))))))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))))))))))))))))))) +(declare-fun separation_anonymous_1_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?x_global_507_411 c_unique)) (forall ((?p2_global_506_412 c_unique)) (forall ((?p1_global_505_413 c_unique)) (forall ((?anonymous_1PM_global_504_414 c_unique)) (forall ((?anonymous_0PM_global_503_415 c_unique)) (forall ((?u1_502_416 c_unique)) (forall ((?tab_501_417 c_unique)) (forall ((?alloc_500_418 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_506_412)) (?v_5 (c_sort ?v_0 ?p1_global_505_413)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_504_414)) (?v_2 (c_sort ?v_1 ?u1_502_416)) (?v_3 (c_sort ?v_1 ?tab_501_417))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_anonymous_0 (c_sort ?v_0 ?x_global_507_411) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_503_415) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_500_418)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_7_499_419 Int)) (=> (and (<= 0 ?index_7_499_419) (< ?index_7_499_419 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_507_411) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_503_415) (c_sort ?v_1 (shift ?v_3 ?index_7_499_419))))))))))))))))))))))))))) +(declare-fun separation_anonymous_1_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?p2_global_513_420 c_unique)) (forall ((?p1_global_512_421 c_unique)) (forall ((?anonymous_1PM_global_511_422 c_unique)) (forall ((?u2_510_423 c_unique)) (forall ((?u1_509_424 c_unique)) (forall ((?alloc_508_425 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_513_420)) (?v_5 (c_sort ?v_0 ?p1_global_512_421)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_511_422)) (?v_2 (c_sort ?v_1 ?u2_510_423)) (?v_3 (c_sort ?v_1 ?u1_509_424))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_1_anonymous_1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_508_425)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10)))))))))))))))))))) +(declare-fun separation_anonymous_1_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?p2_global_519_426 c_unique)) (forall ((?p1_global_518_427 c_unique)) (forall ((?anonymous_1PM_global_517_428 c_unique)) (forall ((?u1_516_429 c_unique)) (forall ((?v_515_430 c_unique)) (forall ((?alloc_514_431 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?p2_global_519_426)) (?v_5 (c_sort ?v_0 ?p1_global_518_427)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_517_428)) (?v_2 (c_sort ?v_1 ?u1_516_429)) (?v_3 (c_sort ?v_1 ?v_515_430))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_1_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_514_431)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8))))))))))))))))))) +(declare-fun separation_anonymous_1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?u_global_528_432 c_unique)) (forall ((?t_global_527_433 c_unique)) (forall ((?s1PM_global_526_434 c_unique)) (forall ((?p2_global_525_435 c_unique)) (forall ((?p1_global_524_436 c_unique)) (forall ((?anonymous_1PM_global_523_437 c_unique)) (forall ((?u1_522_438 c_unique)) (forall ((?s_521_439 c_unique)) (forall ((?alloc_520_440 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_528_432)) (?v_10 (c_sort ?v_0 ?t_global_527_433)) (?v_11 (c_sort ?v_0 ?s1PM_global_526_434)) (?v_7 (c_sort ?v_0 ?p2_global_525_435)) (?v_5 (c_sort ?v_0 ?p1_global_524_436)) (?v_6 (c_sort ?v_0 ?anonymous_1PM_global_523_437)) (?v_2 (c_sort ?v_1 ?u1_522_438)) (?v_3 (c_sort ?v_1 ?s_521_439))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_1_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_520_440)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13))))))))))))))))))))))) +(declare-fun separation_anonymous_2_anonymous_0 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?x_global_537_441 c_unique)) (forall ((?anonymous_2_p2_global_536_442 c_unique)) (forall ((?anonymous_2_p1_global_535_443 c_unique)) (forall ((?anonymous_2PM_global_534_444 c_unique)) (forall ((?anonymous_0PM_global_533_445 c_unique)) (forall ((?u3_532_446 c_unique)) (forall ((?tab_531_447 c_unique)) (forall ((?alloc_530_448 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_536_442)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_535_443)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_534_444)) (?v_2 (c_sort ?v_1 ?u3_532_446)) (?v_3 (c_sort ?v_1 ?tab_531_447))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_anonymous_0 (c_sort ?v_0 ?x_global_537_441) ?v_7 ?v_5 ?v_6 (c_sort ?v_0 ?anonymous_0PM_global_533_445) ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_530_448)) (and (not (= (base_addr ?v_2) ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (forall ((?index_15_529_449 Int)) (=> (and (<= 0 ?index_15_529_449) (< ?index_15_529_449 5)) (not (= (base_addr ?v_2) (base_addr (c_sort ?v_1 (acc (c_sort ?v_0 ?x_global_537_441) (c_sort ?v_1 (acc (c_sort ?v_0 ?anonymous_0PM_global_533_445) (c_sort ?v_1 (shift ?v_3 ?index_15_529_449))))))))))))))))))))))))))) +(declare-fun separation_anonymous_2_anonymous_1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?p2_global_546_450 c_unique)) (forall ((?p1_global_545_451 c_unique)) (forall ((?anonymous_2_p2_global_544_452 c_unique)) (forall ((?anonymous_2_p1_global_543_453 c_unique)) (forall ((?anonymous_2PM_global_542_454 c_unique)) (forall ((?anonymous_1PM_global_541_455 c_unique)) (forall ((?u3_540_456 c_unique)) (forall ((?u1_539_457 c_unique)) (forall ((?alloc_538_458 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?p2_global_546_450)) (?v_10 (c_sort ?v_0 ?p1_global_545_451)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_544_452)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_543_453)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_542_454)) (?v_11 (c_sort ?v_0 ?anonymous_1PM_global_541_455)) (?v_2 (c_sort ?v_1 ?u3_540_456)) (?v_3 (c_sort ?v_1 ?u1_539_457))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_anonymous_1 ?v_12 ?v_10 ?v_7 ?v_5 ?v_6 ?v_11 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_538_458)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13))))))))))))))))))))))) +(declare-fun separation_anonymous_2_anonymous_2 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?anonymous_2_p2_global_552_459 c_unique)) (forall ((?anonymous_2_p1_global_551_460 c_unique)) (forall ((?anonymous_2PM_global_550_461 c_unique)) (forall ((?u4_549_462 c_unique)) (forall ((?u3_548_463 c_unique)) (forall ((?alloc_547_464 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_552_459)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_551_460)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_550_461)) (?v_2 (c_sort ?v_1 ?u4_549_462)) (?v_3 (c_sort ?v_1 ?u3_548_463))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_anonymous_2_anonymous_2 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_547_464)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10)))))))))))))))))))) +(declare-fun separation_anonymous_2_int (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?anonymous_2_p2_global_558_465 c_unique)) (forall ((?anonymous_2_p1_global_557_466 c_unique)) (forall ((?anonymous_2PM_global_556_467 c_unique)) (forall ((?u3_555_468 c_unique)) (forall ((?v_554_469 c_unique)) (forall ((?alloc_553_470 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_558_465)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_557_466)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_556_467)) (?v_2 (c_sort ?v_1 ?u3_555_468)) (?v_3 (c_sort ?v_1 ?v_554_469))) (let ((?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2)))) (= (separation_anonymous_2_int ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_553_470)) (and (not (= (base_addr ?v_2) ?v_4)) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8))))))))))))))))))) +(declare-fun separation_anonymous_2_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?u_global_567_471 c_unique)) (forall ((?t_global_566_472 c_unique)) (forall ((?s1PM_global_565_473 c_unique)) (forall ((?anonymous_2_p2_global_564_474 c_unique)) (forall ((?anonymous_2_p1_global_563_475 c_unique)) (forall ((?anonymous_2PM_global_562_476 c_unique)) (forall ((?u3_561_477 c_unique)) (forall ((?s_560_478 c_unique)) (forall ((?alloc_559_479 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_12 (c_sort ?v_0 ?u_global_567_471)) (?v_10 (c_sort ?v_0 ?t_global_566_472)) (?v_11 (c_sort ?v_0 ?s1PM_global_565_473)) (?v_7 (c_sort ?v_0 ?anonymous_2_p2_global_564_474)) (?v_5 (c_sort ?v_0 ?anonymous_2_p1_global_563_475)) (?v_6 (c_sort ?v_0 ?anonymous_2PM_global_562_476)) (?v_2 (c_sort ?v_1 ?u3_561_477)) (?v_3 (c_sort ?v_1 ?s_560_478))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_13 (c_sort ?v_1 (acc ?v_11 ?v_3)))) (= (separation_anonymous_2_s1 ?v_12 ?v_10 ?v_11 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_559_479)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_10 ?v_13))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_12 ?v_13))))))))))))))))))))))) +(declare-fun separation_int_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?u_global_573_480 c_unique)) (forall ((?t_global_572_481 c_unique)) (forall ((?s1PM_global_571_482 c_unique)) (forall ((?v_570_483 c_unique)) (forall ((?s_569_484 c_unique)) (forall ((?alloc_568_485 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_573_480)) (?v_5 (c_sort ?v_0 ?t_global_572_481)) (?v_6 (c_sort ?v_0 ?s1PM_global_571_482)) (?v_2 (c_sort ?v_1 ?v_570_483)) (?v_3 (c_sort ?v_1 ?s_569_484))) (let ((?v_4 (base_addr ?v_2)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_int_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_568_485)) (and (not (= ?v_4 (base_addr ?v_3))) (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8))))))))))))))))))) +(declare-fun separation_s1_s1 (c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted c_ssorted) Bool) +(assert (forall ((?u_global_579_486 c_unique)) (forall ((?t_global_578_487 c_unique)) (forall ((?s1PM_global_577_488 c_unique)) (forall ((?ss_576_489 c_unique)) (forall ((?s_575_490 c_unique)) (forall ((?alloc_574_491 c_unique)) (let ((?v_1 (type_pointer type_global))) (let ((?v_0 (type_memory ?v_1 type_global))) (let ((?v_7 (c_sort ?v_0 ?u_global_579_486)) (?v_5 (c_sort ?v_0 ?t_global_578_487)) (?v_6 (c_sort ?v_0 ?s1PM_global_577_488)) (?v_2 (c_sort ?v_1 ?ss_576_489)) (?v_3 (c_sort ?v_1 ?s_575_490))) (let ((?v_9 (base_addr ?v_2)) (?v_4 (base_addr ?v_3)) (?v_8 (c_sort ?v_1 (acc ?v_6 ?v_2))) (?v_10 (c_sort ?v_1 (acc ?v_6 ?v_3)))) (= (separation_s1_s1 ?v_7 ?v_5 ?v_6 ?v_2 ?v_3 (c_sort type_alloc_table ?alloc_574_491)) (and (not (= ?v_9 ?v_4)) (and (and (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_8))))) (not (= ?v_4 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_8)))))) (and (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_5 ?v_10))))) (not (= ?v_9 (base_addr (c_sort ?v_1 (acc ?v_7 ?v_10)))))))))))))))))))) +(assert (not (forall ((?alloc c_unique)) (forall ((?anonymous_2PM_global c_unique)) (forall ((?anonymous_2_p1_global c_unique)) (forall ((?anonymous_2_p2_global c_unique)) (forall ((?anonymous_2_v1_global c_unique)) (forall ((?anonymous_2_v2_global c_unique)) (forall ((?intM_global c_unique)) (forall ((?u3 c_unique)) (forall ((?u4 c_unique)) (forall ((?w1 c_unique)) (forall ((?w10 c_unique)) (forall ((?w2 c_unique)) (forall ((?w3 c_unique)) (forall ((?w4 c_unique)) (forall ((?w5 c_unique)) (forall ((?w6 c_unique)) (forall ((?w7 c_unique)) (forall ((?w8 c_unique)) (forall ((?w9 c_unique)) (let ((?v_0 (type_pointer type_global))) (let ((?v_2 (type_memory ?v_0 type_global)) (?v_3 (c_sort ?v_0 ?w3))) (let ((?v_5 (base_addr ?v_3)) (?v_8 (c_sort ?v_0 ?u4))) (let ((?v_1 (base_addr ?v_8)) (?v_6 (c_sort ?v_2 ?anonymous_2_p1_global)) (?v_7 (c_sort ?v_2 ?anonymous_2PM_global))) (let ((?v_4 (c_sort ?v_0 (acc ?v_7 ?v_3)))) (let ((?v_12 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_4)))) (?v_9 (c_sort ?v_2 ?anonymous_2_p2_global))) (let ((?v_13 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_4)))) (?v_10 (c_sort ?v_0 (acc ?v_7 ?v_8)))) (let ((?v_16 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_10)))) (?v_17 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_10)))) (?v_14 (c_sort ?v_0 ?u3))) (let ((?v_11 (base_addr ?v_14)) (?v_15 (c_sort ?v_0 (acc ?v_7 ?v_14)))) (let ((?v_18 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_15)))) (?v_19 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_15)))) (?v_20 (c_sort ?v_0 ?w1))) (let ((?v_22 (base_addr ?v_20)) (?v_21 (c_sort ?v_0 (acc ?v_7 ?v_20)))) (let ((?v_23 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_21)))) (?v_24 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_21)))) (?v_25 (c_sort type_alloc_table ?alloc)) (?v_54 (c_sort ?v_0 ?w9)) (?v_26 (c_sort ?v_0 ?w8)) (?v_27 (c_sort ?v_0 ?w7)) (?v_32 (c_sort ?v_0 ?w6)) (?v_37 (c_sort ?v_0 ?w5)) (?v_40 (c_sort ?v_0 ?w4)) (?v_43 (c_sort ?v_0 ?w2))) (let ((?v_30 (base_addr ?v_26)) (?v_28 (base_addr ?v_27)) (?v_29 (c_sort ?v_0 (acc ?v_7 ?v_26)))) (let ((?v_34 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_29)))) (?v_35 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_29)))) (?v_31 (c_sort ?v_0 (acc ?v_7 ?v_27)))) (let ((?v_59 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_31)))) (?v_60 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_31)))) (?v_33 (base_addr ?v_32)) (?v_36 (c_sort ?v_0 (acc ?v_7 ?v_32)))) (let ((?v_46 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_36)))) (?v_47 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_36)))) (?v_38 (base_addr ?v_37)) (?v_39 (c_sort ?v_0 (acc ?v_7 ?v_37)))) (let ((?v_48 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_39)))) (?v_49 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_39)))) (?v_41 (base_addr ?v_40)) (?v_42 (c_sort ?v_0 (acc ?v_7 ?v_40)))) (let ((?v_50 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_42)))) (?v_51 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_42)))) (?v_44 (base_addr ?v_43)) (?v_45 (c_sort ?v_0 (acc ?v_7 ?v_43)))) (let ((?v_52 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_45)))) (?v_53 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_45)))) (?v_66 (valid ?v_25 ?v_14)) (?v_61 (c_sort ?v_0 ?w10)) (?v_56 (base_addr ?v_54)) (?v_55 (c_sort ?v_0 (acc ?v_7 ?v_54)))) (let ((?v_57 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_55)))) (?v_58 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_55)))) (?v_63 (base_addr ?v_61)) (?v_62 (c_sort ?v_0 (acc ?v_7 ?v_61)))) (let ((?v_64 (base_addr (c_sort ?v_0 (acc ?v_6 ?v_62)))) (?v_65 (base_addr (c_sort ?v_0 (acc ?v_9 ?v_62))))) (=> (and (and (not (= ?v_5 ?v_1)) (and (and (not (= ?v_1 ?v_12)) (not (= ?v_1 ?v_13))) (and (not (= ?v_5 ?v_16)) (not (= ?v_5 ?v_17))))) (and (and (not (= ?v_5 ?v_11)) (and (and (not (= ?v_11 ?v_12)) (not (= ?v_11 ?v_13))) (and (not (= ?v_5 ?v_18)) (not (= ?v_5 ?v_19))))) (and (and (not (= ?v_1 ?v_11)) (and (and (not (= ?v_11 ?v_16)) (not (= ?v_11 ?v_17))) (and (not (= ?v_1 ?v_18)) (not (= ?v_1 ?v_19))))) (and (and (not (= ?v_22 ?v_1)) (and (and (not (= ?v_1 ?v_23)) (not (= ?v_1 ?v_24))) (and (not (= ?v_22 ?v_16)) (not (= ?v_22 ?v_17))))) (and (and (not (= ?v_22 ?v_11)) (and (and (not (= ?v_11 ?v_23)) (not (= ?v_11 ?v_24))) (and (not (= ?v_22 ?v_18)) (not (= ?v_22 ?v_19))))) (and (valid ?v_25 ?v_54) (and (valid ?v_25 ?v_26) (and (valid ?v_25 ?v_27) (and (valid ?v_25 ?v_32) (and (valid ?v_25 ?v_37) (and (valid ?v_25 ?v_40) (and (valid ?v_25 ?v_3) (and (valid ?v_25 ?v_43) (and (valid ?v_25 ?v_20) (and (and (not (= ?v_30 ?v_28)) (and (and (not (= ?v_28 ?v_34)) (not (= ?v_28 ?v_35))) (and (not (= ?v_30 ?v_59)) (not (= ?v_30 ?v_60))))) (and (and (not (= ?v_30 ?v_33)) (and (and (not (= ?v_33 ?v_34)) (not (= ?v_33 ?v_35))) (and (not (= ?v_30 ?v_46)) (not (= ?v_30 ?v_47))))) (and (and (not (= ?v_30 ?v_38)) (and (and (not (= ?v_38 ?v_34)) (not (= ?v_38 ?v_35))) (and (not (= ?v_30 ?v_48)) (not (= ?v_30 ?v_49))))) (and (and (not (= ?v_30 ?v_41)) (and (and (not (= ?v_41 ?v_34)) (not (= ?v_41 ?v_35))) (and (not (= ?v_30 ?v_50)) (not (= ?v_30 ?v_51))))) (and (and (not (= ?v_30 ?v_5)) (and (and (not (= ?v_5 ?v_34)) (not (= ?v_5 ?v_35))) (and (not (= ?v_30 ?v_12)) (not (= ?v_30 ?v_13))))) (and (and (not (= ?v_30 ?v_44)) (and (and (not (= ?v_44 ?v_34)) (not (= ?v_44 ?v_35))) (and (not (= ?v_30 ?v_52)) (not (= ?v_30 ?v_53))))) (and (and (not (= ?v_30 ?v_22)) (and (and (not (= ?v_22 ?v_34)) (not (= ?v_22 ?v_35))) (and (not (= ?v_30 ?v_23)) (not (= ?v_30 ?v_24))))) (and (valid ?v_25 ?v_8) (and ?v_66 (and (and (not (= ?v_33 ?v_38)) (and (and (not (= ?v_38 ?v_46)) (not (= ?v_38 ?v_47))) (and (not (= ?v_33 ?v_48)) (not (= ?v_33 ?v_49))))) (and (and (not (= ?v_33 ?v_41)) (and (and (not (= ?v_41 ?v_46)) (not (= ?v_41 ?v_47))) (and (not (= ?v_33 ?v_50)) (not (= ?v_33 ?v_51))))) (and (and (not (= ?v_33 ?v_5)) (and (and (not (= ?v_5 ?v_46)) (not (= ?v_5 ?v_47))) (and (not (= ?v_33 ?v_12)) (not (= ?v_33 ?v_13))))) (and (and (not (= ?v_33 ?v_44)) (and (and (not (= ?v_44 ?v_46)) (not (= ?v_44 ?v_47))) (and (not (= ?v_33 ?v_52)) (not (= ?v_33 ?v_53))))) (and (and (not (= ?v_33 ?v_22)) (and (and (not (= ?v_22 ?v_46)) (not (= ?v_22 ?v_47))) (and (not (= ?v_33 ?v_23)) (not (= ?v_33 ?v_24))))) (and (and (not (= ?v_30 ?v_1)) (and (and (not (= ?v_1 ?v_34)) (not (= ?v_1 ?v_35))) (and (not (= ?v_30 ?v_16)) (not (= ?v_30 ?v_17))))) (and (and (not (= ?v_30 ?v_11)) (and (and (not (= ?v_11 ?v_34)) (not (= ?v_11 ?v_35))) (and (not (= ?v_30 ?v_18)) (not (= ?v_30 ?v_19))))) (and (and (not (= ?v_41 ?v_5)) (and (and (not (= ?v_5 ?v_50)) (not (= ?v_5 ?v_51))) (and (not (= ?v_41 ?v_12)) (not (= ?v_41 ?v_13))))) (and (and (not (= ?v_41 ?v_44)) (and (and (not (= ?v_44 ?v_50)) (not (= ?v_44 ?v_51))) (and (not (= ?v_41 ?v_52)) (not (= ?v_41 ?v_53))))) (and (and (not (= ?v_41 ?v_22)) (and (and (not (= ?v_22 ?v_50)) (not (= ?v_22 ?v_51))) (and (not (= ?v_41 ?v_23)) (not (= ?v_41 ?v_24))))) (and (and (not (= ?v_33 ?v_1)) (and (and (not (= ?v_1 ?v_46)) (not (= ?v_1 ?v_47))) (and (not (= ?v_33 ?v_16)) (not (= ?v_33 ?v_17))))) (and (and (not (= ?v_33 ?v_11)) (and (and (not (= ?v_11 ?v_46)) (not (= ?v_11 ?v_47))) (and (not (= ?v_33 ?v_18)) (not (= ?v_33 ?v_19))))) (and (and (not (= ?v_44 ?v_22)) (and (and (not (= ?v_22 ?v_52)) (not (= ?v_22 ?v_53))) (and (not (= ?v_44 ?v_23)) (not (= ?v_44 ?v_24))))) (and (and (not (= ?v_41 ?v_1)) (and (and (not (= ?v_1 ?v_50)) (not (= ?v_1 ?v_51))) (and (not (= ?v_41 ?v_16)) (not (= ?v_41 ?v_17))))) (and (and (not (= ?v_41 ?v_11)) (and (and (not (= ?v_11 ?v_50)) (not (= ?v_11 ?v_51))) (and (not (= ?v_41 ?v_18)) (not (= ?v_41 ?v_19))))) (and (valid ?v_25 ?v_61) (and (and (not (= ?v_44 ?v_1)) (and (and (not (= ?v_1 ?v_52)) (not (= ?v_1 ?v_53))) (and (not (= ?v_44 ?v_16)) (not (= ?v_44 ?v_17))))) (and (and (not (= ?v_44 ?v_11)) (and (and (not (= ?v_11 ?v_52)) (not (= ?v_11 ?v_53))) (and (not (= ?v_44 ?v_18)) (not (= ?v_44 ?v_19))))) (and (and (not (= ?v_56 ?v_30)) (and (and (not (= ?v_30 ?v_57)) (not (= ?v_30 ?v_58))) (and (not (= ?v_56 ?v_34)) (not (= ?v_56 ?v_35))))) (and (and (not (= ?v_56 ?v_28)) (and (and (not (= ?v_28 ?v_57)) (not (= ?v_28 ?v_58))) (and (not (= ?v_56 ?v_59)) (not (= ?v_56 ?v_60))))) (and (and (not (= ?v_56 ?v_33)) (and (and (not (= ?v_33 ?v_57)) (not (= ?v_33 ?v_58))) (and (not (= ?v_56 ?v_46)) (not (= ?v_56 ?v_47))))) (and (and (not (= ?v_56 ?v_38)) (and (and (not (= ?v_38 ?v_57)) (not (= ?v_38 ?v_58))) (and (not (= ?v_56 ?v_48)) (not (= ?v_56 ?v_49))))) (and (and (not (= ?v_63 ?v_56)) (and (and (not (= ?v_56 ?v_64)) (not (= ?v_56 ?v_65))) (and (not (= ?v_63 ?v_57)) (not (= ?v_63 ?v_58))))) (and (and (not (= ?v_56 ?v_41)) (and (and (not (= ?v_41 ?v_57)) (not (= ?v_41 ?v_58))) (and (not (= ?v_56 ?v_50)) (not (= ?v_56 ?v_51))))) (and (and (not (= ?v_63 ?v_30)) (and (and (not (= ?v_30 ?v_64)) (not (= ?v_30 ?v_65))) (and (not (= ?v_63 ?v_34)) (not (= ?v_63 ?v_35))))) (and (and (not (= ?v_56 ?v_5)) (and (and (not (= ?v_5 ?v_57)) (not (= ?v_5 ?v_58))) (and (not (= ?v_56 ?v_12)) (not (= ?v_56 ?v_13))))) (and (and (not (= ?v_63 ?v_28)) (and (and (not (= ?v_28 ?v_64)) (not (= ?v_28 ?v_65))) (and (not (= ?v_63 ?v_59)) (not (= ?v_63 ?v_60))))) (and (and (not (= ?v_56 ?v_44)) (and (and (not (= ?v_44 ?v_57)) (not (= ?v_44 ?v_58))) (and (not (= ?v_56 ?v_52)) (not (= ?v_56 ?v_53))))) (and (and (not (= ?v_63 ?v_33)) (and (and (not (= ?v_33 ?v_64)) (not (= ?v_33 ?v_65))) (and (not (= ?v_63 ?v_46)) (not (= ?v_63 ?v_47))))) (and (and (not (= ?v_56 ?v_22)) (and (and (not (= ?v_22 ?v_57)) (not (= ?v_22 ?v_58))) (and (not (= ?v_56 ?v_23)) (not (= ?v_56 ?v_24))))) (and (and (not (= ?v_63 ?v_38)) (and (and (not (= ?v_38 ?v_64)) (not (= ?v_38 ?v_65))) (and (not (= ?v_63 ?v_48)) (not (= ?v_63 ?v_49))))) (and (and (not (= ?v_63 ?v_41)) (and (and (not (= ?v_41 ?v_64)) (not (= ?v_41 ?v_65))) (and (not (= ?v_63 ?v_50)) (not (= ?v_63 ?v_51))))) (and (and (not (= ?v_63 ?v_5)) (and (and (not (= ?v_5 ?v_64)) (not (= ?v_5 ?v_65))) (and (not (= ?v_63 ?v_12)) (not (= ?v_63 ?v_13))))) (and (and (not (= ?v_63 ?v_44)) (and (and (not (= ?v_44 ?v_64)) (not (= ?v_44 ?v_65))) (and (not (= ?v_63 ?v_52)) (not (= ?v_63 ?v_53))))) (and (and (not (= ?v_63 ?v_22)) (and (and (not (= ?v_22 ?v_64)) (not (= ?v_22 ?v_65))) (and (not (= ?v_63 ?v_23)) (not (= ?v_63 ?v_24))))) (and (and (not (= ?v_28 ?v_33)) (and (and (not (= ?v_33 ?v_59)) (not (= ?v_33 ?v_60))) (and (not (= ?v_28 ?v_46)) (not (= ?v_28 ?v_47))))) (and (and (not (= ?v_28 ?v_38)) (and (and (not (= ?v_38 ?v_59)) (not (= ?v_38 ?v_60))) (and (not (= ?v_28 ?v_48)) (not (= ?v_28 ?v_49))))) (and (and (not (= ?v_28 ?v_41)) (and (and (not (= ?v_41 ?v_59)) (not (= ?v_41 ?v_60))) (and (not (= ?v_28 ?v_50)) (not (= ?v_28 ?v_51))))) (and (and (not (= ?v_28 ?v_5)) (and (and (not (= ?v_5 ?v_59)) (not (= ?v_5 ?v_60))) (and (not (= ?v_28 ?v_12)) (not (= ?v_28 ?v_13))))) (and (and (not (= ?v_28 ?v_44)) (and (and (not (= ?v_44 ?v_59)) (not (= ?v_44 ?v_60))) (and (not (= ?v_28 ?v_52)) (not (= ?v_28 ?v_53))))) (and (and (not (= ?v_28 ?v_22)) (and (and (not (= ?v_22 ?v_59)) (not (= ?v_22 ?v_60))) (and (not (= ?v_28 ?v_23)) (not (= ?v_28 ?v_24))))) (and (and (not (= ?v_56 ?v_1)) (and (and (not (= ?v_1 ?v_57)) (not (= ?v_1 ?v_58))) (and (not (= ?v_56 ?v_16)) (not (= ?v_56 ?v_17))))) (and (and (not (= ?v_56 ?v_11)) (and (and (not (= ?v_11 ?v_57)) (not (= ?v_11 ?v_58))) (and (not (= ?v_56 ?v_18)) (not (= ?v_56 ?v_19))))) (and (and (not (= ?v_63 ?v_1)) (and (and (not (= ?v_1 ?v_64)) (not (= ?v_1 ?v_65))) (and (not (= ?v_63 ?v_16)) (not (= ?v_63 ?v_17))))) (and (and (not (= ?v_63 ?v_11)) (and (and (not (= ?v_11 ?v_64)) (not (= ?v_11 ?v_65))) (and (not (= ?v_63 ?v_18)) (not (= ?v_63 ?v_19))))) (and (and (not (= ?v_38 ?v_41)) (and (and (not (= ?v_41 ?v_48)) (not (= ?v_41 ?v_49))) (and (not (= ?v_38 ?v_50)) (not (= ?v_38 ?v_51))))) (and (and (not (= ?v_38 ?v_5)) (and (and (not (= ?v_5 ?v_48)) (not (= ?v_5 ?v_49))) (and (not (= ?v_38 ?v_12)) (not (= ?v_38 ?v_13))))) (and (and (not (= ?v_38 ?v_44)) (and (and (not (= ?v_44 ?v_48)) (not (= ?v_44 ?v_49))) (and (not (= ?v_38 ?v_52)) (not (= ?v_38 ?v_53))))) (and (and (not (= ?v_38 ?v_22)) (and (and (not (= ?v_22 ?v_48)) (not (= ?v_22 ?v_49))) (and (not (= ?v_38 ?v_23)) (not (= ?v_38 ?v_24))))) (and (and (not (= ?v_28 ?v_1)) (and (and (not (= ?v_1 ?v_59)) (not (= ?v_1 ?v_60))) (and (not (= ?v_28 ?v_16)) (not (= ?v_28 ?v_17))))) (and (and (not (= ?v_28 ?v_11)) (and (and (not (= ?v_11 ?v_59)) (not (= ?v_11 ?v_60))) (and (not (= ?v_28 ?v_18)) (not (= ?v_28 ?v_19))))) (and (and (not (= ?v_5 ?v_44)) (and (and (not (= ?v_44 ?v_12)) (not (= ?v_44 ?v_13))) (and (not (= ?v_5 ?v_52)) (not (= ?v_5 ?v_53))))) (and (and (not (= ?v_5 ?v_22)) (and (and (not (= ?v_22 ?v_12)) (not (= ?v_22 ?v_13))) (and (not (= ?v_5 ?v_23)) (not (= ?v_5 ?v_24))))) (and (and (not (= ?v_38 ?v_1)) (and (and (not (= ?v_1 ?v_48)) (not (= ?v_1 ?v_49))) (and (not (= ?v_38 ?v_16)) (not (= ?v_38 ?v_17))))) (and (and (not (= ?v_38 ?v_11)) (and (and (not (= ?v_11 ?v_48)) (not (= ?v_11 ?v_49))) (and (not (= ?v_38 ?v_18)) (not (= ?v_38 ?v_19))))) (and (separation1 ?v_6 ?v_9) (and (valid_acc ?v_9) (and (valid_acc ?v_6) (and (valid_acc_range ?v_9 5) (valid_acc_range ?v_6 5))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (=> ?v_66 (forall ((?anonymous_2_v1_global0 c_unique)) (forall ((?anonymous_2_v2_global0 c_unique)) (forall ((?intM_global0 c_unique)) (let ((?v_67 (type_memory c_int type_global)) (?v_69 (type_pset type_global))) (let ((?v_68 (c_sort ?v_69 (pset_singleton ?v_14)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global) (c_sort ?v_67 ?anonymous_2_v1_global0) ?v_68) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global) (c_sort ?v_67 ?anonymous_2_v2_global0) ?v_68)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global) (c_sort ?v_67 ?intM_global0) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_14)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_14)))) 0 4)))))) (=> (valid ?v_25 ?v_8) (forall ((?anonymous_2_v1_global1 c_unique)) (forall ((?anonymous_2_v2_global1 c_unique)) (forall ((?intM_global1 c_unique)) (let ((?v_70 (c_sort ?v_69 (pset_singleton ?v_8)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global0) (c_sort ?v_67 ?anonymous_2_v1_global1) ?v_70) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global0) (c_sort ?v_67 ?anonymous_2_v2_global1) ?v_70)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global0) (c_sort ?v_67 ?intM_global1) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_8)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_8)))) 0 4)))))) (=> (valid ?v_25 ?v_20) (forall ((?anonymous_2_v1_global2 c_unique)) (forall ((?anonymous_2_v2_global2 c_unique)) (forall ((?intM_global2 c_unique)) (let ((?v_71 (c_sort ?v_69 (pset_singleton ?v_20)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global1) (c_sort ?v_67 ?anonymous_2_v1_global2) ?v_71) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global1) (c_sort ?v_67 ?anonymous_2_v2_global2) ?v_71)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global1) (c_sort ?v_67 ?intM_global2) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_20)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_20)))) 0 4)))))) (=> (valid ?v_25 ?v_43) (forall ((?anonymous_2_v1_global3 c_unique)) (forall ((?anonymous_2_v2_global3 c_unique)) (forall ((?intM_global3 c_unique)) (let ((?v_72 (c_sort ?v_69 (pset_singleton ?v_43)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global2) (c_sort ?v_67 ?anonymous_2_v1_global3) ?v_72) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global2) (c_sort ?v_67 ?anonymous_2_v2_global3) ?v_72)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global2) (c_sort ?v_67 ?intM_global3) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_43)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_43)))) 0 4)))))) (=> (valid ?v_25 ?v_3) (forall ((?anonymous_2_v1_global4 c_unique)) (forall ((?anonymous_2_v2_global4 c_unique)) (forall ((?intM_global4 c_unique)) (let ((?v_73 (c_sort ?v_69 (pset_singleton ?v_3)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global3) (c_sort ?v_67 ?anonymous_2_v1_global4) ?v_73) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global3) (c_sort ?v_67 ?anonymous_2_v2_global4) ?v_73)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global3) (c_sort ?v_67 ?intM_global4) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_3)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_3)))) 0 4)))))) (=> (valid ?v_25 ?v_40) (forall ((?anonymous_2_v1_global5 c_unique)) (forall ((?anonymous_2_v2_global5 c_unique)) (forall ((?intM_global5 c_unique)) (let ((?v_74 (c_sort ?v_69 (pset_singleton ?v_40)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global4) (c_sort ?v_67 ?anonymous_2_v1_global5) ?v_74) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global4) (c_sort ?v_67 ?anonymous_2_v2_global5) ?v_74)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global4) (c_sort ?v_67 ?intM_global5) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_40)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_40)))) 0 4)))))) (=> (valid ?v_25 ?v_37) (forall ((?anonymous_2_v1_global6 c_unique)) (forall ((?anonymous_2_v2_global6 c_unique)) (forall ((?intM_global6 c_unique)) (let ((?v_75 (c_sort ?v_69 (pset_singleton ?v_37)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global5) (c_sort ?v_67 ?anonymous_2_v1_global6) ?v_75) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global5) (c_sort ?v_67 ?anonymous_2_v2_global6) ?v_75)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global5) (c_sort ?v_67 ?intM_global6) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_37)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_37)))) 0 4)))))) (=> (valid ?v_25 ?v_32) (forall ((?anonymous_2_v1_global7 c_unique)) (forall ((?anonymous_2_v2_global7 c_unique)) (forall ((?intM_global7 c_unique)) (let ((?v_76 (c_sort ?v_69 (pset_singleton ?v_32)))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global6) (c_sort ?v_67 ?anonymous_2_v1_global7) ?v_76) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global6) (c_sort ?v_67 ?anonymous_2_v2_global7) ?v_76)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global6) (c_sort ?v_67 ?intM_global7) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_32)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_32)))) 0 4)))))) (=> (valid ?v_25 ?v_27) (forall ((?anonymous_2_v1_global8 c_unique)) (forall ((?anonymous_2_v2_global8 c_unique)) (forall ((?intM_global8 c_unique)) (let ((?v_77 (c_sort ?v_69 (pset_singleton ?v_27))) (?v_78 (offset ?v_26))) (=> (and (and (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v1_global7) (c_sort ?v_67 ?anonymous_2_v1_global8) ?v_77) (not_assigns ?v_25 (c_sort ?v_67 ?anonymous_2_v2_global7) (c_sort ?v_67 ?anonymous_2_v2_global8) ?v_77)) (not_assigns ?v_25 (c_sort ?v_67 ?intM_global7) (c_sort ?v_67 ?intM_global8) (c_sort ?v_69 (pset_union (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_9 ?v_27)))) 0 4)) (c_sort ?v_69 (pset_range (c_sort ?v_69 (pset_singleton (c_sort ?v_0 (acc ?v_6 ?v_27)))) 0 4)))))) (and (<= 0 ?v_78) (< ?v_78 (block_length ?v_25 ?v_26))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) +(check-sat) +(exit)