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 \
if( options::ufssSymBreak() ){
options::sortInference.set( true );
}
- if( options::qcfMode.wasSetByUser() ){
+ if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
options::quantConflictFind.set( true );
}
* - (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:
}
}
+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);
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;
--- /dev/null
+/********************* */
+/*! \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<int>& simplexRounds)
+ : d_alg(Simplex)
+{}
+
+Algorithms InferBoundAlgorithm::getAlgorithm() const{
+ return d_alg;
+}
+
+const Maybe<int>& 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<int>& 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 */
--- /dev/null
+/********************* */
+/*! \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 <ostream>
+
+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<int> d_simplexRounds;
+ InferBoundAlgorithm(Algorithms a);
+ InferBoundAlgorithm(const Maybe<int>& simplexRounds);
+
+public:
+ InferBoundAlgorithm();
+
+ Algorithms getAlgorithm() const;
+ const Maybe<int>& getSimplexRounds() const;
+
+ static InferBoundAlgorithm mkLookup();
+ static InferBoundAlgorithm mkRowSum();
+ static InferBoundAlgorithm mkSimplex(const Maybe<int>& rounds);
+};
+
+std::ostream& operator<<(std::ostream& os, const Algorithms a);
+} /* namespace inferbounds */
+
+class ArithEntailmentCheckParameters : public EntailmentCheckParameters {
+private:
+ typedef std::vector<inferbounds::InferBoundAlgorithm> 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 */
#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;
return d_internal->getModelValue( var );
}
+
+std::pair<bool, Node> 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<const ArithEntailmentCheckParameters*>(params);
+ }
+ Assert(aparams != NULL);
+
+ ArithEntailmentCheckSideEffects* ase = NULL;
+ if(out == NULL){
+ ase = new ArithEntailmentCheckSideEffects();
+ }else{
+ AlwaysAssert(out->getTheoryId() == getId());
+ ase = dynamic_cast<ArithEntailmentCheckSideEffects*>(out);
+ }
+ Assert(ase != NULL);
+
+ std::pair<bool, Node> 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 */
#include "expr/node.h"
#include "theory/arith/theory_arith_private_forward.h"
+
namespace CVC4 {
namespace theory {
void addSharedTerm(TNode n);
Node getModelValue(TNode var);
+
+
+ std::pair<bool, Node> entailmentCheck(TNode lit,
+ const EntailmentCheckParameters* params,
+ EntailmentCheckSideEffects* out);
+
};/* class TheoryArith */
}/* CVC4::theory::arith namespace */
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),
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){
return d_rowTracking[ridx];
}
+
Node TheoryArithPrivate::expandDefinition(LogicRequest &logicRequest, Node node) {
NodeManager* nm = NodeManager::currentNM();
}
+
+
+// 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<bool, Node> 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<bool>(), 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<Node, DeltaRational> bestPrimLeft, bestNegPrimRight, bestPrimDiff, tmp;
+ std::pair<Node, DeltaRational> 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<Node, DeltaRational>&, 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<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& 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<bool, Node> 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<Node, DeltaRational> 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 << ") : " <<left << endl
+ << " right:" << rc << " + " << rm << "*(" << rp << ") : " << right << endl
+ << " diff: " << dc << " + " << dm << "*("<< dp <<"): " << diff << endl
+ << " sep: " << sep << endl;
+
+
+ // k in LT, LEQ, EQUAL, DISEQUAL
+ // [dir*lm*( lp ) + dir*lc] k [dir*rm*( rp ) + dir*rc]
+ Rational change = rc - lc;
+ Assert(change == (-dc));
+ // [dir*lm*( lp )] k [dir*rm*( rp ) + dir*(rc - lc)]
+ if(normKind == LT){
+ sep = DeltaRational(change, Rational(-1));
+ k = LEQ;
+ }else{
+ sep = DeltaRational(change);
+ k = normKind;
+ }
+ // k in LEQ, EQUAL, DISEQUAL
+ // dir*lm*( lp ) k [dir*rm*( rp )] + dir*(sep + d * delta)
+ return true;
+}
+
+/**
+ * Precondition:
+ * tp is a polynomial not containing an ite.
+ * either tp is constant or contains no constants.
+ * Post:
+ * if tmp.first is not null, then
+ * sgn * tp <= sgn * tmp.second
+ */
+void TheoryArithPrivate::entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& 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<Rational>());
+ }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<Node, DeltaRational>& 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<Node, DeltaRational> 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<DeltaRational> threshold;
+ // TODO: get this from the parameters
+
+ // setup term
+ Polynomial p = Polynomial::parsePolynomial(tp);
+ vector<ArithVar> variables;
+ vector<Rational> 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<ArithVar> variables;
+// vector<Rational> 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 */
#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"
class TreeLog;
class ApproximateStatistics;
+class ArithEntailmentCheckParameters;
+class ArithEntailmentCheckSideEffects;
+namespace inferbounds {
+ class InferBoundAlgorithm;
+}
+class InferBoundsResult;
+
/**
* Implementation of QF_LRA.
* Based upon:
void releaseArithVar(ArithVar v);
void signal(ArithVar v){ d_errorSet.signalVariable(v); }
+
private:
+ // t does not contain constants
+ void entailmentCheckBoundLookup(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
+ void entailmentCheckRowSum(std::pair<Node, DeltaRational>& tmp, int sgn, TNode tp) const;
+
+ std::pair<Node, DeltaRational> 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
+ * -- <dr, exp> 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 <v, term> 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 <threshold, term>
+ */
+ //std::pair<DeltaRational, Node> 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<Node, DeltaRational>& min, const std::pair<Node, DeltaRational>& e);
+
/**
* The map between arith variables to nodes.
*/
Node getModelValue(TNode var);
+
+ std::pair<bool, Node> entailmentCheck(TNode lit, const ArithEntailmentCheckParameters& params, ArithEntailmentCheckSideEffects& out);
+
+
private:
/** The constant zero. */
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;
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);
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(){
StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith);
StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_arith_minus);
StatisticsRegistry::unregisterStat(&d_instantiations_cbqi_datatypes);
+ StatisticsRegistry::unregisterStat(&d_instantiation_rounds);
}
IntStat d_instantiations_cbqi_arith;
IntStat d_instantiations_cbqi_arith_minus;
IntStat d_instantiations_cbqi_datatypes;
+ IntStat d_instantiation_rounds;
Statistics();
~Statistics();
};
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
d_mg = new MatchGen( this, qn );\r
\r
if( d_mg->isValid() ){\r
- for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){\r
- if( d_vars[j].getKind()!=BOUND_VARIABLE ){\r
- bool beneathQuant = d_nbeneathQuant.find( d_vars[j] )==d_nbeneathQuant.end();\r
- d_var_mg[j] = new MatchGen( this, d_vars[j], true, beneathQuant );\r
- if( !d_var_mg[j]->isValid() ){\r
- d_mg->setInvalid();\r
- break;\r
- }else{\r
- std::vector< int > bvars;\r
- d_var_mg[j]->determineVariableOrder( this, bvars );\r
- }\r
+ /*\r
+ for( unsigned j=0; j<q[0].getNumChildren(); j++ ){\r
+ if( d_inMatchConstraint.find( q[0][j] )==d_inMatchConstraint.end() ){\r
+ Trace("qcf-invalid") << "QCF invalid : variable " << q[0][j] << " does not exist in a matching constraint." << std::endl;\r
+ d_mg->setInvalid();\r
+ break;\r
}\r
}\r
-\r
+ */\r
if( d_mg->isValid() ){\r
- std::vector< int > bvars;\r
- d_mg->determineVariableOrder( this, bvars );\r
+ for( unsigned j=q[0].getNumChildren(); j<d_vars.size(); j++ ){\r
+ if( d_vars[j].getKind()!=BOUND_VARIABLE ){\r
+ d_var_mg[j] = NULL;\r
+ bool is_tsym = false;\r
+ if( !MatchGen::isHandledUfTerm( d_vars[j] ) && d_vars[j].getKind()!=ITE ){\r
+ is_tsym = true;\r
+ d_tsym_vars.push_back( j );\r
+ }\r
+ if( !is_tsym || options::qcfTConstraint() ){\r
+ d_var_mg[j] = new MatchGen( this, d_vars[j], true );\r
+ }\r
+ if( !d_var_mg[j] || !d_var_mg[j]->isValid() ){\r
+ Trace("qcf-invalid") << "QCF invalid : cannot match for " << d_vars[j] << std::endl;\r
+ d_mg->setInvalid();\r
+ break;\r
+ }else{\r
+ std::vector< int > bvars;\r
+ d_var_mg[j]->determineVariableOrder( this, bvars );\r
+ }\r
+ }\r
+ }\r
+ if( d_mg->isValid() ){\r
+ std::vector< int > bvars;\r
+ d_mg->determineVariableOrder( this, bvars );\r
+ }\r
}\r
+ }else{\r
+ Trace("qcf-invalid") << "QCF invalid : body of formula cannot be processed." << std::endl;\r
}\r
Trace("qcf-qregister-summary") << "QCF register : " << ( d_mg->isValid() ? "VALID " : "INVALID" ) << " : " << q << std::endl;\r
}\r
for( unsigned i=1; i<=2; i++ ){\r
flatten( n[i], beneathQuant );\r
}\r
+ registerNode( n[0], false, pol, beneathQuant );\r
+ }else if( options::qcfTConstraint() ){\r
+ //a theory-specific predicate\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ flatten( n[i], beneathQuant );\r
+ }\r
}\r
}\r
- }\r
- if( isVar( n ) && !beneathQuant ){\r
- d_nbeneathQuant[n] = true;\r
- }\r
- for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
- bool newHasPol;\r
- bool newPol;\r
- QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
- //QcfNode * qcfc = new QcfNode( d_c );\r
- //qcfc->d_parent = qcf;\r
- //qcf->d_child[i] = qcfc;\r
- registerNode( n[i], newHasPol, newPol, beneathQuant );\r
+ }else{\r
+ for( unsigned i=0; i<n.getNumChildren(); i++ ){\r
+ bool newHasPol;\r
+ bool newPol;\r
+ QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );\r
+ //QcfNode * qcfc = new QcfNode( d_c );\r
+ //qcfc->d_parent = qcf;\r
+ //qcf->d_child[i] = qcfc;\r
+ registerNode( n[i], newHasPol, newPol, beneathQuant );\r
+ }\r
}\r
}\r
}\r
void QuantInfo::flatten( Node n, bool beneathQuant ) {\r
Trace("qcf-qregister-debug2") << "Flatten : " << n << std::endl;\r
if( n.hasBoundVar() ){\r
+ if( n.getKind()==BOUND_VARIABLE ){\r
+ d_inMatchConstraint[n] = true;\r
+ }\r
+ //if( MatchGen::isHandledUfTerm( n ) || n.getKind()==ITE ){\r
if( d_var_num.find( n )==d_var_num.end() ){\r
Trace("qcf-qregister-debug2") << "Add FLATTEN VAR : " << n << std::endl;\r
d_var_num[n] = d_vars.size();\r
flatten( n[i], beneathQuant );\r
}\r
}\r
- if( !beneathQuant ){\r
- d_nbeneathQuant[n] = true;\r
- }\r
}else{\r
Trace("qcf-qregister-debug2") << "...already processed" << std::endl;\r
}\r
d_match_term[i] = TNode::null();\r
}\r
d_curr_var_deq.clear();\r
+ d_tconstraints.clear();\r
//add built-in variable constraints\r
for( unsigned r=0; r<2; r++ ){\r
for( std::map< int, std::vector< Node > >::iterator it = d_var_constraint[r].begin();\r
}else if( chDiseq && !isVar( n ) && !isVar( cv ) ){\r
//they must actually be disequal if we are looking for conflicts\r
if( !p->areDisequal( n, cv ) ){\r
+ //TODO : check for entailed disequal\r
+\r
return false;\r
}\r
}\r
return false;\r
}\r
\r
+bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms ) {\r
+ if( !d_tconstraints.empty() ){\r
+ //check constraints\r
+ for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){\r
+ //apply substitution to the tconstraint\r
+ Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),\r
+ p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),\r
+ terms.begin(), terms.end() );\r
+ cons = it->second ? cons : cons.negate();\r
+ if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){\r
+ return true;\r
+ }\r
+ }\r
+ }\r
+ return false;\r
+}\r
+\r
+bool QuantInfo::entailmentTest( QuantConflictFind * p, Node lit, bool chEnt ) {\r
+ Trace("qcf-tconstraint-debug") << "Check : " << lit << std::endl;\r
+ Node rew = Rewriter::rewrite( lit );\r
+ if( rew==p->d_false ){\r
+ Trace("qcf-tconstraint-debug") << "...constraint " << lit << " is disentailed (rewrites to false)." << std::endl;\r
+ return false;\r
+ }else if( rew!=p->d_true ){\r
+ //if checking for conflicts, we must be sure that the constraint is entailed\r
+ if( chEnt ){\r
+ //check if it is entailed\r
+ Trace("qcf-tconstraint-debug") << "Check entailment of " << rew << "..." << std::endl;\r
+ std::pair<bool, Node> et = p->getQuantifiersEngine()->getTheoryEngine()->entailmentCheck(THEORY_OF_TYPE_BASED, rew );\r
+ ++(p->d_statistics.d_entailment_checks);\r
+ Trace("qcf-tconstraint-debug") << "ET result : " << et.first << " " << et.second << std::endl;\r
+ if( !et.first ){\r
+ Trace("qcf-tconstraint-debug") << "...cannot show entailment of " << rew << "." << std::endl;\r
+ return false;\r
+ }else{\r
+ return true;\r
+ }\r
+ }else{\r
+ Trace("qcf-tconstraint-debug") << "...does not need to be entailed." << std::endl;\r
+ return true;\r
+ }\r
+ }else{\r
+ Trace("qcf-tconstraint-debug") << "...rewrites to true." << std::endl;\r
+ return true;\r
+ }\r
+}\r
+\r
bool QuantInfo::completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue ) {\r
//assign values for variables that were unassigned (usually not necessary, but handles corner cases)\r
bool doFail = false;\r
doFail = true;\r
success = false;\r
}else{\r
- d_unassigned.clear();\r
- d_unassigned_tn.clear();\r
- std::vector< int > unassigned[2];\r
- std::vector< TypeNode > unassigned_tn[2];\r
- for( int i=0; i<getNumVars(); i++ ){\r
- if( d_match[i].isNull() ){\r
- int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
- unassigned[rindex].push_back( i );\r
- unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
- assigned.push_back( i );\r
- }\r
- }\r
- d_unassigned_nvar = unassigned[0].size();\r
- for( unsigned i=0; i<2; i++ ){\r
- d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );\r
- d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );\r
+ //solve for interpreted symbol matches\r
+ // this breaks the invariant that all introduced constraints are over existing terms\r
+ for( int i=(int)(d_tsym_vars.size()-1); i>=0; i-- ){\r
+ int index = d_tsym_vars[i];\r
+ TNode v = getCurrentValue( d_vars[index] );\r
+ int slv_v = -1;\r
+ if( v==d_vars[index] ){\r
+ slv_v = index;\r
+ }\r
+ Trace("qcf-tconstraint-debug") << "Solve " << d_vars[index] << " = " << v << " " << d_vars[index].getKind() << std::endl;\r
+ if( d_vars[index].getKind()==PLUS || d_vars[index].getKind()==MULT ){\r
+ Kind k = d_vars[index].getKind();\r
+ std::vector< TNode > children;\r
+ for( unsigned j=0; j<d_vars[index].getNumChildren(); j++ ){\r
+ int vn = getVarNum( d_vars[index][j] );\r
+ if( vn!=-1 ){\r
+ TNode vv = getCurrentValue( d_vars[index][j] );\r
+ if( vv==d_vars[index][j] ){\r
+ //we will assign this\r
+ if( slv_v==-1 ){\r
+ Trace("qcf-tconstraint-debug") << "...will solve for var #" << vn << std::endl;\r
+ slv_v = vn;\r
+ if( p->d_effort!=QuantConflictFind::effort_conflict ){\r
+ break;\r
+ }\r
+ }else{\r
+ Node z = p->getZero( k );\r
+ if( !z.isNull() ){\r
+ Trace("qcf-tconstraint-debug") << "...set " << d_vars[vn] << " = " << z << std::endl;\r
+ assigned.push_back( vn );\r
+ if( !setMatch( p, vn, z ) ){\r
+ success = false;\r
+ break;\r
+ }\r
+ }\r
+ }\r
+ }else{\r
+ Trace("qcf-tconstraint-debug") << "...sum value " << vv << std::endl;\r
+ children.push_back( vv );\r
+ }\r
+ }else{\r
+ Trace("qcf-tconstraint-debug") << "...sum " << d_vars[index][j] << std::endl;\r
+ children.push_back( d_vars[index][j] );\r
+ }\r
+ }\r
+ if( success ){\r
+ if( slv_v!=-1 ){\r
+ Node lhs;\r
+ if( children.empty() ){\r
+ lhs = p->getZero( k );\r
+ }else if( children.size()==1 ){\r
+ lhs = children[0];\r
+ }else{\r
+ lhs = NodeManager::currentNM()->mkNode( k, children );\r
+ }\r
+ Node sum;\r
+ if( v==d_vars[index] ){\r
+ sum = lhs;\r
+ }else{\r
+ if( p->d_effort==QuantConflictFind::effort_conflict ){\r
+ Kind kn = k;\r
+ if( d_vars[index].getKind()==PLUS ){\r
+ kn = MINUS;\r
+ }\r
+ if( kn!=k ){\r
+ sum = NodeManager::currentNM()->mkNode( kn, v, lhs );\r
+ }\r
+ }\r
+ }\r
+ if( !sum.isNull() ){\r
+ assigned.push_back( slv_v );\r
+ Trace("qcf-tconstraint-debug") << "...set " << d_vars[slv_v] << " = " << sum << std::endl;\r
+ if( !setMatch( p, slv_v, sum ) ){\r
+ success = false;\r
+ }\r
+ p->d_tempCache.push_back( sum );\r
+ }\r
+ }else{\r
+ //must show that constraint is met\r
+ Node sum = NodeManager::currentNM()->mkNode( k, children );\r
+ Node eq = sum.eqNode( v );\r
+ if( !entailmentTest( p, eq ) ){\r
+ success = false;\r
+ }\r
+ p->d_tempCache.push_back( sum );\r
+ }\r
+ }\r
+ }\r
+\r
+ if( !success ){\r
+ break;\r
+ }\r
+ }\r
+ if( success ){\r
+ //check what is left to assign\r
+ d_unassigned.clear();\r
+ d_unassigned_tn.clear();\r
+ std::vector< int > unassigned[2];\r
+ std::vector< TypeNode > unassigned_tn[2];\r
+ for( int i=0; i<getNumVars(); i++ ){\r
+ if( d_match[i].isNull() ){\r
+ int rindex = d_var_mg.find( i )==d_var_mg.end() ? 1 : 0;\r
+ unassigned[rindex].push_back( i );\r
+ unassigned_tn[rindex].push_back( getVar( i ).getType() );\r
+ assigned.push_back( i );\r
+ }\r
+ }\r
+ d_unassigned_nvar = unassigned[0].size();\r
+ for( unsigned i=0; i<2; i++ ){\r
+ d_unassigned.insert( d_unassigned.end(), unassigned[i].begin(), unassigned[i].end() );\r
+ d_unassigned_tn.insert( d_unassigned_tn.end(), unassigned_tn[i].begin(), unassigned_tn[i].end() );\r
+ }\r
+ d_una_eqc_count.clear();\r
+ d_una_index = 0;\r
}\r
- d_una_eqc_count.clear();\r
- d_una_index = 0;\r
}\r
- if( !d_unassigned.empty() ){\r
+\r
+ if( !d_unassigned.empty() && ( success || doContinue ) ){\r
Trace("qcf-check") << "Assign to unassigned..." << std::endl;\r
do {\r
if( doFail ){\r
}while( success && isMatchSpurious( p ) );\r
}\r
if( success ){\r
+ for( unsigned i=0; i<d_unassigned.size(); i++ ){\r
+ int ui = d_unassigned[i];\r
+ if( !d_match[ui].isNull() ){\r
+ Trace("qcf-check") << " Assigned #" << ui << " : " << d_vars[ui] << " -> " << d_match[ui] << std::endl;\r
+ }\r
+ }\r
return true;\r
}else{\r
for( unsigned i=0; i<assigned.size(); i++ ){\r
}\r
Trace(c) << std::endl;\r
}\r
+ if( !d_tconstraints.empty() ){\r
+ Trace(c) << "ADDITIONAL CONSTRAINTS : " << std::endl;\r
+ for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){\r
+ Trace(c) << " " << it->first << " -> " << it->second << std::endl;\r
+ }\r
+ }\r
}\r
\r
-//void QuantInfo::addFuncParent( int v, Node f, int arg ) {\r
-// if( std::find( d_f_parent[v][f].begin(), d_f_parent[v][f].end(), arg )==d_f_parent[v][f].end() ){\r
-// d_f_parent[v][f].push_back( arg );\r
-// }\r
-//}\r
-\r
-MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar, bool beneathQuant ){\r
- Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << ", beneathQuant = " << beneathQuant << std::endl;\r
+MatchGen::MatchGen( QuantInfo * qi, Node n, bool isVar ){\r
+ Trace("qcf-qregister-debug") << "Make match gen for " << n << ", isVar = " << isVar << std::endl;\r
std::vector< Node > qni_apps;\r
d_qni_size = 0;\r
if( isVar ){\r
Assert( qi->d_var_num.find( n )!=qi->d_var_num.end() );\r
- if( isHandledUfTerm( n ) ){\r
- d_qni_var_num[0] = qi->getVarNum( n );\r
- d_qni_size++;\r
- d_type = typ_var;\r
- d_type_not = false;\r
- d_n = n;\r
- //Node f = getOperator( n );\r
- for( unsigned j=0; j<d_n.getNumChildren(); j++ ){\r
- Node nn = d_n[j];\r
- Trace("qcf-qregister-debug") << " " << d_qni_size;\r
- if( qi->isVar( nn ) ){\r
- int v = qi->d_var_num[nn];\r
- Trace("qcf-qregister-debug") << " is var #" << v << std::endl;\r
- d_qni_var_num[d_qni_size] = v;\r
- //qi->addFuncParent( v, f, j );\r
- }else{\r
- Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
- d_qni_gterm[d_qni_size] = nn;\r
- }\r
- d_qni_size++;\r
- }\r
- }else if( n.getKind()==ITE ){\r
+ if( n.getKind()==ITE ){\r
d_type = typ_ite_var;\r
d_type_not = false;\r
d_n = n;\r
d_type = typ_invalid;\r
}\r
}else{\r
- //for now, unknown term\r
- d_type = typ_invalid;\r
+ d_type = isHandledUfTerm( n ) ? typ_var : typ_tsym;\r
+ d_qni_var_num[0] = qi->getVarNum( n );\r
+ d_qni_size++;\r
+ d_type_not = false;\r
+ d_n = n;\r
+ //Node f = getOperator( n );\r
+ for( unsigned j=0; j<d_n.getNumChildren(); j++ ){\r
+ Node nn = d_n[j];\r
+ Trace("qcf-qregister-debug") << " " << d_qni_size;\r
+ if( qi->isVar( nn ) ){\r
+ int v = qi->d_var_num[nn];\r
+ Trace("qcf-qregister-debug") << " is var #" << v << std::endl;\r
+ d_qni_var_num[d_qni_size] = v;\r
+ //qi->addFuncParent( v, f, j );\r
+ }else{\r
+ Trace("qcf-qregister-debug") << " is gterm " << nn << std::endl;\r
+ d_qni_gterm[d_qni_size] = nn;\r
+ }\r
+ d_qni_size++;\r
+ }\r
}\r
}else{\r
if( n.hasBoundVar() ){\r
if( isHandledBoolConnective( d_n ) ){\r
//non-literals\r
d_type = typ_formula;\r
- bool nBeneathQuant = beneathQuant || d_n.getKind()==FORALL;\r
for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
if( d_n.getKind()!=FORALL || i==1 ){\r
- d_children.push_back( MatchGen( qi, d_n[i], false, nBeneathQuant ) );\r
+ d_children.push_back( MatchGen( qi, d_n[i], false ) );\r
if( !d_children[d_children.size()-1].isValid() ){\r
setInvalid();\r
break;\r
}else{\r
d_type = typ_invalid;\r
//literals\r
- if( d_n.getKind()==EQUAL ){\r
- for( unsigned i=0; i<2; i++ ){\r
+ if( isHandledUfTerm( d_n ) ){\r
+ Assert( qi->isVar( d_n ) );\r
+ d_type = typ_pred;\r
+ }else if( d_n.getKind()==BOUND_VARIABLE ){\r
+ Assert( d_n.getType().isBoolean() );\r
+ d_type = typ_bool_var;\r
+ }else if( d_n.getKind()==EQUAL || options::qcfTConstraint() ){\r
+ for( unsigned i=0; i<d_n.getNumChildren(); i++ ){\r
if( d_n[i].hasBoundVar() ){\r
if( !qi->isVar( d_n[i] ) ){\r
Trace("qcf-qregister-debug") << "ERROR : not var " << d_n[i] << std::endl;\r
}\r
Assert( qi->isVar( d_n[i] ) );\r
+ if( d_n.getKind()!=EQUAL && qi->isVar( d_n[i] ) ){\r
+ d_qni_var_num[i+1] = qi->d_var_num[d_n[i]];\r
+ }\r
}else{\r
d_qni_gterm[i] = d_n[i];\r
}\r
}\r
- d_type = typ_eq;\r
- }else if( isHandledUfTerm( d_n ) ){\r
- Assert( qi->isVar( d_n ) );\r
- d_type = typ_pred;\r
- }else if( d_n.getKind()==BOUND_VARIABLE ){\r
- d_type = typ_bool_var;\r
- }else{\r
- Trace("qcf-invalid") << "Unhandled : " << d_n << std::endl;\r
+ d_type = d_n.getKind()==EQUAL ? typ_eq : typ_tconstraint;\r
+ Trace("qcf-tconstraint") << "T-Constraint : " << d_n << std::endl;\r
}\r
}\r
}else{\r
\r
//set up processing matches\r
if( d_type==typ_invalid ){\r
- //do nothing : return success once?\r
+ //do nothing\r
}else if( d_type==typ_ground ){\r
if( d_ground_eval[0]==( d_tgt ? p->d_true : p->d_false ) ){\r
d_child_counter = 0;\r
d_qn.push_back( qni );\r
}\r
d_matched_basis = false;\r
+ }else if( d_type==typ_tsym || d_type==typ_tconstraint ){\r
+ for( std::map< int, int >::iterator it = d_qni_var_num.begin(); it != d_qni_var_num.end(); ++it ){\r
+ int repVar = qi->getCurrentRepVar( it->second );\r
+ if( qi->d_match[repVar].isNull() ){\r
+ Debug("qcf-match-debug") << "Force matching on child #" << it->first << ", which is var #" << repVar << std::endl;\r
+ d_qni_bound[it->first] = repVar;\r
+ }\r
+ }\r
+ d_qn.push_back( NULL );\r
}else if( d_type==typ_pred || d_type==typ_eq ){\r
//add initial constraint\r
Node nn[2];\r
d_wasSet = false;\r
return false;\r
}\r
- }else if( d_type==typ_var || d_type==typ_eq || d_type==typ_pred || d_type==typ_bool_var ){\r
+ }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 ){\r
bool success = false;\r
bool terminate = false;\r
do {\r
d_binding = true;\r
d_binding_it = d_qni_bound.begin();\r
doReset = true;\r
+ //for tconstraint, add constraint\r
+ if( d_type==typ_tconstraint ){\r
+ std::map< Node, bool >::iterator it = qi->d_tconstraints.find( d_n );\r
+ if( it==qi->d_tconstraints.end() ){\r
+ qi->d_tconstraints[d_n] = d_tgt;\r
+ //store that we added this constraint\r
+ d_qni_bound_cons[0] = d_n;\r
+ }else if( d_tgt!=it->second ){\r
+ success = false;\r
+ terminate = true;\r
+ }\r
+ }\r
}else{\r
Debug("qcf-match-debug") << " - Matching failed" << std::endl;\r
success = false;\r
}\r
d_qni_bound.clear();\r
}\r
+ if( d_type==typ_tconstraint ){\r
+ //remove constraint if applicable\r
+ if( d_qni_bound_cons.find( 0 )!=d_qni_bound_cons.end() ){\r
+ qi->d_tconstraints.erase( d_n );\r
+ d_qni_bound_cons.clear();\r
+ }\r
+ }\r
/*\r
if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){\r
d_matched_basis = true;\r
if( d_performCheck ){\r
++(d_statistics.d_inst_rounds);\r
double clSet = 0;\r
+ int prevEt = 0;\r
if( Trace.isOn("qcf-engine") ){\r
+ prevEt = d_statistics.d_entailment_checks.getData();\r
clSet = double(clock())/double(CLOCKS_PER_SEC);\r
Trace("qcf-engine") << "---Conflict Find Engine Round, effort = " << level << "---" << std::endl;\r
}\r
*/\r
std::vector< Node > terms;\r
qi->getMatch( terms );\r
- if( Debug.isOn("qcf-check-inst") ){\r
- //if( e==effort_conflict ){\r
- Node inst = d_quantEngine->getInstantiation( q, terms );\r
- Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
- Assert( evaluate( inst )!=1 );\r
- Assert( evaluate( inst )==-1 || e>effort_conflict );\r
- //}\r
- }\r
- if( d_quantEngine->addInstantiation( q, terms ) ){\r
- Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
- ++addedLemmas;\r
- if( e==effort_conflict ){\r
- d_quant_order.insert( d_quant_order.begin(), q );\r
- d_conflict.set( true );\r
- ++(d_statistics.d_conflict_inst);\r
- break;\r
- }else if( e==effort_prop_eq ){\r
- ++(d_statistics.d_prop_inst);\r
+ if( !qi->isTConstraintSpurious( this, terms ) ){\r
+ if( Debug.isOn("qcf-check-inst") ){\r
+ //if( e==effort_conflict ){\r
+ Node inst = d_quantEngine->getInstantiation( q, terms );\r
+ Debug("qcf-check-inst") << "Check instantiation " << inst << "..." << std::endl;\r
+ Assert( evaluate( inst )!=1 );\r
+ Assert( evaluate( inst )==-1 || e>effort_conflict );\r
+ //}\r
+ }\r
+ if( d_quantEngine->addInstantiation( q, terms ) ){\r
+ Trace("qcf-check") << " ... Added instantiation" << std::endl;\r
+ Trace("qcf-inst") << "*** Was from effort " << e << " : " << std::endl;\r
+ qi->debugPrintMatch("qcf-inst");\r
+ Trace("qcf-inst") << std::endl;\r
+ ++addedLemmas;\r
+ if( e==effort_conflict ){\r
+ d_quant_order.insert( d_quant_order.begin(), q );\r
+ d_conflict.set( true );\r
+ ++(d_statistics.d_conflict_inst);\r
+ break;\r
+ }else if( e==effort_prop_eq ){\r
+ ++(d_statistics.d_prop_inst);\r
+ }\r
+ }else{\r
+ Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;\r
+ //Assert( false );\r
}\r
- }else{\r
- Trace("qcf-check") << " ... Failed to add instantiation" << std::endl;\r
- //Assert( false );\r
}\r
//clean up assigned\r
qi->revertMatch( assigned );\r
+ d_tempCache.clear();\r
}else{\r
Trace("qcf-check") << " ... Spurious instantiation (cannot assign unassigned variables)" << std::endl;\r
}\r
Trace("qcf-engine") << ", addedLemmas = " << addedLemmas;\r
}\r
Trace("qcf-engine") << std::endl;\r
+ int currEt = d_statistics.d_entailment_checks.getData();\r
+ Trace("qcf-engine") << " Entailment checks = " << ( currEt - prevEt ) << std::endl;\r
}\r
}\r
Trace("qcf-check2") << "QCF : finished check : " << level << std::endl;\r
QuantConflictFind::Statistics::Statistics():\r
d_inst_rounds("QuantConflictFind::Inst_Rounds", 0),\r
d_conflict_inst("QuantConflictFind::Instantiations_Conflict_Find", 0 ),\r
- d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 )\r
+ d_prop_inst("QuantConflictFind::Instantiations_Prop", 0 ),\r
+ d_entailment_checks("QuantConflictFind::Entailment_Checks",0)\r
{\r
StatisticsRegistry::registerStat(&d_inst_rounds);\r
StatisticsRegistry::registerStat(&d_conflict_inst);\r
StatisticsRegistry::registerStat(&d_prop_inst);\r
+ StatisticsRegistry::registerStat(&d_entailment_checks);\r
}\r
\r
QuantConflictFind::Statistics::~Statistics(){\r
StatisticsRegistry::unregisterStat(&d_inst_rounds);\r
StatisticsRegistry::unregisterStat(&d_conflict_inst);\r
StatisticsRegistry::unregisterStat(&d_prop_inst);\r
+ StatisticsRegistry::unregisterStat(&d_entailment_checks);\r
}\r
\r
+TNode QuantConflictFind::getZero( Kind k ) {\r
+ std::map< Kind, Node >::iterator it = d_zero.find( k );\r
+ if( it==d_zero.end() ){\r
+ Node nn;\r
+ if( k==PLUS ){\r
+ nn = NodeManager::currentNM()->mkConst( Rational(0) );\r
+ }\r
+ d_zero[k] = nn;\r
+ return nn;\r
+ }else{\r
+ return it->second;\r
+ }\r
+}\r
+\r
+\r
}\r
typ_var,\r
typ_ite_var,\r
typ_bool_var,\r
+ typ_tconstraint,\r
+ typ_tsym,\r
};\r
void debugPrintType( const char * c, short typ, bool isTrace = false );\r
public:\r
MatchGen() : d_type( typ_invalid ){}\r
- MatchGen( QuantInfo * qi, Node n, bool isVar = false, bool beneathQuant = false );\r
+ MatchGen( QuantInfo * qi, Node n, bool isVar = false );\r
bool d_tgt;\r
bool d_tgt_orig;\r
bool d_wasSet;\r
~QuantInfo() { delete d_mg; }\r
std::vector< TNode > d_vars;\r
std::map< TNode, int > d_var_num;\r
- std::map< TNode, bool > d_nbeneathQuant;\r
+ std::vector< int > d_tsym_vars;\r
+ std::map< TNode, bool > d_inMatchConstraint;\r
std::map< int, std::vector< Node > > d_var_constraint[2];\r
int getVarNum( TNode v ) { return d_var_num.find( v )!=d_var_num.end() ? d_var_num[v] : -1; }\r
bool isVar( TNode v ) { return d_var_num.find( v )!=d_var_num.end(); }\r
std::vector< TNode > d_match;\r
std::vector< TNode > d_match_term;\r
std::map< int, std::map< TNode, int > > d_curr_var_deq;\r
+ std::map< Node, bool > d_tconstraints;\r
int getCurrentRepVar( int v );\r
TNode getCurrentValue( TNode n );\r
TNode getCurrentExpValue( TNode n );\r
int addConstraint( QuantConflictFind * p, int v, TNode n, int vn, bool polarity, bool doRemove );\r
bool setMatch( QuantConflictFind * p, int v, TNode n );\r
bool isMatchSpurious( QuantConflictFind * p );\r
+ bool isTConstraintSpurious( QuantConflictFind * p, std::vector< Node >& terms );\r
+ bool entailmentTest( QuantConflictFind * p, Node lit, bool chEnt = true );\r
bool completeMatch( QuantConflictFind * p, std::vector< int >& assigned, bool doContinue = false );\r
void revertMatch( std::vector< int >& assigned );\r
void debugPrintMatch( const char * c );\r
context::CDO< bool > d_conflict;\r
bool d_performCheck;\r
std::vector< Node > d_quant_order;\r
+ std::map< Kind, Node > d_zero;\r
+ //for storing nodes created during t-constraint solving (prevents memory leaks)\r
+ std::vector< Node > d_tempCache;\r
private:\r
std::map< Node, Node > d_op_node;\r
int d_fid_count;\r
public: //for ground terms\r
Node d_true;\r
Node d_false;\r
+ TNode getZero( Kind k );\r
private:\r
Node evaluateTerm( Node n );\r
int evaluate( Node n, bool pref = false, bool hasPref = false );\r
IntStat d_inst_rounds;\r
IntStat d_conflict_inst;\r
IntStat d_prop_inst;\r
+ IntStat d_entailment_checks;\r
Statistics();\r
~Statistics();\r
};\r
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 */
return PP_ASSERT_STATUS_UNSOLVED;
}
+std::pair<bool, Node> 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 */
class TheoryModel;
class SubstitutionMap;
+class EntailmentCheckParameters;
+class EntailmentCheckSideEffects;
+
namespace rrinst {
class CandidateGenerator;
}/* CVC4::theory::rrinst namespace */
* in a queriable form. As this is
*/
std::hash_set<TNode, TNodeHashFunction> 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 <b,E> s.t. if b is true, then a formula E such that
+ * E |= lit in the theory.
+ */
+ virtual std::pair<bool, Node> entailmentCheck(TNode lit, const EntailmentCheckParameters* params = NULL, EntailmentCheckSideEffects* out = NULL);
+
};/* class Theory */
std::ostream& operator<<(std::ostream& os, theory::Theory::Effort level);
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 */
}
}
}
+
+std::pair<bool, Node> 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);
+}
namespace eq {
class EqualityEngine;
}
+
+ class EntailmentCheckParameters;
+ class EntailmentCheckSideEffects;
}/* CVC4::theory namespace */
class DecisionEngine;
class RemoveITE;
*/
Node getModelValue(TNode var);
+ /**
+ * Forwards an entailmentCheck according to the given theoryOfMode mode.
+ * See theory.h for documentation on entailmentCheck().
+ */
+ std::pair<bool, Node> entailmentCheck(theory::TheoryOfMode mode, TNode lit, const theory::EntailmentCheckParameters* params = NULL, theory::EntailmentCheckSideEffects* out = NULL);
+
private:
/** Default visitor for pre-registration */
throw std::invalid_argument(ss.str());
}
}
+
+bool Integer::fitsSignedInt() const {
+ // TODO improve performance
+ return d_value <= std::numeric_limits<signed int>::max() &&
+ d_value >= std::numeric_limits<signed int>::min();
+}
+
+bool Integer::fitsUnsignedInt() const {
+ // TODO improve performance
+ return sgn() >= 0 && d_value <= std::numeric_limits<unsigned int>::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);
+}
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<long>::max(), this,
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<int>::max(), this,
+ "Overflow detected in Integer::getSignedInt()");
+ CheckArgument(d_value >= std::numeric_limits<int>::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<unsigned int>::max(), this,
+ "Overflow detected in Integer::getUnsignedInt()");
+ CheckArgument(d_value >= std::numeric_limits<unsigned int>::min(), this,
+ "Overflow detected in Integer::getUnsignedInt()");
+ CheckArgument(fitsSignedInt(), this, "Overflow detected in Integer::getUnsignedInt()");
+ return (unsigned int) d_value.get_ui();
+}
#include <string>
#include <iostream>
+#include <limits>
#include "util/gmp_util.h"
#include "util/exception.h"
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();
if(m.nothing()){
out << "Nothing";
}else{
+ out << "Just ";
out << m.constValue();
}
out << "}";
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 \
# 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
+; COMMAND-LINE: --full-saturate-quant
+; EXPECT: unsat
(set-logic AUFLIA)
(set-info :smt-lib-version 2.0)
(set-info :category "crafted")
(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)
-% EXPECT: unknown
-% EXPECT: (:reason-unknown incomplete)
+% EXPECT: unsat
--- /dev/null
+; 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)
--- /dev/null
+; 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)
projects / cvc5.git / commitdiff