theory/shared_terms_database.cpp \
theory/term_registration_visitor.h \
theory/term_registration_visitor.cpp \
- theory/ite_simplifier.h \
- theory/ite_simplifier.cpp \
+ theory/ite_utilities.h \
+ theory/ite_utilities.cpp \
theory/unconstrained_simplifier.h \
theory/unconstrained_simplifier.cpp \
theory/quantifiers_engine.h \
namespace expr {
namespace attr {
+AttributeManager::AttributeManager(context::Context* ctxt) :
+ d_cdbools(ctxt),
+ d_cdints(ctxt),
+ d_cdtnodes(ctxt),
+ d_cdnodes(ctxt),
+ d_cdstrings(ctxt),
+ d_cdptrs(ctxt),
+ d_inGarbageCollection(false)
+{}
+
+bool AttributeManager::inGarbageCollection() const {
+ return d_inGarbageCollection;
+}
void AttributeManager::debugHook(int debugFlag) {
/* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
}
void AttributeManager::deleteAllAttributes(NodeValue* nv) {
+ Assert(!inGarbageCollection());
d_bools.erase(nv);
deleteFromTable(d_ints, nv);
deleteFromTable(d_tnodes, nv);
template <class T, bool context_dep>
friend struct getTable;
+ bool d_inGarbageCollection;
+
+ void clearDeleteAllAttributesBuffer();
+
public:
/** Construct an attribute manager. */
- AttributeManager(context::Context* ctxt) :
- d_cdbools(ctxt),
- d_cdints(ctxt),
- d_cdtnodes(ctxt),
- d_cdnodes(ctxt),
- d_cdstrings(ctxt),
- d_cdptrs(ctxt) {
- }
+ AttributeManager(context::Context* ctxt);
/**
* Get a particular attribute on a particular node.
*/
void deleteAllAttributes();
+ /**
+ * Returns true if a table is currently being deleted.
+ */
+ bool inGarbageCollection() const ;
/**
* Determines the AttrTableId of an attribute.
/**
* Search for the NodeValue in all attribute tables and remove it,
* calling the cleanup function if one is defined.
+ *
+ * This cannot use nv as anything other than a pointer!
*/
template <class T>
inline void AttributeManager::deleteFromTable(AttrHash<T>& table,
*/
template <class T>
inline void AttributeManager::deleteAllFromTable(AttrHash<T>& table) {
+ Assert(!d_inGarbageCollection);
+ d_inGarbageCollection = true;
+
bool anyRequireClearing = false;
typedef AttributeTraits<T, false> traits_t;
typedef AttrHash<T> hash_t;
}
}
table.clear();
+ d_inGarbageCollection = false;
+ Assert(!d_inGarbageCollection);
}
template <class AttrKind>
template <class T>
void AttributeManager::deleteAttributesFromTable(AttrHash<T>& table, const std::vector<uint64_t>& ids){
+ d_inGarbageCollection = true;
typedef AttributeTraits<T, false> traits_t;
typedef AttrHash<T> hash_t;
++it;
}
}
+ d_inGarbageCollection = false;
static const size_t ReconstructShrinkRatio = 8;
if(initialSize/ReconstructShrinkRatio > table.size()){
reconstructTable(table);
template <class T>
void AttributeManager::reconstructTable(AttrHash<T>& table){
+ d_inGarbageCollection = true;
typedef AttrHash<T> hash_t;
hash_t cpy;
cpy.insert(table.begin(), table.end());
cpy.swap(table);
+ d_inGarbageCollection = false;
}
typerules=
construles=
+neverconstrules=
seen_theory=false
seen_theory_builtin=false
case kind::$1:
#line $lineno \"$kf\"
return $2::computeIsConst(nodeManager, n);
+"
+ neverconstrules="${neverconstrules}
+#line $lineno \"$kf\"
+ case kind::$1:
+#line $lineno \"$kf\"
+ return false;
"
}
typechecker_includes \
typerules \
construles \
+ neverconstrules \
; do
eval text="\${text//\\\$\\{$var\\}/\${$var}}"
done
Debug("isConst") << "Node::isConst() returning false, it's a VARIABLE" << std::endl;
return false;
default:
+ if(expr::TypeChecker::neverIsConst(NodeManager::currentNM(), *this)){
+ Debug("isConst") << "Node::isConst() returning false, the kind is never const" << std::endl;
+ return false;
+ }
if(getAttribute(IsConstComputedAttr())) {
bool bval = getAttribute(IsConstAttr());
Debug("isConst") << "Node::isConst() returning cached value " << (bval ? "true" : "false") << " for: " << *this << std::endl;
d_operators[i] = Node::null();
}
+ Assert(!d_attrManager->inGarbageCollection() );
while(!d_zombies.empty()) {
reclaimZombies();
}
void NodeManager::reclaimZombies() {
// FIXME multithreading
+ Assert(!d_attrManager->inGarbageCollection());
Debug("gc") << "reclaiming " << d_zombies.size() << " zombie(s)!\n";
return dtt;
}
+void NodeManager::reclaimAllZombies(){
+ reclaimZombiesUntil(0u);
+}
+
+/** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+void NodeManager::reclaimZombiesUntil(uint32_t k){
+ if(safeToReclaimZombies()){
+ while(poolSize() >= k && !d_zombies.empty()){
+ reclaimZombies();
+ }
+ }
+}
+
+size_t NodeManager::poolSize() const{
+ return d_nodeValuePool.size();
+}
+
TypeNode NodeManager::mkSort(uint32_t flags) {
NodeBuilder<1> nb(this, kind::SORT_TYPE);
Node sortTag = NodeBuilder<0>(this, kind::SORT_TAG);
return n;
}
+bool NodeManager::safeToReclaimZombies() const{
+ // FIXME multithreading
+ return !d_inReclaimZombies && !d_attrManager->inGarbageCollection();
+}
+
void NodeManager::deleteAttributes(const std::vector<const expr::attr::AttributeUniqueId*>& ids){
d_attrManager->deleteAttributes(ids);
}
}
d_zombies.insert(nv);// FIXME multithreading
- if(!d_inReclaimZombies) {// FIXME multithreading
- // for now, collect eagerly. can add heuristic here later..
+ if(safeToReclaimZombies()) {
if(d_zombies.size() > 5000) {
reclaimZombies();
}
*/
void reclaimZombies();
+ /**
+ * It is safe to collect zombies.
+ */
+ bool safeToReclaimZombies() const;
+
/**
* This template gives a mechanism to stack-allocate a NodeValue
* with enough space for N children (where N is a compile-time
*/
static inline TypeNode fromType(Type t);
+ /** Reclaim zombies while there are more than k nodes in the pool (if possible).*/
+ void reclaimZombiesUntil(uint32_t k);
+
+ /** Reclaims all zombies (if possible).*/
+ void reclaimAllZombies();
+
+ /** Size of the node pool. */
+ size_t poolSize() const;
+
/** Deletes a list of attributes from the NM's AttributeManager.*/
void deleteAttributes(const std::vector< const expr::attr::AttributeUniqueId* >& ids);
* any published code!
*/
void debugHook(int debugFlag);
-
};/* class NodeManager */
/**
option typeChecking /--no-type-checking bool :default DO_SEMANTIC_CHECKS_BY_DEFAULT :link /--lazy-type-checking
never type check expressions
+option biasedITERemoval --biased-ites bool :default false
+ try the new remove ite pass that is biased against term ites appearing
+
endmodule
static bool computeIsConst(NodeManager* nodeManager, TNode n)
throw (AssertionException);
+ static bool neverIsConst(NodeManager* nodeManager, TNode n)
+ throw (AssertionException);
+
};/* class TypeChecker */
}/* CVC4::expr namespace */
}/* TypeChecker::computeIsConst */
+bool TypeChecker::neverIsConst(NodeManager* nodeManager, TNode n)
+ throw (AssertionException) {
+
+ Assert(n.getMetaKind() == kind::metakind::OPERATOR || n.getMetaKind() == kind::metakind::PARAMETERIZED);
+
+ switch(n.getKind()) {
+${neverconstrules}
+
+#line 90 "${template}"
+
+ default:;
+ }
+
+ return true;
+
+}/* TypeChecker::neverIsConst */
+
}/* CVC4::expr namespace */
}/* CVC4 namespace */
option doITESimp --ite-simp bool :read-write
turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)
+option doITESimpOnRepeat --on-repeat-ite-simp bool :read-write :default false
+ do the ite simplification pass again if repeating simplification
+
+option simplifyWithCareEnabled --simp-with-care bool :default false :read-write
+ enables simplifyWithCare in ite simplificiation
+
+option compressItes --simp-ite-compress bool :default false :read-write
+ enables compressing ites after ite simplification
+
option unconstrainedSimp --unconstrained-simp bool :default false :read-write
turn on unconstrained simplification (see Bruttomesso/Brummayer PhD thesis)
option repeatSimp --repeat-simp bool :read-write
make multiple passes with nonclausal simplifier
+option zombieHuntThreshold --simp-ite-hunt-zombies uint32_t :default 524288
+ post ite compression enables zombie removal while the number of nodes is above this threshold
+
option sortInference --sort-inference bool :read-write :default false
calculate sort inference of input problem, convert the input based on monotonic sorts
common-option incrementalSolving incremental -i --incremental bool
enable incremental solving
+
option abstractValues abstract-values --abstract-values bool :default false
in models, output arrays (and in future, maybe others) using abstract values, as required by the SMT-LIB standard
option modelUninterpDtEnum --model-u-dt-enum bool :default false
#include "util/node_visitor.h"
#include "util/configuration.h"
#include "util/exception.h"
+#include "util/nary_builder.h"
#include "smt/command_list.h"
#include "smt/boolean_terms.h"
#include "smt/options.h"
namespace smt {
+/** Useful for counting the number of recursive calls. */
+class ScopeCounter {
+private:
+ unsigned& d_depth;
+public:
+ ScopeCounter(unsigned& d) : d_depth(d) {
+ ++d_depth;
+ }
+ ~ScopeCounter(){
+ --d_depth;
+ }
+};
+
/**
* Representation of a defined function. We keep these around in
* SmtEngine to permit expanding definitions late (and lazily), to
/** time spent in processAssertions() */
TimerStat d_processAssertionsTime;
+ /** Has something simplified to false? */
+ IntStat d_simplifiedToFalse;
+
SmtEngineStatistics() :
d_definitionExpansionTime("smt::SmtEngine::definitionExpansionTime"),
d_rewriteBooleanTermsTime("smt::SmtEngine::rewriteBooleanTermsTime"),
d_checkModelTime("smt::SmtEngine::checkModelTime"),
d_solveTime("smt::SmtEngine::solveTime"),
d_pushPopTime("smt::SmtEngine::pushPopTime"),
- d_processAssertionsTime("smt::SmtEngine::processAssertionsTime") {
+ d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
+ d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
+
+ {
StatisticsRegistry::registerStat(&d_definitionExpansionTime);
StatisticsRegistry::registerStat(&d_rewriteBooleanTermsTime);
StatisticsRegistry::registerStat(&d_solveTime);
StatisticsRegistry::registerStat(&d_pushPopTime);
StatisticsRegistry::registerStat(&d_processAssertionsTime);
+ StatisticsRegistry::registerStat(&d_simplifiedToFalse);
}
~SmtEngineStatistics() {
StatisticsRegistry::unregisterStat(&d_solveTime);
StatisticsRegistry::unregisterStat(&d_pushPopTime);
StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
+ StatisticsRegistry::unregisterStat(&d_simplifiedToFalse);
}
};/* struct SmtEngineStatistics */
*/
Node d_modZero;
+ /** Number of calls of simplify assertions active.
+ */
+ unsigned d_simplifyAssertionsDepth;
+
public:
/**
* Map from skolem variables to index in d_assertionsToCheck containing
void bvToBool();
// Simplify ITE structure
- void simpITE();
+ bool simpITE();
// Simplify based on unconstrained values
void unconstrainedSimp();
+ // Ensures the assertions asserted after before now
+ // effectively come before d_realAssertionsEnd
+ void compressBeforeRealAssertions(size_t before);
+
/**
* Any variable in an assertion that is declared as a subtype type
* (predicate subtype or integer subrange type) must be constrained
d_divByZero(),
d_intDivByZero(),
d_modZero(),
+ d_simplifyAssertionsDepth(0),
d_iteSkolemMap(),
d_iteRemover(smt.d_userContext),
d_topLevelSubstitutions(smt.d_userContext)
}
// Turn on ite simplification for QF_LIA and QF_AUFBV
if(! options::doITESimp.wasSetByUser()) {
- bool iteSimp = !d_logic.isQuantified() &&
- ((d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() && !d_logic.areRealsUsed()) ||
- (d_logic.isTheoryEnabled(THEORY_ARRAY) && d_logic.isTheoryEnabled(THEORY_UF) && d_logic.isTheoryEnabled(THEORY_BV)));
+ bool qf_aufbv = !d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_BV);
+ bool qf_lia = !d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_ARITH) &&
+ d_logic.isLinear() &&
+ !d_logic.isDifferenceLogic() &&
+ !d_logic.areRealsUsed();
+
+ bool iteSimp = (qf_aufbv || qf_lia);
Trace("smt") << "setting ite simplification to " << iteSimp << endl;
options::doITESimp.set(iteSimp);
}
+ if(! options::compressItes.wasSetByUser() ){
+ bool qf_lia = !d_logic.isQuantified() &&
+ d_logic.isPure(THEORY_ARITH) &&
+ d_logic.isLinear() &&
+ !d_logic.isDifferenceLogic() &&
+ !d_logic.areRealsUsed();
+
+ bool compressIte = qf_lia;
+ Trace("smt") << "setting ite compression to " << compressIte << endl;
+ options::compressItes.set(compressIte);
+ }
+ if(! options::simplifyWithCareEnabled.wasSetByUser() ){
+ bool qf_aufbv = !d_logic.isQuantified() &&
+ d_logic.isTheoryEnabled(THEORY_ARRAY) &&
+ d_logic.isTheoryEnabled(THEORY_UF) &&
+ d_logic.isTheoryEnabled(THEORY_BV);
+
+ bool withCare = qf_aufbv;
+ Trace("smt") << "setting ite simplify with care to " << withCare << endl;
+ options::simplifyWithCareEnabled.set(withCare);
+ }
// Turn off array eager index splitting for QF_AUFLIA
if(! options::arraysEagerIndexSplitting.wasSetByUser()) {
if (not d_logic.isQuantified() &&
}
}
-void SmtEnginePrivate::simpITE() {
+bool SmtEnginePrivate::simpITE() {
TimerStat::CodeTimer simpITETimer(d_smt.d_stats->d_simpITETime);
Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
+ unsigned numAssertionOnEntry = d_assertionsToCheck.size();
for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
- d_assertionsToCheck[i] = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+ Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
+ d_assertionsToCheck[i] = result;
+ if(result.isConst() && !result.getConst<bool>()){
+ return false;
+ }
}
+ bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck);
+ if(numAssertionOnEntry < d_assertionsToCheck.size()){
+ compressBeforeRealAssertions(numAssertionOnEntry);
+ }
+ return result;
}
+void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
+ size_t curr = d_assertionsToCheck.size();
+ if(before >= curr ||
+ d_realAssertionsEnd <= 0 ||
+ d_realAssertionsEnd >= curr){
+ return;
+ }
+
+ // assertions
+ // original: [0 ... d_realAssertionsEnd)
+ // can be modified
+ // ites skolems [d_realAssertionsEnd, before)
+ // cannot be moved
+ // added [before, curr)
+ // can be modified
+ Assert(0 < d_realAssertionsEnd);
+ Assert(d_realAssertionsEnd <= before);
+ Assert(before < curr);
+
+ std::vector<Node> intoConjunction;
+ for(size_t i = before; i<curr; ++i){
+ intoConjunction.push_back(d_assertionsToCheck[i]);
+ }
+ d_assertionsToCheck.resize(before);
+ size_t lastBeforeItes = d_realAssertionsEnd - 1;
+ intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]);
+ Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
+ d_assertionsToCheck[lastBeforeItes] = newLast;
+ Assert(d_assertionsToCheck.size() == before);
+}
void SmtEnginePrivate::unconstrainedSimp() {
TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
d_realAssertionsEnd = d_assertionsToCheck.size();
}
+
// returns false if simplification led to "false"
bool SmtEnginePrivate::simplifyAssertions()
throw(TypeCheckingException, LogicException) {
Assert(d_smt.d_pendingPops == 0);
try {
+ ScopeCounter depth(d_simplifyAssertionsDepth);
Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl;
// ITE simplification
- if(options::doITESimp()) {
+ if(options::doITESimp() &&
+ (d_simplifyAssertionsDepth <= 1 || options::doITESimpOnRepeat())) {
Chat() << "...doing ITE simplification..." << endl;
- simpITE();
+ bool noConflict = simpITE();
+ if(!noConflict){
+ Chat() << "...ITE simplification found unsat..." << endl;
+ return false;
+ }
}
dumpAssertions("post-itesimp", d_assertionsToCheck);
dumpAssertions("pre-simplify", d_assertionsToPreprocess);
Chat() << "simplifying assertions..." << endl;
bool noConflict = simplifyAssertions();
+ if(!noConflict){
+ ++(d_smt.d_stats->d_simplifiedToFalse);
+ }
dumpAssertions("post-simplify", d_assertionsToCheck);
dumpAssertions("pre-static-learning", d_assertionsToCheck);
if(options::repeatSimp()) {
d_assertionsToCheck.swap(d_assertionsToPreprocess);
Chat() << "re-simplifying assertions..." << endl;
+ ScopeCounter depth(d_simplifyAssertionsDepth);
noConflict &= simplifyAssertions();
if (noConflict) {
// Need to fix up assertion list to maintain invariants:
namespace theory {
namespace booleans {
+RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) {
+ return preRewrite(node);
+}
+
/**
* flattenNode looks for children of same kind, and if found merges
* them into the parent.
}
}
+// Equality parity returns
+// * 0 if no relation between a and b is found
+// * 1 if a == b
+// * 2 if a == not(b)
+// * 3 or b == not(a)
+inline int equalityParity(TNode a, TNode b){
+ if(a == b){
+ return 1;
+ }else if(a.getKind() == kind::NOT && a[0] == b){
+ return 2;
+ }else if(b.getKind() == kind::NOT && b[0] == a){
+ return 3;
+ }else{
+ return 0;
+ }
+}
+
+inline Node makeNegation(TNode n){
+ bool even = false;
+ while(n.getKind() == kind::NOT){
+ n = n[0];
+ even = !even;
+ }
+ if(even){
+ return n;
+ } else {
+ if(n.isConst()){
+ return NodeManager::currentNM()->mkConst(!n.getConst<bool>());
+ }else{
+ return n.notNode();
+ }
+ }
+}
+
RewriteResponse TheoryBoolRewriter::preRewrite(TNode n) {
NodeManager* nodeManager = NodeManager::currentNM();
Node tt = nodeManager->mkConst(true);
if (n[0] == ff || n[1] == tt) return RewriteResponse(REWRITE_DONE, tt);
if (n[0] == tt && n[0] == ff) return RewriteResponse(REWRITE_DONE, ff);
if (n[0] == tt) return RewriteResponse(REWRITE_AGAIN, n[1]);
- if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ if (n[1] == ff) return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
break;
}
case kind::IFF:
return RewriteResponse(REWRITE_AGAIN, n[0]);
} else if(n[0] == ff) {
// IFF false x
- return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+ return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
} else if(n[1] == ff) {
// IFF x false
- return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
} else if(n[0] == n[1]) {
// IFF x x
return RewriteResponse(REWRITE_DONE, tt);
if(kappa.knownLessThanOrEqual(two)){
return RewriteResponse(REWRITE_DONE, ff);
}else{
- Node neitherEquality = (n[0].notNode()).andNode(n[1].notNode());
+ Node neitherEquality = (makeNegation(n[0])).andNode(makeNegation(n[1]));
return RewriteResponse(REWRITE_AGAIN, neitherEquality);
}
}
// rewrite simple cases of XOR
if(n[0] == tt) {
// XOR true x
- return RewriteResponse(REWRITE_AGAIN, n[1].notNode());
+ return RewriteResponse(REWRITE_AGAIN, makeNegation(n[1]));
} else if(n[1] == tt) {
// XCR x true
- return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
} else if(n[0] == ff) {
// XOR false x
return RewriteResponse(REWRITE_AGAIN, n[1]);
if (n[0].isConst()) {
if (n[0] == tt) {
// ITE true x y
+
+ Debug("bool-ite") << "n[0] ==tt " << n << ": " << n[1] << std::endl;
return RewriteResponse(REWRITE_AGAIN, n[1]);
} else {
Assert(n[0] == ff);
// ITE false x y
+ Debug("bool-ite") << "n[0] ==ff " << n << ": " << n[1] << std::endl;
return RewriteResponse(REWRITE_AGAIN, n[2]);
}
} else if (n[1].isConst()) {
if (n[1] == tt && n[2] == ff) {
+ Debug("bool-ite") << "n[1] ==tt && n[2] == ff " << n << ": " << n[0] << std::endl;
return RewriteResponse(REWRITE_AGAIN, n[0]);
}
else if (n[1] == ff && n[2] == tt) {
- return RewriteResponse(REWRITE_AGAIN, n[0].notNode());
+ Debug("bool-ite") << "n[1] ==ff && n[2] == tt " << n << ": " << n[0].notNode() << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, makeNegation(n[0]));
}
+ // else if(n[1] == ff){
+ // Node resp = (n[0].notNode()).andNode(n[2]);
+ // return RewriteResponse(REWRITE_AGAIN, resp);
+ // }
}
- if (n[1] == n[2]) {
- return RewriteResponse(REWRITE_AGAIN, n[1]);
+ // else if (n[2].isConst()) {
+ // if(n[2] == ff){
+ // Node resp = (n[0]).andNode(n[1]);
+ // return RewriteResponse(REWRITE_AGAIN, resp);
+ // }
+ // }
+
+ int parityTmp;
+ if ((parityTmp = equalityParity(n[1], n[2])) != 0) {
+ Node resp = (parityTmp == 1) ? (Node)n[1] : n[0].iffNode(n[1]);
+ Debug("bool-ite") << "equalityParity n[1], n[2] " << parityTmp
+ << " " << n << ": " << resp << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, resp);
// Curiously, this rewrite affects several benchmarks dramatically, including copy_array and some simple_startup - disable for now
// } else if (n[0].getKind() == kind::NOT) {
// return RewriteResponse(REWRITE_AGAIN, n[0][0].iteNode(n[2], n[1]));
- } else if (n[0] == n[1]) {
- return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(tt, n[2]));
- } else if (n[0] == n[2]) {
- return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], ff));
- } else if (n[1].getKind() == kind::NOT && n[1][0] == n[0]) {
- return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(ff, n[2]));
- } else if (n[2].getKind() == kind::NOT && n[2][0] == n[0]) {
- return RewriteResponse(REWRITE_AGAIN, n[0].iteNode(n[1], tt));
+ } else if(!n[1].isConst() && (parityTmp = equalityParity(n[0], n[1])) != 0){
+ // (parityTmp == 1) if n[0] == n[1]
+ // otherwise, n[0] == not(n[1]) or not(n[0]) == n[1]
+
+ // if n[1] is constant this can loop, this is possible in prewrite
+ Node resp = n[0].iteNode( (parityTmp == 1) ? tt : ff, n[2]);
+ Debug("bool-ite") << "equalityParity n[0], n[1] " << parityTmp
+ << " " << n << ": " << resp << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, resp);
+ } else if(!n[2].isConst() && (parityTmp = equalityParity(n[0], n[2])) != 0){
+ // (parityTmp == 1) if n[0] == n[2]
+ // otherwise, n[0] == not(n[2]) or not(n[0]) == n[2]
+ Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? ff : tt);
+ Debug("bool-ite") << "equalityParity n[0], n[2] " << parityTmp
+ << " " << n << ": " << resp << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, resp);
+ } else if(n[1].getKind() == kind::ITE &&
+ (parityTmp = equalityParity(n[0], n[1][0])) != 0){
+ // (parityTmp == 1) then n : (ite c (ite c x y) z)
+ // (parityTmp > 1) then n : (ite c (ite (not c) x y) z) or
+ // n: (ite (not c) (ite c x y) z)
+ Node resp = n[0].iteNode((parityTmp == 1) ? n[1][1] : n[1][2], n[2]);
+ Debug("bool-ite") << "equalityParity n[0], n[1][0] " << parityTmp
+ << " " << n << ": " << resp << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, resp);
+ } else if(n[2].getKind() == kind::ITE &&
+ (parityTmp = equalityParity(n[0], n[2][0])) != 0){
+ // (parityTmp == 1) then n : (ite c x (ite c y z))
+ // (parityTmp > 1) then n : (ite c x (ite (not c) y z)) or
+ // n: (ite (not c) x (ite c y z))
+ Node resp = n[0].iteNode(n[1], (parityTmp == 1) ? n[2][2] : n[2][1]);
+ Debug("bool-ite") << "equalityParity n[0], n[2][0] " << parityTmp
+ << " " << n << ": " << resp << std::endl;
+ return RewriteResponse(REWRITE_AGAIN, resp);
}
break;
}
public:
static RewriteResponse preRewrite(TNode node);
- static RewriteResponse postRewrite(TNode node) {
- return preRewrite(node);
- }
+ static RewriteResponse postRewrite(TNode node);
static void init() {}
static void shutdown() {}
+++ /dev/null
-/********************* */
-/*! \file ite_simplifier.cpp
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Simplifications for ITE expressions
- **
- ** This module implements preprocessing phases designed to simplify ITE
- ** expressions. Based on:
- ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
- ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
- **/
-
-
-#include "theory/ite_simplifier.h"
-
-
-using namespace std;
-using namespace CVC4;
-using namespace theory;
-
-
-bool ITESimplifier::containsTermITE(TNode e)
-{
- if (e.getKind() == kind::ITE && !e.getType().isBoolean()) {
- return true;
- }
-
- hash_map<Node, bool, NodeHashFunction>::iterator it;
- it = d_containsTermITECache.find(e);
- if (it != d_containsTermITECache.end()) {
- return (*it).second;
- }
-
- size_t k = 0, sz = e.getNumChildren();
- for (; k < sz; ++k) {
- if (containsTermITE(e[k])) {
- d_containsTermITECache[e] = true;
- return true;
- }
- }
-
- d_containsTermITECache[e] = false;
- return false;
-}
-
-
-bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
-{
- Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) ||
- Theory::theoryOf(e) != THEORY_BOOL);
- if (e.isConst()) {
- return true;
- }
-
- hash_map<Node, bool, NodeHashFunction>::iterator it;
- it = d_leavesConstCache.find(e);
- if (it != d_leavesConstCache.end()) {
- return (*it).second;
- }
-
- if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) {
- d_leavesConstCache[e] = false;
- return false;
- }
-
- Assert(e.getNumChildren() > 0);
- size_t k = 0, sz = e.getNumChildren();
-
- if (e.getKind() == kind::ITE) {
- k = 1;
- }
-
- for (; k < sz; ++k) {
- if (!leavesAreConst(e[k], tid)) {
- d_leavesConstCache[e] = false;
- return false;
- }
- }
- d_leavesConstCache[e] = true;
- return true;
-}
-
-
-Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar)
-{
- NodePairMap::iterator it;
- it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode));
- if (it != d_simpConstCache.end()) {
- return (*it).second;
- }
-
- if (iteNode.getKind() == kind::ITE) {
- NodeBuilder<> builder(kind::ITE);
- builder << iteNode[0];
- unsigned i = 1;
- for (; i < iteNode.getNumChildren(); ++ i) {
- Node n = simpConstants(simpContext, iteNode[i], simpVar);
- if (n.isNull()) {
- return n;
- }
- builder << n;
- }
- // Mark the substitution and continue
- Node result = builder;
- result = Rewriter::rewrite(result);
- d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
- return result;
- }
-
- if (!containsTermITE(iteNode)) {
- Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
- d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
- return n;
- }
-
- Node iteNode2;
- Node simpVar2;
- d_simpContextCache.clear();
- Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
- if (!simpContext2.isNull()) {
- Assert(!iteNode2.isNull());
- simpContext2 = simpContext.substitute(simpVar, simpContext2);
- Node n = simpConstants(simpContext2, iteNode2, simpVar2);
- if (n.isNull()) {
- return n;
- }
- d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
- return n;
- }
- return Node();
-}
-
-
-Node ITESimplifier::getSimpVar(TypeNode t)
-{
- std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
- it = d_simpVars.find(t);
- if (it != d_simpVars.end()) {
- return (*it).second;
- }
- else {
- Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification");
- d_simpVars[t] = var;
- return var;
- }
-}
-
-
-Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
-{
- NodeMap::iterator it;
- it = d_simpContextCache.find(c);
- if (it != d_simpContextCache.end()) {
- return (*it).second;
- }
-
- if (!containsTermITE(c)) {
- d_simpContextCache[c] = c;
- return c;
- }
-
- if (c.getKind() == kind::ITE && !c.getType().isBoolean()) {
- // Currently only support one ite node in a simp context
- // Return Null if more than one is found
- if (!iteNode.isNull()) {
- return Node();
- }
- simpVar = getSimpVar(c.getType());
- if (simpVar.isNull()) {
- return Node();
- }
- d_simpContextCache[c] = simpVar;
- iteNode = c;
- return simpVar;
- }
-
- NodeBuilder<> builder(c.getKind());
- if (c.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << c.getOperator();
- }
- unsigned i = 0;
- for (; i < c.getNumChildren(); ++ i) {
- Node newChild = createSimpContext(c[i], iteNode, simpVar);
- if (newChild.isNull()) {
- return newChild;
- }
- builder << newChild;
- }
- // Mark the substitution and continue
- Node result = builder;
- d_simpContextCache[c] = result;
- return result;
-}
-
-
-Node ITESimplifier::simpITEAtom(TNode atom)
-{
- if (leavesAreConst(atom)) {
- Node iteNode;
- Node simpVar;
- d_simpContextCache.clear();
- Node simpContext = createSimpContext(atom, iteNode, simpVar);
- if (!simpContext.isNull()) {
- if (iteNode.isNull()) {
- Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
- return Rewriter::rewrite(simpContext);
- }
- Node n = simpConstants(simpContext, iteNode, simpVar);
- if (!n.isNull()) {
- return n;
- }
- }
- }
- return atom;
-}
-
-
-struct preprocess_stack_element {
- TNode node;
- bool children_added;
- preprocess_stack_element(TNode node)
- : node(node), children_added(false) {}
-};/* struct preprocess_stack_element */
-
-
-Node ITESimplifier::simpITE(TNode assertion)
-{
- // Do a topological sort of the subexpressions and substitute them
- vector<preprocess_stack_element> toVisit;
- toVisit.push_back(assertion);
-
- while (!toVisit.empty())
- {
- // The current node we are processing
- preprocess_stack_element& stackHead = toVisit.back();
- TNode current = stackHead.node;
-
- // If node has no ITE's or already in the cache we're done, pop from the stack
- if (current.getNumChildren() == 0 ||
- (Theory::theoryOf(current) != THEORY_BOOL && !containsTermITE(current))) {
- d_simpITECache[current] = current;
- toVisit.pop_back();
- continue;
- }
-
- NodeMap::iterator find = d_simpITECache.find(current);
- if (find != d_simpITECache.end()) {
- toVisit.pop_back();
- continue;
- }
-
- // Not yet substituted, so process
- if (stackHead.children_added) {
- // Children have been processed, so substitute
- NodeBuilder<> builder(current.getKind());
- if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << current.getOperator();
- }
- for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
- Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
- builder << d_simpITECache[current[i]];
- }
- // Mark the substitution and continue
- Node result = builder;
-
- // If this is an atom, we process it
- if (Theory::theoryOf(result) != THEORY_BOOL &&
- result.getType().isBoolean()) {
- result = simpITEAtom(result);
- }
-
- result = Rewriter::rewrite(result);
- d_simpITECache[current] = result;
- toVisit.pop_back();
- } else {
- // Mark that we have added the children if any
- if (current.getNumChildren() > 0) {
- stackHead.children_added = true;
- // We need to add the children
- for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
- TNode childNode = *child_it;
- NodeMap::iterator childFind = d_simpITECache.find(childNode);
- if (childFind == d_simpITECache.end()) {
- toVisit.push_back(childNode);
- }
- }
- } else {
- // No children, so we're done
- d_simpITECache[current] = current;
- toVisit.pop_back();
- }
- }
- }
- return d_simpITECache[assertion];
-}
-
-
-ITESimplifier::CareSetPtr ITESimplifier::getNewSet()
-{
- if (d_usedSets.empty()) {
- return ITESimplifier::CareSetPtr::mkNew(*this);
- }
- else {
- ITESimplifier::CareSetPtr cs = ITESimplifier::CareSetPtr::recycle(d_usedSets.back());
- cs.getCareSet().clear();
- d_usedSets.pop_back();
- return cs;
- }
-}
-
-
-void ITESimplifier::updateQueue(CareMap& queue,
- TNode e,
- ITESimplifier::CareSetPtr& careSet)
-{
- CareMap::iterator it = queue.find(e), iend = queue.end();
- if (it != iend) {
- set<Node>& cs2 = (*it).second.getCareSet();
- ITESimplifier::CareSetPtr csNew = getNewSet();
- set_intersection(careSet.getCareSet().begin(),
- careSet.getCareSet().end(),
- cs2.begin(), cs2.end(),
- inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
- (*it).second = csNew;
- }
- else {
- queue[e] = careSet;
- }
-}
-
-
-Node ITESimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
-{
- TNodeMap::iterator it = cache.find(e), iend = cache.end();
- if (it != iend) {
- return it->second;
- }
-
- // do substitution?
- it = substTable.find(e);
- iend = substTable.end();
- if (it != iend) {
- Node result = substitute(it->second, substTable, cache);
- cache[e] = result;
- return result;
- }
-
- size_t sz = e.getNumChildren();
- if (sz == 0) {
- cache[e] = e;
- return e;
- }
-
- NodeBuilder<> builder(e.getKind());
- if (e.getMetaKind() == kind::metakind::PARAMETERIZED) {
- builder << e.getOperator();
- }
- for (unsigned i = 0; i < e.getNumChildren(); ++ i) {
- builder << substitute(e[i], substTable, cache);
- }
-
- Node result = builder;
- // it = substTable.find(result);
- // if (it != iend) {
- // result = substitute(it->second, substTable, cache);
- // }
- cache[e] = result;
- return result;
-}
-
-
-Node ITESimplifier::simplifyWithCare(TNode e)
-{
- TNodeMap substTable;
- CareMap queue;
- CareMap::iterator it;
- ITESimplifier::CareSetPtr cs = getNewSet();
- ITESimplifier::CareSetPtr cs2;
- queue[e] = cs;
-
- TNode v;
- bool done;
- unsigned i;
-
- while (!queue.empty()) {
- it = queue.end();
- --it;
- v = it->first;
- cs = it->second;
- set<Node>& css = cs.getCareSet();
- queue.erase(v);
-
- done = false;
- set<Node>::iterator iCare, iCareEnd = css.end();
-
- switch (v.getKind()) {
- case kind::ITE: {
- iCare = css.find(v[0]);
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = v[1];
- updateQueue(queue, v[1], cs);
- done = true;
- break;
- }
- else {
- iCare = css.find(v[0].negate());
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = v[2];
- updateQueue(queue, v[2], cs);
- done = true;
- break;
- }
- }
- updateQueue(queue, v[0], cs);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0]);
- updateQueue(queue, v[1], cs2);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0].negate());
- updateQueue(queue, v[2], cs2);
- done = true;
- break;
- }
- case kind::AND: {
- for (i = 0; i < v.getNumChildren(); ++i) {
- iCare = css.find(v[i].negate());
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = d_false;
- done = true;
- break;
- }
- }
- if (done) break;
-
- Assert(v.getNumChildren() > 1);
- updateQueue(queue, v[0], cs);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0]);
- for (i = 1; i < v.getNumChildren(); ++i) {
- updateQueue(queue, v[i], cs2);
- }
- done = true;
- break;
- }
- case kind::OR: {
- for (i = 0; i < v.getNumChildren(); ++i) {
- iCare = css.find(v[i]);
- if (iCare != iCareEnd) {
- Assert(substTable.find(v) == substTable.end());
- substTable[v] = d_true;
- done = true;
- break;
- }
- }
- if (done) break;
-
- Assert(v.getNumChildren() > 1);
- updateQueue(queue, v[0], cs);
- cs2 = getNewSet();
- cs2.getCareSet() = css;
- cs2.getCareSet().insert(v[0].negate());
- for (i = 1; i < v.getNumChildren(); ++i) {
- updateQueue(queue, v[i], cs2);
- }
- done = true;
- break;
- }
- default:
- break;
- }
-
- if (done) {
- continue;
- }
-
- for (unsigned i = 0; i < v.getNumChildren(); ++i) {
- updateQueue(queue, v[i], cs);
- }
- }
- while (!d_usedSets.empty()) {
- delete d_usedSets.back();
- d_usedSets.pop_back();
- }
-
- TNodeMap cache;
- return substitute(e, substTable, cache);
-}
-
+++ /dev/null
-/********************* */
-/*! \file ite_simplifier.h
- ** \verbatim
- ** Original author: Clark Barrett
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Simplifications for ITE expressions
- **
- ** This module implements preprocessing phases designed to simplify ITE
- ** expressions. Based on:
- ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
- ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__ITE_SIMPLIFIER_H
-#define __CVC4__ITE_SIMPLIFIER_H
-
-#include <deque>
-#include <vector>
-#include <utility>
-
-#include "expr/node.h"
-#include "expr/command.h"
-#include "prop/prop_engine.h"
-#include "context/cdhashset.h"
-#include "theory/theory.h"
-#include "theory/rewriter.h"
-#include "theory/shared_terms_database.h"
-#include "theory/term_registration_visitor.h"
-#include "theory/valuation.h"
-#include "util/statistics_registry.h"
-#include "util/hash.h"
-#include "util/cache.h"
-#include "util/ite_removal.h"
-
-namespace CVC4 {
-namespace theory {
-
-class ITESimplifier {
- Node d_true;
- Node d_false;
-
- std::hash_map<Node, bool, NodeHashFunction> d_containsTermITECache;
- bool containsTermITE(TNode e);
-
- std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
- bool leavesAreConst(TNode e, theory::TheoryId tid);
- bool leavesAreConst(TNode e)
- { return leavesAreConst(e, theory::Theory::theoryOf(e)); }
-
- typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
- typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
-
- typedef std::pair<Node, Node> NodePair;
- struct NodePairHashFunction {
- size_t operator () (const NodePair& pair) const {
- size_t hash = 0;
- hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first);
- hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
- return hash;
- }
- };/* struct ITESimplifier::NodePairHashFunction */
-
- typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
-
-
- NodePairMap d_simpConstCache;
- Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
- std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
- Node getSimpVar(TypeNode t);
-
- NodeMap d_simpContextCache;
- Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
-
- Node simpITEAtom(TNode atom);
-
- NodeMap d_simpITECache;
-
-public:
- Node simpITE(TNode assertion);
-
-private:
-
- class CareSetPtr;
- class CareSetPtrVal {
- friend class ITESimplifier::CareSetPtr;
- ITESimplifier& d_iteSimplifier;
- unsigned d_refCount;
- std::set<Node> d_careSet;
- CareSetPtrVal(ITESimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
- };
-
- std::vector<CareSetPtrVal*> d_usedSets;
- void careSetPtrGC(CareSetPtrVal* val) {
- d_usedSets.push_back(val);
- }
-
- class CareSetPtr {
- CareSetPtrVal* d_val;
- CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
- public:
- CareSetPtr() : d_val(NULL) {}
- CareSetPtr(const CareSetPtr& cs) {
- d_val = cs.d_val;
- if (d_val != NULL) {
- ++(d_val->d_refCount);
- }
- }
- ~CareSetPtr() {
- if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
- d_val->d_iteSimplifier.careSetPtrGC(d_val);
- }
- }
- CareSetPtr& operator=(const CareSetPtr& cs) {
- if (d_val != cs.d_val) {
- if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
- d_val->d_iteSimplifier.careSetPtrGC(d_val);
- }
- d_val = cs.d_val;
- if (d_val != NULL) {
- ++(d_val->d_refCount);
- }
- }
- return *this;
- }
- std::set<Node>& getCareSet() { return d_val->d_careSet; }
- static CareSetPtr mkNew(ITESimplifier& simp) {
- CareSetPtrVal* val = new CareSetPtrVal(simp);
- return CareSetPtr(val);
- }
- static CareSetPtr recycle(CareSetPtrVal* val) {
- Assert(val != NULL && val->d_refCount == 0);
- val->d_refCount = 1;
- return CareSetPtr(val);
- }
- };
-
- CareSetPtr getNewSet();
-
- typedef std::map<TNode, CareSetPtr> CareMap;
- void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
- Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
-
-public:
- Node simplifyWithCare(TNode e);
-
- ITESimplifier() {
- d_true = NodeManager::currentNM()->mkConst<bool>(true);
- d_false = NodeManager::currentNM()->mkConst<bool>(false);
- }
- ~ITESimplifier() {}
-
-};
-
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif
--- /dev/null
+/********************* */
+/*! \file ite_simplifier.cpp
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Simplifications for ITE expressions
+ **
+ ** This module implements preprocessing phases designed to simplify ITE
+ ** expressions. Based on:
+ ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
+ ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
+ **/
+
+
+#include "theory/ite_utilities.h"
+#include <utility>
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+using namespace std;
+namespace CVC4 {
+namespace theory {
+
+namespace ite {
+inline static bool isTermITE(TNode e) {
+ return (e.getKind() == kind::ITE && !e.getType().isBoolean());
+}
+
+inline static bool triviallyContainsNoTermITEs(TNode e) {
+ return e.isConst() || e.isVar();
+}
+
+static bool isTheoryAtom(TNode a){
+ using namespace kind;
+ switch(a.getKind()){
+ case EQUAL:
+ case DISTINCT:
+ return !(a[0].getType().isBoolean());
+
+ /* from uf */
+ case APPLY_UF:
+ return a.getType().isBoolean();
+ case CARDINALITY_CONSTRAINT:
+ case DIVISIBLE:
+ case LT:
+ case LEQ:
+ case GT:
+ case GEQ:
+ case IS_INTEGER:
+ case BITVECTOR_COMP:
+ case BITVECTOR_ULT:
+ case BITVECTOR_ULE:
+ case BITVECTOR_UGT:
+ case BITVECTOR_UGE:
+ case BITVECTOR_SLT:
+ case BITVECTOR_SLE:
+ case BITVECTOR_SGT:
+ case BITVECTOR_SGE:
+ return true;
+ default:
+ return false;
+ }
+}
+
+struct CTIVStackElement {
+ TNode curr;
+ unsigned pos;
+ CTIVStackElement(){}
+ CTIVStackElement(TNode c) : curr(c), pos(0){ }
+};/* CTIVStackElement */
+
+} /* CVC4::theory::ite */
+
+
+
+ITEUtilities::ITEUtilities(ContainsTermITEVistor* containsVisitor)
+ : d_containsVisitor(containsVisitor)
+ , d_compressor(NULL)
+ , d_simplifier(NULL)
+ , d_careSimp(NULL)
+{
+ Assert(d_containsVisitor != NULL);
+}
+
+ITEUtilities::~ITEUtilities(){
+
+ if(d_simplifier != NULL){
+ delete d_simplifier;
+ }
+ if(d_compressor != NULL){
+ delete d_compressor;
+ }
+ if(d_careSimp != NULL){
+ delete d_careSimp;
+ }
+}
+
+Node ITEUtilities::simpITE(TNode assertion){
+ if(d_simplifier == NULL){
+ d_simplifier = new ITESimplifier(d_containsVisitor);
+ }
+ return d_simplifier->simpITE(assertion);
+}
+
+bool ITEUtilities::simpIteDidALotOfWorkHeuristic() const{
+ if(d_simplifier == NULL){
+ return false;
+ }else{
+ return d_simplifier->doneALotOfWorkHeuristic();
+ }
+}
+
+/* returns false if an assertion is discovered to be equal to false. */
+bool ITEUtilities::compress(std::vector<Node>& assertions){
+ if(d_compressor == NULL){
+ d_compressor = new ITECompressor(d_containsVisitor);
+ }
+ return d_compressor->compress(assertions);
+}
+
+Node ITEUtilities::simplifyWithCare(TNode e){
+ if(d_careSimp == NULL){
+ d_careSimp = new ITECareSimplifier();
+ }
+ return d_careSimp->simplifyWithCare(e);
+}
+
+void ITEUtilities::clear(){
+ if(d_simplifier != NULL){
+ d_simplifier->clearSimpITECaches();
+ }
+ if(d_compressor != NULL){
+ d_compressor->garbageCollect();
+ }
+ if(d_careSimp != NULL){
+ d_careSimp->clear();
+ }
+}
+
+/********************* */
+/* ContainsTermITEVistor
+ */
+ContainsTermITEVistor::ContainsTermITEVistor(): d_cache() {}
+ContainsTermITEVistor::~ContainsTermITEVistor(){}
+bool ContainsTermITEVistor::containsTermITE(TNode e){
+ /* throughout execution skip through NOT nodes. */
+ e = (e.getKind() == kind::NOT) ? e[0] : e;
+ if(ite::triviallyContainsNoTermITEs(e)){ return false; }
+
+ NodeBoolMap::const_iterator end = d_cache.end();
+ NodeBoolMap::const_iterator tmp_it = d_cache.find(e);
+ if(tmp_it != end){
+ return (*tmp_it).second;
+ }
+
+ bool foundTermIte = false;
+ std::vector<ite::CTIVStackElement> stack;
+ stack.push_back(ite::CTIVStackElement(e));
+ while(!foundTermIte && !stack.empty()){
+ ite::CTIVStackElement& top = stack.back();
+ TNode curr = top.curr;
+ if(top.pos >= curr.getNumChildren()){
+ // all of the children have been visited
+ // no term ites were found
+ d_cache[curr] = false;
+ stack.pop_back();
+ }else{
+ // this is someone's child
+ TNode child = curr[top.pos];
+ child = (child.getKind() == kind::NOT) ? child[0] : child;
+ ++top.pos;
+ if(ite::triviallyContainsNoTermITEs(child)){
+ // skip
+ }else{
+ tmp_it = d_cache.find(child);
+ if(tmp_it != end){
+ foundTermIte = (*tmp_it).second;
+ }else{
+ stack.push_back(ite::CTIVStackElement(child));
+ foundTermIte = ite::isTermITE(child);
+ }
+ }
+ }
+ }
+ if(foundTermIte){
+ while(!stack.empty()){
+ TNode curr = stack.back().curr;
+ stack.pop_back();
+ d_cache[curr] = true;
+ }
+ }
+ return foundTermIte;
+}
+void ContainsTermITEVistor::garbageCollect() {
+ d_cache.clear();
+}
+
+/********************* */
+/* IncomingArcCounter
+ */
+IncomingArcCounter::IncomingArcCounter(bool skipVars, bool skipConstants)
+ : d_reachCount()
+ , d_skipVariables(skipVars)
+ , d_skipConstants(skipConstants)
+{}
+IncomingArcCounter::~IncomingArcCounter(){}
+
+void IncomingArcCounter::computeReachability(const std::vector<Node>& assertions){
+ std::vector<TNode> tovisit(assertions.begin(), assertions.end());
+
+ while(!tovisit.empty()){
+ TNode back = tovisit.back();
+ tovisit.pop_back();
+
+ bool skip = false;
+ switch(back.getMetaKind()){
+ case kind::metakind::CONSTANT:
+ skip = d_skipConstants;
+ break;
+ case kind::metakind::VARIABLE:
+ skip = d_skipVariables;
+ break;
+ default:
+ break;
+ }
+
+ if(skip) { continue; }
+ if(d_reachCount.find(back) != d_reachCount.end()){
+ d_reachCount[back] = 1 + d_reachCount[back];
+ }else{
+ d_reachCount[back] = 1;
+ for(TNode::iterator cit=back.begin(), end = back.end(); cit != end; ++cit){
+ tovisit.push_back(*cit);
+ }
+ }
+ }
+}
+
+void IncomingArcCounter::clear() {
+ d_reachCount.clear();
+}
+
+/********************* */
+/* ITECompressor
+ */
+ITECompressor::ITECompressor(ContainsTermITEVistor* contains)
+ : d_contains(contains)
+ , d_assertions(NULL)
+ , d_incoming(true, true)
+{
+ Assert(d_contains != NULL);
+
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITECompressor::~ITECompressor() {
+ reset();
+}
+
+void ITECompressor::reset(){
+ d_incoming.clear();
+ d_compressed.clear();
+}
+
+void ITECompressor::garbageCollect(){
+ reset();
+}
+
+ITECompressor::Statistics::Statistics():
+ d_compressCalls("ite-simp::compressCalls", 0),
+ d_skolemsAdded("ite-simp::skolems", 0)
+{
+ StatisticsRegistry::registerStat(&d_compressCalls);
+ StatisticsRegistry::registerStat(&d_skolemsAdded);
+
+}
+ITECompressor::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_compressCalls);
+ StatisticsRegistry::unregisterStat(&d_skolemsAdded);
+}
+
+Node ITECompressor::push_back_boolean(Node original, Node compressed){
+ Node rewritten = Rewriter::rewrite(compressed);
+ // There is a bug if the rewritter takes a pure boolean expression
+ // and changes its theory
+ if(rewritten.isConst()){
+ d_compressed[compressed] = rewritten;
+ d_compressed[original] = rewritten;
+ d_compressed[rewritten] = rewritten;
+ return rewritten;
+ }else if(d_compressed.find(rewritten) != d_compressed.end()){
+ Node res = d_compressed[rewritten];
+ d_compressed[original] = res;
+ d_compressed[compressed] = res;
+ return res;
+ }else if(rewritten.isVar() ||
+ (rewritten.getKind() == kind::NOT && rewritten[0].isVar())){
+ d_compressed[original] = rewritten;
+ d_compressed[compressed] = rewritten;
+ d_compressed[rewritten] = rewritten;
+ return rewritten;
+ }else{
+ NodeManager* nm = NodeManager::currentNM();
+ Node skolem = nm->mkSkolem("compress_$$", nm->booleanType());
+ d_compressed[rewritten] = skolem;
+ d_compressed[original] = skolem;
+ d_compressed[compressed] = skolem;
+
+ Node iff = skolem.iffNode(rewritten);
+ d_assertions->push_back(iff);
+ ++(d_statistics.d_skolemsAdded);
+ return skolem;
+ }
+}
+
+bool ITECompressor::multipleParents(TNode c){
+ return d_incoming.lookupIncoming(c) >= 2;
+}
+
+Node ITECompressor::compressBooleanITEs(Node toCompress){
+ Assert(toCompress.getKind() == kind::ITE);
+ Assert(toCompress.getType().isBoolean());
+
+ if(!(toCompress[1] == d_false || toCompress[2] == d_false)){
+ Node cmpCnd = compressBoolean(toCompress[0]);
+ if(cmpCnd.isConst()){
+ Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
+ Node res = compressBoolean(branch);
+ d_compressed[toCompress] = res;
+ return res;
+ }else{
+ Node cmpThen = compressBoolean(toCompress[1]);
+ Node cmpElse = compressBoolean(toCompress[2]);
+ Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
+ if(multipleParents(toCompress)){
+ return push_back_boolean(toCompress, newIte);
+ }else{
+ return newIte;
+ }
+ }
+ }
+
+ NodeBuilder<> nb(kind::AND);
+ Node curr = toCompress;
+ while(curr.getKind() == kind::ITE &&
+ (curr[1] == d_false || curr[2] == d_false) &&
+ (!multipleParents(curr) || curr == toCompress)){
+
+ bool negateCnd = (curr[1] == d_false);
+ Node compressCnd = compressBoolean(curr[0]);
+ if(compressCnd.isConst()){
+ if(compressCnd.getConst<bool>() == negateCnd){
+ return push_back_boolean(toCompress, d_false);
+ }else{
+ // equivalent to true don't push back
+ }
+ }else{
+ Node pb = negateCnd ? compressCnd.notNode() : compressCnd;
+ nb << pb;
+ }
+ curr = negateCnd ? curr[2] : curr[1];
+ }
+ Assert(toCompress != curr);
+
+ nb << compressBoolean(curr);
+ Node res = nb.getNumChildren() == 1 ? nb[0] : (Node)nb;
+ return push_back_boolean(toCompress, res);
+}
+
+Node ITECompressor::compressTerm(Node toCompress){
+ if(toCompress.isConst() || toCompress.isVar()){
+ return toCompress;
+ }
+
+ if(d_compressed.find(toCompress) != d_compressed.end()){
+ return d_compressed[toCompress];
+ }
+ if(toCompress.getKind() == kind::ITE){
+ Node cmpCnd = compressBoolean(toCompress[0]);
+ if(cmpCnd.isConst()){
+ Node branch = (cmpCnd == d_true) ? toCompress[1] : toCompress[2];
+ Node res = compressTerm(toCompress);
+ d_compressed[toCompress] = res;
+ return res;
+ }else{
+ Node cmpThen = compressTerm(toCompress[1]);
+ Node cmpElse = compressTerm(toCompress[2]);
+ Node newIte = cmpCnd.iteNode(cmpThen, cmpElse);
+ d_compressed[toCompress] = newIte;
+ return newIte;
+ }
+ }
+
+ NodeBuilder<> nb(toCompress.getKind());
+
+ if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << (toCompress.getOperator());
+ }
+ for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
+ nb << compressTerm(*it);
+ }
+ Node compressed = (Node)nb;
+ if(multipleParents(toCompress)){
+ d_compressed[toCompress] = compressed;
+ }
+ return compressed;
+}
+
+Node ITECompressor::compressBoolean(Node toCompress){
+ static int instance = 0;
+ ++instance;
+ if(toCompress.isConst() || toCompress.isVar()){
+ return toCompress;
+ }
+ if(d_compressed.find(toCompress) != d_compressed.end()){
+ return d_compressed[toCompress];
+ }else if(toCompress.getKind() == kind::ITE){
+ return compressBooleanITEs(toCompress);
+ }else{
+ bool ta = ite::isTheoryAtom(toCompress);
+ NodeBuilder<> nb(toCompress.getKind());
+ if(toCompress.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << (toCompress.getOperator());
+ }
+ for(Node::iterator it = toCompress.begin(), end = toCompress.end(); it != end; ++it){
+ Node pb = (ta) ? compressTerm(*it) : compressBoolean(*it);
+ nb << pb;
+ }
+ Node compressed = nb;
+ if(ta || multipleParents(toCompress)){
+ return push_back_boolean(toCompress, compressed);
+ }else{
+ return compressed;
+ }
+ }
+}
+
+
+
+bool ITECompressor::compress(std::vector<Node>& assertions){
+ reset();
+
+ d_assertions = &assertions;
+ d_incoming.computeReachability(assertions);
+
+ ++(d_statistics.d_compressCalls);
+ Chat() << "Computed reachability" << endl;
+
+ bool nofalses = true;
+ size_t original_size = assertions.size();
+ Chat () << "compressing " << original_size << endl;
+ for(size_t i = 0; i < original_size && nofalses; ++i){
+ Node assertion = assertions[i];
+ Node compressed = compressBoolean(assertion);
+ Node rewritten = Rewriter::rewrite(compressed);
+ assertions[i] = rewritten;
+ Assert(!d_contains->containsTermITE(rewritten));
+
+ nofalses = (rewritten != d_false);
+ }
+
+ d_assertions = NULL;
+
+ return nofalses;
+}
+
+TermITEHeightCounter::TermITEHeightCounter()
+ :d_termITEHeight()
+{}
+
+TermITEHeightCounter::~TermITEHeightCounter(){}
+
+void TermITEHeightCounter::clear(){
+ d_termITEHeight.clear();
+}
+
+size_t TermITEHeightCounter::cache_size() const{
+ return d_termITEHeight.size();
+}
+
+namespace ite {
+struct TITEHStackElement {
+ TNode curr;
+ unsigned pos;
+ uint32_t maxChildHeight;
+ TITEHStackElement(){}
+ TITEHStackElement(TNode c) : curr(c), pos(0), maxChildHeight(0){ }
+};
+} /* namespace ite */
+
+uint32_t TermITEHeightCounter::termITEHeight(TNode e){
+
+ if(ite::triviallyContainsNoTermITEs(e)){ return 0; }
+
+ NodeCountMap::const_iterator end = d_termITEHeight.end();
+ NodeCountMap::const_iterator tmp_it = d_termITEHeight.find(e);
+ if(tmp_it != end){
+ return (*tmp_it).second;
+ }
+
+
+ uint32_t returnValue = 0;
+ // This is initially 0 as the very first call this is included in the max,
+ // but this has no effect.
+ std::vector<ite::TITEHStackElement> stack;
+ stack.push_back(ite::TITEHStackElement(e));
+ while(!stack.empty()){
+ ite::TITEHStackElement& top = stack.back();
+ top.maxChildHeight = std::max(top.maxChildHeight, returnValue);
+ TNode curr = top.curr;
+ if(top.pos >= curr.getNumChildren()){
+ // done with the current node
+ returnValue = top.maxChildHeight + (ite::isTermITE(curr) ? 1 : 0);
+ d_termITEHeight[curr] = returnValue;
+ stack.pop_back();
+ continue;
+ }else{
+ if(top.pos == 0 && curr.getKind() == kind::ITE){
+ ++top.pos;
+ returnValue = 0;
+ continue;
+ }
+ // this is someone's child
+ TNode child = curr[top.pos];
+ ++top.pos;
+ if(ite::triviallyContainsNoTermITEs(child)){
+ returnValue = 0;
+ }else{
+ tmp_it = d_termITEHeight.find(child);
+ if(tmp_it != end){
+ returnValue = (*tmp_it).second;
+ }else{
+ stack.push_back(ite::TITEHStackElement(child));
+ }
+ }
+ }
+ }
+ return returnValue;
+}
+
+
+
+ITESimplifier::ITESimplifier(ContainsTermITEVistor* contains)
+ : d_containsVisitor(contains)
+ , d_termITEHeight()
+ , d_constantLeaves()
+ , d_allocatedConstantLeaves()
+ , d_citeEqConstApplications(0)
+ , d_constantIteEqualsConstantCache()
+ , d_replaceOverCache()
+ , d_replaceOverTermIteCache()
+ , d_leavesConstCache()
+ , d_simpConstCache()
+ , d_simpContextCache()
+ , d_simpITECache()
+{
+ Assert(d_containsVisitor != NULL);
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITESimplifier::~ITESimplifier() {
+ clearSimpITECaches();
+ Assert(d_constantLeaves.empty());
+ Assert(d_allocatedConstantLeaves.empty());
+}
+
+bool ITESimplifier::leavesAreConst(TNode e){
+ return leavesAreConst(e, theory::Theory::theoryOf(e));
+}
+
+void ITESimplifier::clearSimpITECaches(){
+ Chat() << "clear ite caches " << endl;
+ for(size_t i = 0, N = d_allocatedConstantLeaves.size(); i < N; ++i){
+ NodeVec* curr = d_allocatedConstantLeaves[i];
+ delete curr;
+ }
+ d_citeEqConstApplications = 0;
+ d_constantLeaves.clear();
+ d_allocatedConstantLeaves.clear();
+ d_termITEHeight.clear();
+ d_constantIteEqualsConstantCache.clear();
+ d_replaceOverCache.clear();
+ d_replaceOverTermIteCache.clear();
+ d_simpITECache.clear();
+ d_simpVars.clear();
+ d_simpConstCache.clear();
+ d_leavesConstCache.clear();
+ d_simpContextCache.clear();
+}
+
+bool ITESimplifier::doneALotOfWorkHeuristic() const {
+ static const size_t SIZE_BOUND = 1000;
+ Chat() << "d_citeEqConstApplications size " << d_citeEqConstApplications << endl;
+ return (d_citeEqConstApplications > SIZE_BOUND);
+}
+
+ITESimplifier::Statistics::Statistics():
+ d_maxNonConstantsFolded("ite-simp::maxNonConstantsFolded", 0),
+ d_unexpected("ite-simp::unexpected", 0),
+ d_unsimplified("ite-simp::unsimplified", 0),
+ d_exactMatchFold("ite-simp::exactMatchFold", 0),
+ d_binaryPredFold("ite-simp::binaryPredFold", 0),
+ d_specialEqualityFolds("ite-simp::specialEqualityFolds", 0),
+ d_simpITEVisits("ite-simp::simpITE.visits", 0),
+ d_inSmaller("ite-simp::inSmaller")
+{
+ StatisticsRegistry::registerStat(&d_maxNonConstantsFolded);
+ StatisticsRegistry::registerStat(&d_unexpected);
+ StatisticsRegistry::registerStat(&d_unsimplified);
+ StatisticsRegistry::registerStat(&d_exactMatchFold);
+ StatisticsRegistry::registerStat(&d_binaryPredFold);
+ StatisticsRegistry::registerStat(&d_specialEqualityFolds);
+ StatisticsRegistry::registerStat(&d_simpITEVisits);
+ StatisticsRegistry::registerStat(&d_inSmaller);
+}
+
+ITESimplifier::Statistics::~Statistics(){
+ StatisticsRegistry::unregisterStat(&d_maxNonConstantsFolded);
+ StatisticsRegistry::unregisterStat(&d_unexpected);
+ StatisticsRegistry::unregisterStat(&d_unsimplified);
+ StatisticsRegistry::unregisterStat(&d_exactMatchFold);
+ StatisticsRegistry::unregisterStat(&d_binaryPredFold);
+ StatisticsRegistry::unregisterStat(&d_specialEqualityFolds);
+ StatisticsRegistry::unregisterStat(&d_simpITEVisits);
+ StatisticsRegistry::unregisterStat(&d_inSmaller);
+}
+
+bool ITESimplifier::isConstantIte(TNode e){
+ if(e.isConst()){
+ return true;
+ }else if(ite::isTermITE(e)){
+ NodeVec* constants = computeConstantLeaves(e);
+ return constants != NULL;
+ }else{
+ return false;
+ }
+}
+
+ITESimplifier::NodeVec* ITESimplifier::computeConstantLeaves(TNode ite){
+ Assert(ite::isTermITE(ite));
+ ConstantLeavesMap::const_iterator it = d_constantLeaves.find(ite);
+ ConstantLeavesMap::const_iterator end = d_constantLeaves.end();
+ if(it != end){
+ return (*it).second;
+ }
+ TNode thenB = ite[1];
+ TNode elseB = ite[2];
+
+ // special case 2 constant children
+ if(thenB.isConst() && elseB.isConst()){
+ NodeVec* pair = new NodeVec(2);
+ (*pair)[0] = std::min(thenB, elseB);
+ (*pair)[1] = std::max(thenB, elseB);
+ d_constantLeaves[ite] = pair;
+ return pair;
+ }
+ // At least 1 is an ITE
+ if(!(thenB.isConst() || thenB.getKind() == kind::ITE) ||
+ !(elseB.isConst() || elseB.getKind() == kind::ITE)){
+ // Cannot be a termITE tree
+ d_constantLeaves[ite] = NULL;
+ return NULL;
+ }
+
+ // At least 1 is not a constant
+ TNode definitelyITE = thenB.isConst() ? elseB : thenB;
+ TNode maybeITE = thenB.isConst() ? thenB : elseB;
+
+ NodeVec* defChildren = computeConstantLeaves(definitelyITE);
+ if(defChildren == NULL){
+ d_constantLeaves[ite] = NULL;
+ return NULL;
+ }
+
+ NodeVec scratch;
+ NodeVec* maybeChildren = NULL;
+ if(maybeITE.getKind() == kind::ITE){
+ maybeChildren = computeConstantLeaves(maybeITE);
+ }else{
+ scratch.push_back(maybeITE);
+ maybeChildren = &scratch;
+ }
+ if(maybeChildren == NULL){
+ d_constantLeaves[ite] = NULL;
+ return NULL;
+ }
+
+ NodeVec* both = new NodeVec(defChildren->size()+maybeChildren->size());
+ NodeVec::iterator newEnd;
+ newEnd = std::set_union(defChildren->begin(), defChildren->end(),
+ maybeChildren->begin(), maybeChildren->end(),
+ both->begin());
+ both->resize(newEnd - both->begin());
+ d_constantLeaves[ite] = both;
+ return both;
+}
+
+// This is uncached! Better for protoyping or getting limited size examples
+struct IteTreeSearchData{
+ set<Node> visited;
+ set<Node> constants;
+ set<Node> nonConstants;
+ int maxConstants;
+ int maxNonconstants;
+ int maxDepth;
+ bool failure;
+ IteTreeSearchData()
+ : maxConstants(-1), maxNonconstants(-1), maxDepth(-1), failure(false)
+ {}
+};
+void iteTreeSearch(Node e, int depth, IteTreeSearchData& search){
+ if(search.maxDepth >= 0 && depth > search.maxDepth){
+ search.failure = true;
+ }
+ if(search.failure){
+ return;
+ }
+ if(search.visited.find(e) != search.visited.end()){
+ return;
+ }else{
+ search.visited.insert(e);
+ }
+
+ if(e.isConst()){
+ search.constants.insert(e);
+ if(search.maxConstants >= 0 &&
+ search.constants.size() > (unsigned)search.maxConstants){
+ search.failure = true;
+ }
+ }else if(e.getKind() == kind::ITE){
+ iteTreeSearch(e[1], depth+1, search);
+ iteTreeSearch(e[2], depth+1, search);
+ }else{
+ search.nonConstants.insert(e);
+ if(search.maxNonconstants >= 0 &&
+ search.nonConstants.size() > (unsigned)search.maxNonconstants){
+ search.failure = true;
+ }
+ }
+}
+
+Node ITESimplifier::replaceOver(Node n, Node replaceWith, Node simpVar){
+ if(n == simpVar){
+ return replaceWith;
+ }else if(n.getNumChildren() == 0){
+ return n;
+ }
+ Assert(n.getNumChildren() > 0);
+ Assert(!n.isVar());
+
+ pair<Node, Node> p = make_pair(n, replaceWith);
+ if(d_replaceOverCache.find(p) != d_replaceOverCache.end()){
+ return d_replaceOverCache[p];
+ }
+
+ NodeBuilder<> builder(n.getKind());
+ if (n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << n.getOperator();
+ }
+ unsigned i = 0;
+ for (; i < n.getNumChildren(); ++ i) {
+ Node newChild = replaceOver(n[i], replaceWith, simpVar);
+ builder << newChild;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ d_replaceOverCache[p] = result;
+ return result;
+}
+
+Node ITESimplifier::replaceOverTermIte(Node e, Node simpAtom, Node simpVar){
+ if(e.getKind() == kind::ITE){
+ pair<Node, Node> p = make_pair(e, simpAtom);
+ if(d_replaceOverTermIteCache.find(p) != d_replaceOverTermIteCache.end()){
+ return d_replaceOverTermIteCache[p];
+ }
+ Assert(!e.getType().isBoolean());
+ Node cnd = e[0];
+ Node newThen = replaceOverTermIte(e[1], simpAtom, simpVar);
+ Node newElse = replaceOverTermIte(e[2], simpAtom, simpVar);
+ Node newIte = cnd.iteNode(newThen, newElse);
+ d_replaceOverTermIteCache[p] = newIte;
+ return newIte;
+ }else{
+ return replaceOver(simpAtom, e, simpVar);
+ }
+}
+
+Node ITESimplifier::attemptLiftEquality(TNode atom){
+ if(atom.getKind() == kind::EQUAL){
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if((left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
+ !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
+
+ // exactly 1 is an ite
+ TNode ite = left.getKind() == kind::ITE ? left :right;
+ TNode notIte = left.getKind() == kind::ITE ? right : left;
+
+ if(notIte == ite[1]){
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(d_true, notIte.eqNode(ite[2]));
+ }else if(notIte == ite[2]){
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(notIte.eqNode(ite[1]), d_true);
+ }
+ if(notIte.isConst() &&
+ (ite[1].isConst() || ite[2].isConst())){
+ ++(d_statistics.d_exactMatchFold);
+ return ite[0].iteNode(notIte.eqNode(ite[1]), notIte.eqNode(ite[2]));
+ }
+ }
+ }
+
+ // try a similar more relaxed version for non-equality operators
+ if(atom.getMetaKind() == kind::metakind::OPERATOR &&
+ atom.getNumChildren() == 2 &&
+ !atom[1].getType().isBoolean()){
+
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if( (left.getKind() == kind::ITE || right.getKind() == kind::ITE)&&
+ !(left.getKind() == kind::ITE && right.getKind() == kind::ITE)){
+ // exactly 1 is an ite
+ bool leftIsIte = left.getKind() == kind::ITE;
+ Node ite = leftIsIte ? left :right;
+ Node notIte = leftIsIte ? right : left;
+
+ if(notIte.isConst()){
+ IteTreeSearchData search;
+ search.maxNonconstants = 2;
+ iteTreeSearch(ite, 0, search);
+ if(!search.failure){
+ d_statistics.d_maxNonConstantsFolded.maxAssign(search.nonConstants.size());
+ Debug("ite::simpite") << "used " << search.nonConstants.size() << " nonconstants" << endl;
+ NodeManager* nm = NodeManager::currentNM();
+ Node simpVar = getSimpVar(notIte.getType());
+ TNode newLeft = leftIsIte ? simpVar : notIte;
+ TNode newRight = leftIsIte ? notIte : simpVar;
+ Node newAtom = nm->mkNode(atom.getKind(), newLeft, newRight);
+
+ ++(d_statistics.d_binaryPredFold);
+ return replaceOverTermIte(ite, newAtom, simpVar);
+ }
+ }
+ }
+ }
+
+ // TODO "This is way too tailored. Must generalize!"
+ if(atom.getKind() == kind::EQUAL &&
+ atom.getNumChildren() == 2 &&
+ ite::isTermITE(atom[0]) &&
+ atom[1].getKind() == kind::MULT &&
+ atom[1].getNumChildren() == 2 &&
+ atom[1][0].isConst() &&
+ atom[1][0].getConst<Rational>().isNegativeOne() &&
+ ite::isTermITE(atom[1][1]) &&
+ d_termITEHeight.termITEHeight(atom[0]) == 1 &&
+ d_termITEHeight.termITEHeight(atom[1][1]) == 1 &&
+ (atom[0][1].isConst() || atom[0][2].isConst()) &&
+ (atom[1][1][1].isConst() || atom[1][1][2].isConst()) ){
+ // expand all 4 cases
+
+ Node negOne = atom[1][0];
+
+ Node lite = atom[0];
+ Node lC = lite[0];
+ Node lT = lite[1];
+ Node lE = lite[2];
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node negRite = atom[1][1];
+ Node rC = negRite[0];
+ Node rT = nm->mkNode(kind::MULT, negOne, negRite[1]);
+ Node rE = nm->mkNode(kind::MULT, negOne, negRite[2]);
+
+ // (ite lC lT lE) = (ite rC rT rE)
+ // (ite lc (= lT (ite rC rT rE) (= lE (ite rC rT rE))))
+ // (ite lc (ite rC (= lT rT) (= lT rE))
+ // (ite rC (= lE rT) (= lE rE)))
+
+ Node eqTT = lT.eqNode(rT);
+ Node eqTE = lT.eqNode(rE);
+ Node eqET = lE.eqNode(rT);
+ Node eqEE = lE.eqNode(rE);
+ Node thenLC = rC.iteNode(eqTT, eqTE);
+ Node elseLC = rC.iteNode(eqET, eqEE);
+ Node newIte = lC.iteNode(thenLC, elseLC);
+
+ ++(d_statistics.d_specialEqualityFolds);
+ return newIte;
+ }
+ return Node::null();
+}
+
+// Interesting classes of atoms:
+// 2. Contains constants and 1 constant term ite
+// 3. Contains 2 constant term ites
+Node ITESimplifier::transformAtom(TNode atom){
+ if(! d_containsVisitor->containsTermITE(atom)){
+ if(atom.getKind() == kind::EQUAL &&
+ atom[0].isConst() && atom[1].isConst()){
+ // constant equality
+ return NodeManager::currentNM()->mkConst<bool>(atom[0] == atom[1]);
+ }
+ return Node::null();
+ }else{
+ Node acr = attemptConstantRemoval(atom);
+ if(!acr.isNull()){
+ return acr;
+ }
+ // Node ale = attemptLiftEquality(atom);
+ // if(!ale.isNull()){
+ // //return ale;
+ // }
+ return Node::null();
+ }
+}
+
+static unsigned numBranches = 0;
+static unsigned numFalseBranches = 0;
+static unsigned itesMade = 0;
+
+Node ITESimplifier::constantIteEqualsConstant(TNode cite, TNode constant){
+ static int instance = 0;
+ ++instance;
+ Debug("ite::constantIteEqualsConstant") << instance << "constantIteEqualsConstant("<<cite << ", " << constant<<")"<< endl;
+ if(cite.isConst()){
+ Node res = (cite == constant) ? d_true : d_false;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << res << endl;
+ return res;
+ }
+ std::pair<Node,Node> pair = make_pair(cite, constant);
+
+ NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
+ if(eq_pos != d_constantIteEqualsConstantCache.end()){
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << (*eq_pos).second << endl;
+ return (*eq_pos).second;
+ }
+
+ ++d_citeEqConstApplications;
+
+ NodeVec* leaves = computeConstantLeaves(cite);
+ Assert(leaves != NULL);
+ if(std::binary_search(leaves->begin(), leaves->end(), constant)){
+ if(leaves->size() == 1){
+ // probably unreachable
+ d_constantIteEqualsConstantCache[pair] = d_true;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << d_true << endl;
+ return d_true;
+ }else{
+ Assert(cite.getKind() == kind::ITE);
+ TNode cnd = cite[0];
+ TNode tB = cite[1];
+ TNode fB = cite[2];
+ Node tEqs = constantIteEqualsConstant(tB, constant);
+ Node fEqs = constantIteEqualsConstant(fB, constant);
+ Node boolIte = cnd.iteNode(tEqs, fEqs);
+ if(!(tEqs.isConst() || fEqs.isConst())){
+ ++numBranches;
+ }
+ if(!(tEqs == d_false || fEqs == d_false)){
+ ++numFalseBranches;
+ }
+ ++itesMade;
+ d_constantIteEqualsConstantCache[pair] = boolIte;
+ //Debug("ite::constantIteEqualsConstant") << instance << "->" << boolIte << endl;
+ return boolIte;
+ }
+ }else{
+ d_constantIteEqualsConstantCache[pair] = d_false;
+ Debug("ite::constantIteEqualsConstant") << instance << "->" << d_false << endl;
+ return d_false;
+ }
+}
+
+
+Node ITESimplifier::intersectConstantIte(TNode lcite, TNode rcite){
+ // intersect the constant ite trees lcite and rcite
+
+ if(lcite.isConst() || rcite.isConst()){
+ bool lIsConst = lcite.isConst();
+ TNode constant = lIsConst ? lcite : rcite;
+ TNode cite = lIsConst ? rcite : lcite;
+
+ (d_statistics.d_inSmaller)<< 1;
+ unsigned preItesMade = itesMade;
+ unsigned preNumBranches = numBranches;
+ unsigned preNumFalseBranches = numFalseBranches;
+ Node bterm = constantIteEqualsConstant(cite, constant);
+ Debug("intersectConstantIte")
+ << (numBranches - preNumBranches)
+ << " " << (numFalseBranches - preNumFalseBranches)
+ << " " << (itesMade - preItesMade) << endl;
+ return bterm;
+ }
+ Assert(lcite.getKind() == kind::ITE);
+ Assert(rcite.getKind() == kind::ITE);
+
+ NodeVec* leftValues = computeConstantLeaves(lcite);
+ NodeVec* rightValues = computeConstantLeaves(rcite);
+
+ uint32_t smaller = std::min(leftValues->size(), rightValues->size());
+
+ (d_statistics.d_inSmaller)<< smaller;
+ NodeVec intersection(smaller, Node::null());
+ NodeVec::iterator newEnd;
+ newEnd = std::set_intersection(leftValues->begin(), leftValues->end(),
+ rightValues->begin(), rightValues->end(),
+ intersection.begin());
+ intersection.resize(newEnd - intersection.begin());
+ if(intersection.empty()){
+ return d_false;
+ }else{
+ NodeBuilder<> nb(kind::OR);
+ NodeVec::const_iterator it = intersection.begin(), end=intersection.end();
+ for(; it != end; ++it){
+ Node inBoth = *it;
+ Node lefteq = constantIteEqualsConstant(lcite, inBoth);
+ Node righteq = constantIteEqualsConstant(rcite, inBoth);
+ Node bothHold = lefteq.andNode(righteq);
+ nb << bothHold;
+ }
+ Node result = (nb.getNumChildren() >= 1) ? (Node)nb : nb[0];
+ return result;
+ }
+}
+
+
+Node ITESimplifier::attemptEagerRemoval(TNode atom){
+ if(atom.getKind() == kind::EQUAL){
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if((left.isConst() &&
+ right.getKind() == kind::ITE && isConstantIte(right)) ||
+ (right.isConst() &&
+ left.getKind() == kind::ITE && isConstantIte(left))){
+ TNode constant = left.isConst() ? left : right;
+ TNode cite = left.isConst() ? right : left;
+
+ std::pair<Node,Node> pair = make_pair(cite, constant);
+ NodePairMap::const_iterator eq_pos = d_constantIteEqualsConstantCache.find(pair);
+ if(eq_pos != d_constantIteEqualsConstantCache.end()){
+ Node ret = (*eq_pos).second;
+ if(ret.isConst()){
+ return ret;
+ }else{
+ return Node::null();
+ }
+ }
+
+ NodeVec* leaves = computeConstantLeaves(cite);
+ Assert(leaves != NULL);
+ if(!std::binary_search(leaves->begin(), leaves->end(), constant)){
+ std::pair<Node,Node> pair = make_pair(cite, constant);
+ d_constantIteEqualsConstantCache[pair] = d_false;
+ return d_false;
+ }
+ }
+ }
+ return Node::null();
+}
+
+Node ITESimplifier::attemptConstantRemoval(TNode atom){
+ if(atom.getKind() == kind::EQUAL){
+ TNode left = atom[0];
+ TNode right = atom[1];
+ if(isConstantIte(left) && isConstantIte(right)){
+ return intersectConstantIte(left, right);
+ }
+ }
+ return Node::null();
+}
+
+
+bool ITESimplifier::leavesAreConst(TNode e, TheoryId tid)
+{
+ Assert((e.getKind() == kind::ITE && !e.getType().isBoolean()) ||
+ Theory::theoryOf(e) != THEORY_BOOL);
+ if (e.isConst()) {
+ return true;
+ }
+
+ hash_map<Node, bool, NodeHashFunction>::iterator it;
+ it = d_leavesConstCache.find(e);
+ if (it != d_leavesConstCache.end()) {
+ return (*it).second;
+ }
+
+ if (!containsTermITE(e) && Theory::isLeafOf(e, tid)) {
+ d_leavesConstCache[e] = false;
+ return false;
+ }
+
+ Assert(e.getNumChildren() > 0);
+ size_t k = 0, sz = e.getNumChildren();
+
+ if (e.getKind() == kind::ITE) {
+ k = 1;
+ }
+
+ for (; k < sz; ++k) {
+ if (!leavesAreConst(e[k], tid)) {
+ d_leavesConstCache[e] = false;
+ return false;
+ }
+ }
+ d_leavesConstCache[e] = true;
+ return true;
+}
+
+
+Node ITESimplifier::simpConstants(TNode simpContext, TNode iteNode, TNode simpVar)
+{
+ NodePairMap::iterator it;
+ it = d_simpConstCache.find(pair<Node, Node>(simpContext,iteNode));
+ if (it != d_simpConstCache.end()) {
+ return (*it).second;
+ }
+
+ if (iteNode.getKind() == kind::ITE) {
+ NodeBuilder<> builder(kind::ITE);
+ builder << iteNode[0];
+ unsigned i = 1;
+ for (; i < iteNode.getNumChildren(); ++ i) {
+ Node n = simpConstants(simpContext, iteNode[i], simpVar);
+ if (n.isNull()) {
+ return n;
+ }
+ builder << n;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ result = Rewriter::rewrite(result);
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = result;
+ return result;
+ }
+
+ if (!containsTermITE(iteNode)) {
+ Node n = Rewriter::rewrite(simpContext.substitute(simpVar, iteNode));
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
+ return n;
+ }
+
+ Node iteNode2;
+ Node simpVar2;
+ d_simpContextCache.clear();
+ Node simpContext2 = createSimpContext(iteNode, iteNode2, simpVar2);
+ if (!simpContext2.isNull()) {
+ Assert(!iteNode2.isNull());
+ simpContext2 = simpContext.substitute(simpVar, simpContext2);
+ Node n = simpConstants(simpContext2, iteNode2, simpVar2);
+ if (n.isNull()) {
+ return n;
+ }
+ d_simpConstCache[pair<Node, Node>(simpContext, iteNode)] = n;
+ return n;
+ }
+ return Node();
+}
+
+
+Node ITESimplifier::getSimpVar(TypeNode t)
+{
+ std::hash_map<TypeNode, Node, TypeNode::HashFunction>::iterator it;
+ it = d_simpVars.find(t);
+ if (it != d_simpVars.end()) {
+ return (*it).second;
+ }
+ else {
+ Node var = NodeManager::currentNM()->mkSkolem("iteSimp_$$", t, "is a variable resulting from ITE simplification");
+ d_simpVars[t] = var;
+ return var;
+ }
+}
+
+
+Node ITESimplifier::createSimpContext(TNode c, Node& iteNode, Node& simpVar)
+{
+ NodeMap::iterator it;
+ it = d_simpContextCache.find(c);
+ if (it != d_simpContextCache.end()) {
+ return (*it).second;
+ }
+
+ if (!containsTermITE(c)) {
+ d_simpContextCache[c] = c;
+ return c;
+ }
+
+ if (c.getKind() == kind::ITE && !c.getType().isBoolean()) {
+ // Currently only support one ite node in a simp context
+ // Return Null if more than one is found
+ if (!iteNode.isNull()) {
+ return Node();
+ }
+ simpVar = getSimpVar(c.getType());
+ if (simpVar.isNull()) {
+ return Node();
+ }
+ d_simpContextCache[c] = simpVar;
+ iteNode = c;
+ return simpVar;
+ }
+
+ NodeBuilder<> builder(c.getKind());
+ if (c.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << c.getOperator();
+ }
+ unsigned i = 0;
+ for (; i < c.getNumChildren(); ++ i) {
+ Node newChild = createSimpContext(c[i], iteNode, simpVar);
+ if (newChild.isNull()) {
+ return newChild;
+ }
+ builder << newChild;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+ d_simpContextCache[c] = result;
+ return result;
+}
+typedef std::hash_set<Node, NodeHashFunction> NodeSet;
+void countReachable_(Node x, Kind k, NodeSet& visited, uint32_t& reached){
+ if(visited.find(x) != visited.end()){
+ return;
+ }
+ visited.insert(x);
+ if(x.getKind() == k){
+ ++reached;
+ }
+ for(unsigned i =0, N=x.getNumChildren(); i < N; ++i){
+ countReachable_(x[i], k, visited, reached);
+ }
+}
+
+uint32_t countReachable(TNode x, Kind k){
+ NodeSet visited;
+ uint32_t reached = 0;
+ countReachable_(x, k, visited, reached);
+ return reached;
+}
+
+Node ITESimplifier::simpITEAtom(TNode atom)
+{
+ static int CVC4_UNUSED instance = 0;
+ Debug("ite::atom") << "still simplifying " << (++instance) << endl;
+ Node attempt = transformAtom(atom);
+ Debug("ite::atom") << " finished " << instance << endl;
+ if(!attempt.isNull()){
+ Node rewritten = Rewriter::rewrite(attempt);
+ Debug("ite::print-success")
+ << instance << " "
+ << "rewriting " << countReachable(rewritten, kind::ITE)
+ << " from " << countReachable(atom, kind::ITE) << endl
+ << "\t rewritten " << rewritten << endl
+ << "\t input " << atom << endl;
+ return rewritten;
+ }
+
+ if (leavesAreConst(atom)) {
+ Node iteNode;
+ Node simpVar;
+ d_simpContextCache.clear();
+ Node simpContext = createSimpContext(atom, iteNode, simpVar);
+ if (!simpContext.isNull()) {
+ if (iteNode.isNull()) {
+ Assert(leavesAreConst(simpContext) && !containsTermITE(simpContext));
+ ++(d_statistics.d_unexpected);
+ Debug("ite::simpite") << instance << " "
+ << "how about?" << atom << endl;
+ Debug("ite::simpite") << instance << " "
+ << "\t" << simpContext << endl;
+ return Rewriter::rewrite(simpContext);
+ }
+ Node n = simpConstants(simpContext, iteNode, simpVar);
+ if (!n.isNull()) {
+ ++(d_statistics.d_unexpected);
+ Debug("ite::simpite") << instance << " "
+ << "here?" << atom << endl;
+ Debug("ite::simpite") << instance << " "
+ << "\t" << n << endl;
+ return n;
+ }
+ }
+ }
+ if(Debug.isOn("ite::simpite")){
+ if(countReachable(atom, kind::ITE) > 0){
+ Debug("ite::simpite") << instance << " "
+ << "remaining " << atom << endl;
+ }
+ }
+ ++(d_statistics.d_unsimplified);
+ return atom;
+}
+
+
+struct preprocess_stack_element {
+ TNode node;
+ bool children_added;
+ preprocess_stack_element(TNode node)
+ : node(node), children_added(false) {}
+};/* struct preprocess_stack_element */
+
+
+Node ITESimplifier::simpITE(TNode assertion)
+{
+ // Do a topological sort of the subexpressions and substitute them
+ vector<preprocess_stack_element> toVisit;
+ toVisit.push_back(assertion);
+
+ static int call = 0;
+ ++call;
+ int iteration = 0;
+
+ while (!toVisit.empty())
+ {
+ iteration ++;
+ //cout << "call " << call << " : " << iteration << endl;
+ // The current node we are processing
+ preprocess_stack_element& stackHead = toVisit.back();
+ TNode current = stackHead.node;
+
+ // If node has no ITE's or already in the cache we're done, pop from the stack
+ if (current.getNumChildren() == 0 ||
+ (Theory::theoryOf(current) != THEORY_BOOL && !containsTermITE(current))) {
+ d_simpITECache[current] = current;
+ ++(d_statistics.d_simpITEVisits);
+ toVisit.pop_back();
+ continue;
+ }
+
+ NodeMap::iterator find = d_simpITECache.find(current);
+ if (find != d_simpITECache.end()) {
+ toVisit.pop_back();
+ continue;
+ }
+
+ // Not yet substituted, so process
+ if (stackHead.children_added) {
+ // Children have been processed, so substitute
+ NodeBuilder<> builder(current.getKind());
+ if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << current.getOperator();
+ }
+ for (unsigned i = 0; i < current.getNumChildren(); ++ i) {
+ Assert(d_simpITECache.find(current[i]) != d_simpITECache.end());
+ Node child = current[i];
+ Node childRes = d_simpITECache[current[i]];
+ builder << childRes;
+ }
+ // Mark the substitution and continue
+ Node result = builder;
+
+ // If this is an atom, we process it
+ if (Theory::theoryOf(result) != THEORY_BOOL &&
+ result.getType().isBoolean()) {
+ result = simpITEAtom(result);
+ }
+
+ // if(current != result && result.isConst()){
+ // static int instance = 0;
+ // //cout << instance << " " << result << current << endl;
+ // }
+
+ result = Rewriter::rewrite(result);
+ d_simpITECache[current] = result;
+ ++(d_statistics.d_simpITEVisits);
+ toVisit.pop_back();
+ } else {
+ // Mark that we have added the children if any
+ if (current.getNumChildren() > 0) {
+ stackHead.children_added = true;
+ // We need to add the children
+ for(TNode::iterator child_it = current.begin(); child_it != current.end(); ++ child_it) {
+ TNode childNode = *child_it;
+ NodeMap::iterator childFind = d_simpITECache.find(childNode);
+ if (childFind == d_simpITECache.end()) {
+ toVisit.push_back(childNode);
+ }
+ }
+ } else {
+ // No children, so we're done
+ d_simpITECache[current] = current;
+ ++(d_statistics.d_simpITEVisits);
+ toVisit.pop_back();
+ }
+ }
+ }
+ return d_simpITECache[assertion];
+}
+
+ITECareSimplifier::ITECareSimplifier()
+ : d_usedSets()
+{
+ d_true = NodeManager::currentNM()->mkConst<bool>(true);
+ d_false = NodeManager::currentNM()->mkConst<bool>(false);
+}
+
+ITECareSimplifier::~ITECareSimplifier(){}
+
+void ITECareSimplifier::clear(){
+ d_usedSets.clear();
+}
+
+ITECareSimplifier::CareSetPtr ITECareSimplifier::getNewSet()
+{
+ if (d_usedSets.empty()) {
+ return ITECareSimplifier::CareSetPtr::mkNew(*this);
+ }
+ else {
+ ITECareSimplifier::CareSetPtr cs = ITECareSimplifier::CareSetPtr::recycle(d_usedSets.back());
+ cs.getCareSet().clear();
+ d_usedSets.pop_back();
+ return cs;
+ }
+}
+
+
+void ITECareSimplifier::updateQueue(CareMap& queue,
+ TNode e,
+ ITECareSimplifier::CareSetPtr& careSet)
+{
+ CareMap::iterator it = queue.find(e), iend = queue.end();
+ if (it != iend) {
+ set<Node>& cs2 = (*it).second.getCareSet();
+ ITECareSimplifier::CareSetPtr csNew = getNewSet();
+ set_intersection(careSet.getCareSet().begin(),
+ careSet.getCareSet().end(),
+ cs2.begin(), cs2.end(),
+ inserter(csNew.getCareSet(), csNew.getCareSet().begin()));
+ (*it).second = csNew;
+ }
+ else {
+ queue[e] = careSet;
+ }
+}
+
+
+Node ITECareSimplifier::substitute(TNode e, TNodeMap& substTable, TNodeMap& cache)
+{
+ TNodeMap::iterator it = cache.find(e), iend = cache.end();
+ if (it != iend) {
+ return it->second;
+ }
+
+ // do substitution?
+ it = substTable.find(e);
+ iend = substTable.end();
+ if (it != iend) {
+ Node result = substitute(it->second, substTable, cache);
+ cache[e] = result;
+ return result;
+ }
+
+ size_t sz = e.getNumChildren();
+ if (sz == 0) {
+ cache[e] = e;
+ return e;
+ }
+
+ NodeBuilder<> builder(e.getKind());
+ if (e.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ builder << e.getOperator();
+ }
+ for (unsigned i = 0; i < e.getNumChildren(); ++ i) {
+ builder << substitute(e[i], substTable, cache);
+ }
+
+ Node result = builder;
+ // it = substTable.find(result);
+ // if (it != iend) {
+ // result = substitute(it->second, substTable, cache);
+ // }
+ cache[e] = result;
+ return result;
+}
+
+
+Node ITECareSimplifier::simplifyWithCare(TNode e)
+{
+ TNodeMap substTable;
+ CareMap queue;
+ CareMap::iterator it;
+ ITECareSimplifier::CareSetPtr cs = getNewSet();
+ ITECareSimplifier::CareSetPtr cs2;
+ queue[e] = cs;
+
+ TNode v;
+ bool done;
+ unsigned i;
+
+ while (!queue.empty()) {
+ it = queue.end();
+ --it;
+ v = it->first;
+ cs = it->second;
+ set<Node>& css = cs.getCareSet();
+ queue.erase(v);
+
+ done = false;
+ set<Node>::iterator iCare, iCareEnd = css.end();
+
+ switch (v.getKind()) {
+ case kind::ITE: {
+ iCare = css.find(v[0]);
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = v[1];
+ updateQueue(queue, v[1], cs);
+ done = true;
+ break;
+ }
+ else {
+ iCare = css.find(v[0].negate());
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = v[2];
+ updateQueue(queue, v[2], cs);
+ done = true;
+ break;
+ }
+ }
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0]);
+ updateQueue(queue, v[1], cs2);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0].negate());
+ updateQueue(queue, v[2], cs2);
+ done = true;
+ break;
+ }
+ case kind::AND: {
+ for (i = 0; i < v.getNumChildren(); ++i) {
+ iCare = css.find(v[i].negate());
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = d_false;
+ done = true;
+ break;
+ }
+ }
+ if (done) break;
+
+ Assert(v.getNumChildren() > 1);
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0]);
+ for (i = 1; i < v.getNumChildren(); ++i) {
+ updateQueue(queue, v[i], cs2);
+ }
+ done = true;
+ break;
+ }
+ case kind::OR: {
+ for (i = 0; i < v.getNumChildren(); ++i) {
+ iCare = css.find(v[i]);
+ if (iCare != iCareEnd) {
+ Assert(substTable.find(v) == substTable.end());
+ substTable[v] = d_true;
+ done = true;
+ break;
+ }
+ }
+ if (done) break;
+
+ Assert(v.getNumChildren() > 1);
+ updateQueue(queue, v[0], cs);
+ cs2 = getNewSet();
+ cs2.getCareSet() = css;
+ cs2.getCareSet().insert(v[0].negate());
+ for (i = 1; i < v.getNumChildren(); ++i) {
+ updateQueue(queue, v[i], cs2);
+ }
+ done = true;
+ break;
+ }
+ default:
+ break;
+ }
+
+ if (done) {
+ continue;
+ }
+
+ for (unsigned i = 0; i < v.getNumChildren(); ++i) {
+ updateQueue(queue, v[i], cs);
+ }
+ }
+ while (!d_usedSets.empty()) {
+ delete d_usedSets.back();
+ d_usedSets.pop_back();
+ }
+
+ TNodeMap cache;
+ return substitute(e, substTable, cache);
+}
+
+
+} /* namespace theory */
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file ite_simplifier.h
+ ** \verbatim
+ ** Original author: Clark Barrett
+ ** Major contributors: none
+ ** Minor contributors (to current version): Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Simplifications for ITE expressions
+ **
+ ** This module implements preprocessing phases designed to simplify ITE
+ ** expressions. Based on:
+ ** Kim, Somenzi, Jin. Efficient Term-ITE Conversion for SMT. FMCAD 2009.
+ ** Burch, Jerry. Techniques for Verifying Superscalar Microprocessors. DAC '96
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__ITE_UTILITIES_H
+#define __CVC4__ITE_UTILITIES_H
+
+#include <vector>
+#include <ext/hash_map>
+#include <ext/hash_set>
+#include "expr/node.h"
+#include "util/statistics_registry.h"
+
+namespace CVC4 {
+namespace theory {
+
+class ContainsTermITEVistor;
+class IncomingArcCounter;
+class TermITEHeightCounter;
+class ITECompressor;
+class ITESimplifier;
+class ITECareSimplifier;
+
+class ITEUtilities {
+public:
+ ITEUtilities(ContainsTermITEVistor* containsVisitor);
+ ~ITEUtilities();
+
+ Node simpITE(TNode assertion);
+
+ bool simpIteDidALotOfWorkHeuristic() const;
+
+ /* returns false if an assertion is discovered to be equal to false. */
+ bool compress(std::vector<Node>& assertions);
+
+ Node simplifyWithCare(TNode e);
+
+ void clear();
+
+private:
+ ContainsTermITEVistor* d_containsVisitor;
+ ITECompressor* d_compressor;
+ ITESimplifier* d_simplifier;
+ ITECareSimplifier* d_careSimp;
+};
+
+/**
+ * A caching visitor that computes whether a node contains a term ite.
+ */
+class ContainsTermITEVistor {
+public:
+ ContainsTermITEVistor();
+ ~ContainsTermITEVistor();
+
+ /** returns true if a node contains a term ite. */
+ bool containsTermITE(TNode n);
+
+ /** Garbage collects the cache. */
+ void garbageCollect();
+
+ /** returns the size of the cache. */
+ size_t cache_size() const { return d_cache.size(); }
+
+private:
+ typedef std::hash_map<Node, bool, NodeHashFunction> NodeBoolMap;
+ NodeBoolMap d_cache;
+};
+
+class IncomingArcCounter {
+public:
+ IncomingArcCounter(bool skipVars = false, bool skipConstants = false);
+ ~IncomingArcCounter();
+ void computeReachability(const std::vector<Node>& assertions);
+
+ inline uint32_t lookupIncoming(Node n) const {
+ NodeCountMap::const_iterator it = d_reachCount.find(n);
+ if(it == d_reachCount.end()){
+ return 0;
+ }else{
+ return (*it).second;
+ }
+ }
+ void clear();
+private:
+ typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+ NodeCountMap d_reachCount;
+
+ bool d_skipVariables;
+ bool d_skipConstants;
+};
+
+class TermITEHeightCounter {
+public:
+ TermITEHeightCounter();
+ ~TermITEHeightCounter();
+
+ /**
+ * Compute and [potentially] cache the termITEHeight() of e.
+ * The term ite height equals the maximum number of term ites
+ * encountered on any path from e to a leaf.
+ * Inductively:
+ * - termITEHeight(leaves) = 0
+ * - termITEHeight(e: term-ite(c, t, e) ) =
+ * 1 + max(termITEHeight(t), termITEHeight(e)) ; Don't include c
+ * - termITEHeight(e not term ite) = max_{c in children(e)) (termITEHeight(c))
+ */
+ uint32_t termITEHeight(TNode e);
+
+ /** Clear the cache. */
+ void clear();
+
+ /** Size of the cache. */
+ size_t cache_size() const;
+
+private:
+ typedef std::hash_map<Node, uint32_t, NodeHashFunction> NodeCountMap;
+ NodeCountMap d_termITEHeight;
+};
+
+/**
+ * A routine designed to undo the potentially large blow up
+ * due to expansion caused by the ite simplifier.
+ */
+class ITECompressor {
+public:
+ ITECompressor(ContainsTermITEVistor* contains);
+ ~ITECompressor();
+
+ /* returns false if an assertion is discovered to be equal to false. */
+ bool compress(std::vector<Node>& assertions);
+
+ /* garbage Collects the compressor. */
+ void garbageCollect();
+
+private:
+
+ Node d_true; /* Copy of true. */
+ Node d_false; /* Copy of false. */
+ ContainsTermITEVistor* d_contains;
+ std::vector<Node>* d_assertions;
+ IncomingArcCounter d_incoming;
+
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ NodeMap d_compressed;
+
+ void reset();
+
+ Node push_back_boolean(Node original, Node compressed);
+ bool multipleParents(TNode c);
+ Node compressBooleanITEs(Node toCompress);
+ Node compressTerm(Node toCompress);
+ Node compressBoolean(Node toCompress);
+
+ class Statistics {
+ public:
+ IntStat d_compressCalls;
+ IntStat d_skolemsAdded;
+ Statistics();
+ ~Statistics();
+ };
+ Statistics d_statistics;
+};
+
+class ITESimplifier {
+public:
+ ITESimplifier(ContainsTermITEVistor* d_containsVisitor);
+ ~ITESimplifier();
+
+ Node simpITE(TNode assertion);
+
+ bool doneALotOfWorkHeuristic() const;
+ void clearSimpITECaches();
+
+private:
+ Node d_true;
+ Node d_false;
+
+ ContainsTermITEVistor* d_containsVisitor;
+ inline bool containsTermITE(TNode n) {
+ return d_containsVisitor->containsTermITE(n);
+ }
+ TermITEHeightCounter d_termITEHeight;
+ inline uint32_t termITEHeight(TNode e) {
+ return d_termITEHeight.termITEHeight(e);
+ }
+
+ // ConstantIte is a small inductive sublanguage:
+ // constant
+ // or termITE(cnd, ConstantIte, ConstantIte)
+ typedef std::vector<Node> NodeVec;
+ typedef std::hash_map<Node, NodeVec*, NodeHashFunction > ConstantLeavesMap;
+ ConstantLeavesMap d_constantLeaves;
+
+ // d_constantLeaves satisfies the following invariants:
+ // not containsTermITE(x) then !isKey(x)
+ // containsTermITE(x):
+ // - not isKey(x) then this value is uncomputed
+ // - d_constantLeaves[x] == NULL, then this contains a non-constant leaf
+ // - d_constantLeaves[x] != NULL, then this contains a sorted list of constant leaf
+ bool isConstantIte(TNode e);
+
+ /** If its not a constant and containsTermITE(ite),
+ * returns a sorted NodeVec of the leaves. */
+ NodeVec* computeConstantLeaves(TNode ite);
+
+ // Lists all of the vectors in d_constantLeaves for fast deletion.
+ std::vector<NodeVec*> d_allocatedConstantLeaves;
+
+
+ /* transforms */
+ Node transformAtom(TNode atom);
+ Node attemptConstantRemoval(TNode atom);
+ Node attemptLiftEquality(TNode atom);
+ Node attemptEagerRemoval(TNode atom);
+
+ // Given ConstantIte trees lcite and rcite,
+ // return a boolean expression equivalent to (= lcite rcite)
+ Node intersectConstantIte(TNode lcite, TNode rcite);
+
+ // Given ConstantIte tree cite and a constant c,
+ // return a boolean expression equivalent to (= lcite c)
+ Node constantIteEqualsConstant(TNode cite, TNode c);
+ uint32_t d_citeEqConstApplications;
+
+ typedef std::pair<Node, Node> NodePair;
+ struct NodePairHashFunction {
+ size_t operator () (const NodePair& pair) const {
+ size_t hash = 0;
+ hash = 0x9e3779b9 + NodeHashFunction().operator()(pair.first);
+ hash ^= 0x9e3779b9 + NodeHashFunction().operator()(pair.second) + (hash << 6) + (hash >> 2);
+ return hash;
+ }
+ };/* struct ITESimplifier::NodePairHashFunction */
+ typedef std::hash_map<NodePair, Node, NodePairHashFunction> NodePairMap;
+ NodePairMap d_constantIteEqualsConstantCache;
+ NodePairMap d_replaceOverCache;
+ NodePairMap d_replaceOverTermIteCache;
+ Node replaceOver(Node n, Node replaceWith, Node simpVar);
+ Node replaceOverTermIte(Node term, Node simpAtom, Node simpVar);
+
+ std::hash_map<Node, bool, NodeHashFunction> d_leavesConstCache;
+ bool leavesAreConst(TNode e, theory::TheoryId tid);
+ bool leavesAreConst(TNode e);
+
+ NodePairMap d_simpConstCache;
+ Node simpConstants(TNode simpContext, TNode iteNode, TNode simpVar);
+ std::hash_map<TypeNode, Node, TypeNode::HashFunction> d_simpVars;
+ Node getSimpVar(TypeNode t);
+
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ NodeMap d_simpContextCache;
+ Node createSimpContext(TNode c, Node& iteNode, Node& simpVar);
+
+ NodeMap d_simpITECache;
+ Node simpITEAtom(TNode atom);
+
+
+private:
+ class Statistics {
+ public:
+ IntStat d_maxNonConstantsFolded;
+ IntStat d_unexpected;
+ IntStat d_unsimplified;
+ IntStat d_exactMatchFold;
+ IntStat d_binaryPredFold;
+ IntStat d_specialEqualityFolds;
+ IntStat d_simpITEVisits;
+
+ HistogramStat<uint32_t> d_inSmaller;
+
+ Statistics();
+ ~Statistics();
+ };
+
+ Statistics d_statistics;
+};
+
+class ITECareSimplifier {
+public:
+ ITECareSimplifier();
+ ~ITECareSimplifier();
+
+ Node simplifyWithCare(TNode e);
+
+ void clear();
+private:
+ Node d_true;
+ Node d_false;
+
+ typedef std::hash_map<TNode, Node, TNodeHashFunction> TNodeMap;
+
+ class CareSetPtr;
+ class CareSetPtrVal {
+ friend class ITECareSimplifier::CareSetPtr;
+ ITECareSimplifier& d_iteSimplifier;
+ unsigned d_refCount;
+ std::set<Node> d_careSet;
+ CareSetPtrVal(ITECareSimplifier& simp) : d_iteSimplifier(simp), d_refCount(1) {}
+ };
+
+ std::vector<CareSetPtrVal*> d_usedSets;
+ void careSetPtrGC(CareSetPtrVal* val) {
+ d_usedSets.push_back(val);
+ }
+
+ class CareSetPtr {
+ CareSetPtrVal* d_val;
+ CareSetPtr(CareSetPtrVal* val) : d_val(val) {}
+ public:
+ CareSetPtr() : d_val(NULL) {}
+ CareSetPtr(const CareSetPtr& cs) {
+ d_val = cs.d_val;
+ if (d_val != NULL) {
+ ++(d_val->d_refCount);
+ }
+ }
+ ~CareSetPtr() {
+ if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
+ d_val->d_iteSimplifier.careSetPtrGC(d_val);
+ }
+ }
+ CareSetPtr& operator=(const CareSetPtr& cs) {
+ if (d_val != cs.d_val) {
+ if (d_val != NULL && (--(d_val->d_refCount) == 0)) {
+ d_val->d_iteSimplifier.careSetPtrGC(d_val);
+ }
+ d_val = cs.d_val;
+ if (d_val != NULL) {
+ ++(d_val->d_refCount);
+ }
+ }
+ return *this;
+ }
+ std::set<Node>& getCareSet() { return d_val->d_careSet; }
+ static CareSetPtr mkNew(ITECareSimplifier& simp) {
+ CareSetPtrVal* val = new CareSetPtrVal(simp);
+ return CareSetPtr(val);
+ }
+ static CareSetPtr recycle(CareSetPtrVal* val) {
+ Assert(val != NULL && val->d_refCount == 0);
+ val->d_refCount = 1;
+ return CareSetPtr(val);
+ }
+ };
+
+ CareSetPtr getNewSet();
+
+ typedef std::map<TNode, CareSetPtr> CareMap;
+ void updateQueue(CareMap& queue, TNode e, CareSetPtr& careSet);
+ Node substitute(TNode e, TNodeMap& substTable, TNodeMap& cache);
+};
+
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif
#include "theory/rep_set.h"
#include "theory/substitutions.h"
#include "theory/type_enumerator.h"
-#include "theory/ite_simplifier.h"
namespace CVC4 {
protected:
/** substitution map for this model */
SubstitutionMap d_substitutions;
- ITESimplifier d_iteSimp;
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
virtual ~TheoryModel(){}
#include "util/node_visitor.h"
#include "util/ite_removal.h"
+//#include "theory/ite_simplifier.h"
+//#include "theory/ite_compressor.h"
+#include "theory/ite_utilities.h"
+#include "theory/unconstrained_simplifier.h"
+
#include "theory/model.h"
#include "theory/quantifiers_engine.h"
#include "theory/quantifiers/theory_quantifiers.h"
d_factsAsserted(context, false),
d_preRegistrationVisitor(this, context),
d_sharedTermsVisitor(d_sharedTerms),
- d_unconstrainedSimp(context, logicInfo),
+ d_unconstrainedSimp(new UnconstrainedSimplifier(context, logicInfo)),
d_bvToBoolPreprocessor()
{
for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
StatisticsRegistry::registerStat(&d_combineTheoriesTime);
d_true = NodeManager::currentNM()->mkConst<bool>(true);
d_false = NodeManager::currentNM()->mkConst<bool>(false);
- PROOF (ProofManager::currentPM()->initTheoryProof(); );
+ PROOF (ProofManager::currentPM()->initTheoryProof(); );
+
+ d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
}
TheoryEngine::~TheoryEngine() {
delete d_masterEqualityEngine;
StatisticsRegistry::unregisterStat(&d_combineTheoriesTime);
+
+ delete d_unconstrainedSimp;
+
+ delete d_iteUtilities;
}
void TheoryEngine::interrupt() throw(ModalException) {
Node TheoryEngine::ppSimpITE(TNode assertion)
{
- Node result = d_iteSimplifier.simpITE(assertion);
- result = d_iteSimplifier.simplifyWithCare(Rewriter::rewrite(result));
- result = Rewriter::rewrite(result);
+ if(!d_iteRemover.containsTermITE(assertion)){
+ return assertion;
+ }else{
+
+ Node result = d_iteUtilities->simpITE(assertion);
+ Node res_rewritten = Rewriter::rewrite(result);
+
+ if(options::simplifyWithCareEnabled()){
+ Chat() << "starting simplifyWithCare()" << endl;
+ Node postSimpWithCare = d_iteUtilities->simplifyWithCare(res_rewritten);
+ Chat() << "ending simplifyWithCare()"
+ << " post simplifyWithCare()" << postSimpWithCare.getId() << endl;
+ result = Rewriter::rewrite(postSimpWithCare);
+ }else{
+ result = res_rewritten;
+ }
+
+ return result;
+ }
+}
+
+bool TheoryEngine::donePPSimpITE(std::vector<Node>& assertions){
+ bool result = true;
+ if(d_iteUtilities->simpIteDidALotOfWorkHeuristic()){
+ if(options::compressItes()){
+ result = d_iteUtilities->compress(assertions);
+ }
+
+ if(result){
+ // if false, don't bother to reclaim memory here.
+ NodeManager* nm = NodeManager::currentNM();
+ if(nm->poolSize() >= options::zombieHuntThreshold()){
+ Chat() << "..ite simplifier did quite a bit of work.. " << nm->poolSize() << endl;
+ Chat() << "....node manager contains " << nm->poolSize() << " nodes before cleanup" << endl;
+ d_iteUtilities->clear();
+ Rewriter::garbageCollect();
+ d_iteRemover.garbageCollect();
+ nm->reclaimZombiesUntil(options::zombieHuntThreshold());
+ Chat() << "....node manager contains " << nm->poolSize() << " nodes after cleanup" << endl;
+ }
+ }
+ }
return result;
}
void TheoryEngine::ppUnconstrainedSimp(vector<Node>& assertions)
{
- d_unconstrainedSimp.processAssertions(assertions);
+ d_unconstrainedSimp->processAssertions(assertions);
}
#include "options/options.h"
#include "smt/options.h"
#include "util/statistics_registry.h"
-#include "util/hash.h"
-#include "util/cache.h"
#include "util/cvc4_assert.h"
#include "util/sort_inference.h"
-#include "theory/ite_simplifier.h"
-#include "theory/unconstrained_simplifier.h"
#include "theory/uf/equality_engine.h"
#include "theory/bv/bv_to_bool.h"
#include "theory/atom_requests.h"
-
+/* Forward Declarations Block */
namespace theory {
class TheoryModel;
class TheoryEngineModelBuilder;
+ class ITEUtilities;
namespace eq {
class EqualityEngine;
}
}/* CVC4::theory namespace */
-
-
class DecisionEngine;
+class RemoveITE;
+class UnconstrainedSimplifier;
/**
* This is essentially an abstraction for a collection of theories. A
/** Dump the assertions to the dump */
void dumpAssertions(const char* tag);
- /** For preprocessing pass simplifying ITEs */
- theory::ITESimplifier d_iteSimplifier;
+ /**
+ * A collection of ite preprocessing passes.
+ */
+ theory::ITEUtilities* d_iteUtilities;
+
/** For preprocessing pass simplifying unconstrained expressions */
- UnconstrainedSimplifier d_unconstrainedSimp;
+ UnconstrainedSimplifier* d_unconstrainedSimp;
/** For preprocessing pass lifting bit-vectors of size 1 to booleans */
theory::bv::BvToBoolPreprocessor d_bvToBoolPreprocessor;
void ppBvToBool(const std::vector<Node>& assertions, std::vector<Node>& new_assertions);
Node ppSimpITE(TNode assertion);
+ /** Returns false if an assertion simplified to false. */
+ bool donePPSimpITE(std::vector<Node>& assertions);
+
void ppUnconstrainedSimp(std::vector<Node>& assertions);
SharedTermsDatabase* getSharedTermsDatabase() { return &d_sharedTerms; }
#include "theory/unconstrained_simplifier.h"
#include "theory/rewriter.h"
+#include "theory/logic_info.h"
using namespace std;
using namespace CVC4;
#include <utility>
#include "expr/node.h"
-#include "theory/theory.h"
#include "theory/substitutions.h"
+#include "util/statistics_registry.h"
namespace CVC4 {
+/* Forward Declarations */
+class LogicInfo;
+
class UnconstrainedSimplifier {
/** number of expressions eliminated due to unconstrained simplification */
boolean_simplification.cpp \
ite_removal.h \
ite_removal.cpp \
+ nary_builder.h \
+ nary_builder.cpp \
node_visitor.h \
chain.h \
index.h \
#include <vector>
#include "util/ite_removal.h"
-#include "theory/rewriter.h"
#include "expr/command.h"
#include "theory/quantifiers/options.h"
+#include "theory/ite_utilities.h"
using namespace CVC4;
using namespace std;
namespace CVC4 {
+RemoveITE::RemoveITE(context::UserContext* u)
+ : d_iteCache(u)
+{
+ d_containsVisitor = new theory::ContainsTermITEVistor();
+}
+
+RemoveITE::~RemoveITE(){
+ delete d_containsVisitor;
+}
+
+void RemoveITE::garbageCollect(){
+ d_containsVisitor->garbageCollect();
+}
+
+theory::ContainsTermITEVistor* RemoveITE::getContainsVisitor(){
+ return d_containsVisitor;
+}
+
+size_t RemoveITE::collectedCacheSizes() const{
+ return d_containsVisitor->cache_size() + d_iteCache.size();
+}
+
void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
{
for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
}
}
+bool RemoveITE::containsTermITE(TNode e){
+ return d_containsVisitor->containsTermITE(e);
+}
+
Node RemoveITE::run(TNode node, std::vector<Node>& output,
- IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar) {
+ IteSkolemMap& iteSkolemMap,
+ std::vector<Node>& quantVar) {
// Current node
Debug("ite") << "removeITEs(" << node << ")" << endl;
+ if(node.isVar() || node.isConst() ||
+ (options::biasedITERemoval() && !containsTermITE(node))){
+ return Node(node);
+ }
+
// The result may be cached already
NodeManager *nodeManager = NodeManager::currentNM();
- ITECache::iterator i = d_iteCache.find(node);
+ ITECache::const_iterator i = d_iteCache.find(node);
if(i != d_iteCache.end()) {
- Node cachedRewrite = (*i).second;
- Debug("ite") << "removeITEs: in-cache: " << cachedRewrite << endl;
- return cachedRewrite.isNull() ? Node(node) : cachedRewrite;
+ Node cached = (*i).second;
+ Debug("ite") << "removeITEs: in-cache: " << cached << endl;
+ return cached.isNull() ? Node(node) : cached;
}
// If an ITE replace it
Debug("ite") << "removeITEs(" << node << ") => " << newAssertion << endl;
// Attach the skolem
- d_iteCache[node] = skolem;
+ d_iteCache.insert(node, skolem);
// Remove ITEs from the new assertion, rewrite it and push it to the output
newAssertion = run(newAssertion, output, iteSkolemMap, quantVar);
// If changes, we rewrite
if(somethingChanged) {
- Node cachedRewrite = nodeManager->mkNode(node.getKind(), newChildren);
- d_iteCache[node] = cachedRewrite;
- return cachedRewrite;
+ Node cached = nodeManager->mkNode(node.getKind(), newChildren);
+ d_iteCache.insert(node, cached);
+ return cached;
} else {
- d_iteCache[node] = Node::null();
+ d_iteCache.insert(node, Node::null());
return node;
}
} else {
- d_iteCache[node] = Node::null();
+ d_iteCache.insert(node, Node::null());
return node;
}
}
+
}/* CVC4 namespace */
#include "expr/node.h"
#include "util/dump.h"
#include "context/context.h"
-#include "context/cdhashmap.h"
+#include "context/cdinsert_hashmap.h"
namespace CVC4 {
+namespace theory {
+class ContainsTermITEVistor;
+}
+
typedef std::hash_map<Node, unsigned, NodeHashFunction> IteSkolemMap;
class RemoveITE {
- typedef context::CDHashMap<Node, Node, NodeHashFunction> ITECache;
+ typedef context::CDInsertHashMap<Node, Node, NodeHashFunction> ITECache;
ITECache d_iteCache;
+
public:
- RemoveITE(context::UserContext* u) :
- d_iteCache(u) {
- }
+ RemoveITE(context::UserContext* u);
+ ~RemoveITE();
/**
* Removes the ITE nodes by introducing skolem variables. All
Node run(TNode node, std::vector<Node>& additionalAssertions,
IteSkolemMap& iteSkolemMap, std::vector<Node>& quantVar);
+ /** Returns true if e contains a term ite.*/
+ bool containsTermITE(TNode e);
+
+ /** Returns the collected size of the caches.*/
+ size_t collectedCacheSizes() const;
+
+ /** Garbage collects non-context dependent data-structures.*/
+ void garbageCollect();
+
+ /** Return the RemoveITE's containsVisitor.*/
+ theory::ContainsTermITEVistor* getContainsVisitor();
+
+private:
+ theory::ContainsTermITEVistor* d_containsVisitor;
+
};/* class RemoveTTE */
}/* CVC4 namespace */
--- /dev/null
+
+#include "util/nary_builder.h"
+#include "expr/metakind.h"
+using namespace std;
+
+namespace CVC4 {
+namespace util {
+
+Node NaryBuilder::mkAssoc(Kind kind, const std::vector<Node>& children){
+ if(children.size() == 0){
+ return zeroArity(kind);
+ }else if(children.size() == 1){
+ return children[0];
+ }else{
+ const unsigned int max = kind::metakind::getUpperBoundForKind(kind);
+ const unsigned int min = kind::metakind::getLowerBoundForKind(kind);
+
+ Assert(min <= children.size());
+
+ unsigned int numChildren = children.size();
+ NodeManager* nm = NodeManager::currentNM();
+ if( numChildren <= max ) {
+ return nm->mkNode(kind,children);
+ }
+
+ typedef std::vector<Node>::const_iterator const_iterator;
+ const_iterator it = children.begin() ;
+ const_iterator end = children.end() ;
+
+ /* The new top-level children and the children of each sub node */
+ std::vector<Node> newChildren;
+ std::vector<Node> subChildren;
+
+ while( it != end && numChildren > max ) {
+ /* Grab the next max children and make a node for them. */
+ for(const_iterator next = it + max; it != next; ++it, --numChildren ) {
+ subChildren.push_back(*it);
+ }
+ Node subNode = nm->mkNode(kind,subChildren);
+ newChildren.push_back(subNode);
+ subChildren.clear();
+ }
+
+ /* If there's children left, "top off" the Expr. */
+ if(numChildren > 0) {
+ /* If the leftovers are too few, just copy them into newChildren;
+ * otherwise make a new sub-node */
+ if(numChildren < min) {
+ for(; it != end; ++it) {
+ newChildren.push_back(*it);
+ }
+ } else {
+ for(; it != end; ++it) {
+ subChildren.push_back(*it);
+ }
+ Node subNode = nm->mkNode(kind, subChildren);
+ newChildren.push_back(subNode);
+ }
+ }
+
+ /* It's inconceivable we could have enough children for this to fail
+ * (more than 2^32, in most cases?). */
+ AlwaysAssert( newChildren.size() <= max,
+ "Too many new children in mkAssociative" );
+
+ /* It would be really weird if this happened (it would require
+ * min > 2, for one thing), but let's make sure. */
+ AlwaysAssert( newChildren.size() >= min,
+ "Too few new children in mkAssociative" );
+
+ return nm->mkNode(kind,newChildren);
+ }
+}
+
+Node NaryBuilder::zeroArity(Kind k){
+ using namespace kind;
+ NodeManager* nm = NodeManager::currentNM();
+ switch(k){
+ case AND:
+ return nm->mkConst(true);
+ case OR:
+ return nm->mkConst(false);
+ case PLUS:
+ return nm->mkConst(Rational(0));
+ case MULT:
+ return nm->mkConst(Rational(1));
+ default:
+ return Node::null();
+ }
+}
+
+
+RePairAssocCommutativeOperators::RePairAssocCommutativeOperators()
+ : d_cache()
+{}
+RePairAssocCommutativeOperators::~RePairAssocCommutativeOperators(){}
+size_t RePairAssocCommutativeOperators::size() const{ return d_cache.size(); }
+void RePairAssocCommutativeOperators::clear(){ d_cache.clear(); }
+
+bool RePairAssocCommutativeOperators::isAssociateCommutative(Kind k){
+ using namespace kind;
+ switch(k){
+ case BITVECTOR_CONCAT:
+ case BITVECTOR_AND:
+ case BITVECTOR_OR:
+ case BITVECTOR_XOR:
+ case BITVECTOR_MULT:
+ case BITVECTOR_PLUS:
+ case DISTINCT:
+ case PLUS:
+ case MULT:
+ case AND:
+ case OR:
+ return true;
+ default:
+ return false;
+ }
+}
+
+Node RePairAssocCommutativeOperators::rePairAssocCommutativeOperators(TNode n){
+ if(d_cache.find(n) != d_cache.end()){
+ return d_cache[n];
+ }
+ Node result =
+ isAssociateCommutative(n.getKind()) ?
+ case_assoccomm(n) : case_other(n);
+
+ d_cache[n] = result;
+ return result;
+}
+
+Node RePairAssocCommutativeOperators::case_assoccomm(TNode n){
+ Kind k = n.getKind();
+ Assert(isAssociateCommutative(k));
+ Assert(n.getMetaKind() != kind::metakind::PARAMETERIZED);
+ unsigned N = n.getNumChildren();
+ Assert(N >= 2);
+
+
+ Node last = rePairAssocCommutativeOperators( n[N-1]);
+ Node nextToLast = rePairAssocCommutativeOperators(n[N-2]);
+
+ NodeManager* nm = NodeManager::currentNM();
+ Node last2 = nm->mkNode(k, nextToLast, last);
+
+ if(N <= 2){
+ return last2;
+ } else{
+ Assert(N > 2);
+ Node prevRound = last2;
+ for(unsigned prevPos = N-2; prevPos > 0; --prevPos){
+ unsigned currPos = prevPos-1;
+ Node curr = rePairAssocCommutativeOperators(n[currPos]);
+ Node round = nm->mkNode(k, curr, prevRound);
+ prevRound = round;
+ }
+ return prevRound;
+ }
+}
+
+Node RePairAssocCommutativeOperators::case_other(TNode n){
+ if(n.isConst() || n.isVar()){
+ return n;
+ }
+
+ NodeBuilder<> nb(n.getKind());
+
+ if(n.getMetaKind() == kind::metakind::PARAMETERIZED) {
+ nb << n.getOperator();
+ }
+
+ // Remove the ITEs from the children
+ for(TNode::const_iterator i = n.begin(), end = n.end(); i != end; ++i) {
+ Node newChild = rePairAssocCommutativeOperators(*i);
+ nb << newChild;
+ }
+
+ Node result = (Node)nb;
+ return result;
+}
+
+}/* util namespace */
+}/* CVC4 namespace */
--- /dev/null
+
+#include "cvc4_private.h"
+
+#pragma once
+
+#include <vector>
+#include "expr/node.h"
+
+namespace CVC4{
+namespace util {
+
+class NaryBuilder {
+public:
+ static Node mkAssoc(Kind k, const std::vector<Node>& children);
+ static Node zeroArity(Kind k);
+};/* class NaryBuilder */
+
+class RePairAssocCommutativeOperators {
+public:
+ RePairAssocCommutativeOperators();
+ ~RePairAssocCommutativeOperators();
+
+ Node rePairAssocCommutativeOperators(TNode n);
+
+ static bool isAssociateCommutative(Kind k);
+
+ size_t size() const;
+ void clear();
+private:
+ Node case_assoccomm(TNode n);
+ Node case_other(TNode n);
+
+ typedef std::hash_map<Node, Node, NodeHashFunction> NodeMap;
+ NodeMap d_cache;
+};/* class RePairAssocCommutativeOperators */
+
+}/* util namespace */
+}/* CVC4 namespace */
miplib2.cvc \
miplib3.cvc \
miplib4.cvc \
- miplibtrick.smt
+ miplibtrick.smt \
+ prp-13-24.smt2
# problem__003.smt2
EXTRA_DIST = $(TESTS) \
--- /dev/null
+(set-logic QF_LIA)
+(set-info :source |http://www.nec-labs.com/~fsoft/bench.html
+ The following changes have been made:
+ The logic is changed to QF_LIA.
+ The category is set as industrial.
+ The status (except 'large' cases) is assigned according to the 'outfile' on http://www.nec-labs.com/~fsoft/bench.html. |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun i1430 () Int)
+(declare-fun i1446 () Int)
+(declare-fun i1474 () Int)
+(declare-fun i1531 () Int)
+(declare-fun i1589 () Int)
+(declare-fun i1651 () Int)
+(declare-fun i1727 () Int)
+(declare-fun i1495 () Int)
+(declare-fun i1874 () Int)
+(declare-fun i2029 () Int)
+(declare-fun i2201 () Int)
+(declare-fun i2370 () Int)
+(declare-fun i2560 () Int)
+(declare-fun i1652 () Int)
+(declare-fun i1875 () Int)
+(declare-fun i1140 () Int)
+(declare-fun i2747 () Int)
+(declare-fun i2954 () Int)
+(declare-fun i2030 () Int)
+(declare-fun i2371 () Int)
+(declare-fun i1728 () Int)
+(declare-fun i2202 () Int)
+(declare-fun i2561 () Int)
+(declare-fun i2748 () Int)
+(declare-fun i2955 () Int)
+(declare-fun i3166 () Int)
+(declare-fun i3389 () Int)
+(declare-fun i3390 () Int)
+(declare-fun i3642 () Int)
+(declare-fun i3643 () Int)
+(declare-fun i3915 () Int)
+(declare-fun i3167 () Int)
+(declare-fun i3916 () Int)
+(declare-fun i4203 () Int)
+(declare-fun i4204 () Int)
+(assert (let ((?v_3 (+ 0 0))) (let ((?v_260 (= i1651 ?v_3)) (?v_261 (= i1874 ?v_3)) (?v_262 (= i2029 ?v_3)) (?v_263 (= i2201 ?v_3)) (?v_264 (= i2370 ?v_3)) (?v_265 (= i2560 ?v_3)) (?v_349 (= i2747 ?v_3)) (?v_413 (= i3166 ?v_3)) (?v_469 (= i3389 ?v_3)) (?v_561 (= i3642 ?v_3)) (?v_655 (= i3915 ?v_3)) (?v_751 (= i4203 ?v_3)) (?v_0 (not (= i1430 ?v_3)))) (let ((?v_1 (ite ?v_0 5 (ite ?v_0 3 41))) (?v_8 (+ 41 0))) (let ((?v_6 (= ?v_1 ?v_8)) (?v_2 (= ?v_1 (+ 5 0)))) (let ((?v_12 (ite (not ?v_6) 0 i1446)) (?v_4 (= (ite (not ?v_2) 0 i1446) ?v_3))) (let ((?v_7 (= ?v_12 ?v_3)) (?v_5 (ite ?v_2 7 (ite ?v_6 43 ?v_1))) (?v_10 (+ 43 0))) (let ((?v_9 (ite (= ?v_5 (+ 7 0)) (ite (not ?v_4) 8 (ite ?v_4 41 ?v_5)) (ite (not (= ?v_5 ?v_10)) ?v_5 (ite (not ?v_7) 46 (ite ?v_7 122 ?v_5))))) (?v_22 (+ 122 0))) (let ((?v_18 (= ?v_9 ?v_22)) (?v_20 (+ 46 0))) (let ((?v_16 (= ?v_9 ?v_20)) (?v_15 (= ?v_9 (+ 8 0))) (?v_11 (= ?v_9 ?v_8))) (let ((?v_59 (ite (not ?v_11) ?v_12 i1474)) (?v_31 (ite (not ?v_18) 0 i1474))) (let ((?v_13 (= ?v_59 ?v_3)) (?v_26 (ite ?v_15 i1474 (ite (not ?v_16) 0 i1474))) (?v_19 (= ?v_31 ?v_3))) (let ((?v_17 (<= 4 (+ ?v_26 0))) (?v_14 (ite ?v_11 43 (ite ?v_15 10 (ite ?v_16 48 (ite ?v_18 124 ?v_9))))) (?v_29 (+ 124 0)) (?v_24 (+ 48 0))) (let ((?v_75 (= ?v_14 (+ 10 0))) (?v_23 (not ?v_17))) (let ((?v_21 (ite (= ?v_14 ?v_10) (ite (not ?v_13) 46 (ite ?v_13 122 ?v_14)) (ite ?v_75 16 (ite (= ?v_14 ?v_24) (ite ?v_23 50 (ite ?v_17 122 ?v_14)) (ite (not (= ?v_14 ?v_29)) ?v_14 (ite (not ?v_19) 125 (ite ?v_19 205 ?v_14))))))) (?v_39 (+ 205 0))) (let ((?v_35 (= ?v_21 ?v_39)) (?v_38 (+ 125 0))) (let ((?v_40 (= ?v_21 ?v_38)) (?v_37 (+ 50 0))) (let ((?v_33 (= ?v_21 ?v_37)) (?v_30 (= ?v_21 ?v_22)) (?v_25 (= ?v_21 ?v_20))) (let ((?v_96 (ite (not ?v_25) ?v_26 i1531)) (?v_45 (ite (not ?v_30) ?v_31 i1531)) (?v_49 (ite (not ?v_33) 0 i1531)) (?v_54 (ite (not ?v_35) 0 i1531)) (?v_307 (not ?v_40))) (let ((?v_27 (<= 4 (+ ?v_96 0))) (?v_32 (= ?v_45 ?v_3)) (?v_34 (= ?v_49 ?v_3)) (?v_28 (ite ?v_25 48 (ite ?v_30 124 (ite (= ?v_21 (+ 16 0)) (ite ?v_17 18 (ite ?v_23 27 ?v_21)) (ite ?v_33 52 (ite ?v_40 126 (ite ?v_35 207 ?v_21))))))) (?v_52 (+ 207 0)) (?v_51 (+ 126 0))) (let ((?v_41 (= ?v_28 ?v_51)) (?v_47 (+ 52 0)) (?v_55 (= ?v_28 (+ 18 0)))) (let ((?v_300 (not ?v_41))) (let ((?v_71 (ite ?v_300 0 i1589)) (?v_36 (ite (= ?v_28 ?v_24) (ite (not ?v_27) 50 (ite ?v_27 122 ?v_28)) (ite (= ?v_28 ?v_29) (ite (not ?v_32) 125 (ite ?v_32 205 ?v_28)) (ite ?v_55 19 (ite (= ?v_28 (+ 27 0)) 29 (ite (= ?v_28 ?v_47) (ite (not ?v_34) 53 (ite ?v_34 89 ?v_28)) (ite ?v_41 128 (ite (not (= ?v_28 ?v_52)) ?v_28 (ite (not (= ?v_54 ?v_3)) 208 ?v_28))))))))) (?v_73 (+ 208 0))) (let ((?v_82 (= ?v_36 ?v_73)) (?v_67 (+ 128 0)) (?v_66 (+ 89 0))) (let ((?v_209 (= ?v_36 ?v_66)) (?v_65 (+ 53 0))) (let ((?v_77 (= ?v_36 ?v_65)) (?v_86 (+ 29 0)) (?v_56 (= ?v_36 (+ 19 0))) (?v_53 (= ?v_36 ?v_39)) (?v_68 (= ?v_36 ?v_38)) (?v_48 (= ?v_36 ?v_37)) (?v_44 (= ?v_36 ?v_22))) (let ((?v_99 (ite (not ?v_44) ?v_45 i1651)) (?v_155 (ite (not ?v_48) ?v_49 i1651)) (?v_64 (ite (not ?v_53) ?v_54 i1651)) (?v_306 (not ?v_68)) (?v_537 (not ?v_77)) (?v_221 (not ?v_82))) (let ((?v_129 (ite ?v_221 0 i1651)) (?v_289 (not ?v_209))) (let ((?v_291 (ite ?v_289 0 i1652)) (?v_46 (= ?v_99 ?v_3)) (?v_50 (= ?v_155 ?v_3)) (?v_93 (+ 210 0)) (?v_92 (+ 203 0)) (?v_91 (+ 130 0)) (?v_90 (+ 90 0)) (?v_89 (+ 54 0)) (?v_113 (+ 35 0)) (?v_126 (+ 219 0)) (?v_122 (+ 132 0)) (?v_121 (+ 91 0)) (?v_114 (+ 56 0)) (?v_146 (+ 223 0)) (?v_145 (+ 201 0)) (?v_144 (+ 133 0)) (?v_143 (+ 473 0)) (?v_142 (+ 57 0)) (?v_173 (+ 225 0)) (?v_169 (+ 135 0)) (?v_168 (+ 92 0)) (?v_167 (+ 58 0)) (?v_204 (+ 263 0)) (?v_203 (+ 227 0)) (?v_202 (+ 170 0)) (?v_201 (+ 138 0)) (?v_200 (+ 93 0)) (?v_199 (+ 449 0)) (?v_253 (+ 265 0)) (?v_249 (+ 229 0)) (?v_248 (+ 171 0)) (?v_247 (+ 139 0)) (?v_244 (+ 95 0)) (?v_243 (+ 59 0)) (?v_353 (+ 344 0)) (?v_351 (+ 500 0)) (?v_347 (+ 584 0)) (?v_346 (+ 172 0)) (?v_345 (+ 629 0)) (?v_257 (+ 115 0)) (?v_328 (+ 97 0)) (?v_327 (+ 60 0)) (?v_390 (+ 1 0)) (?v_418 (+ 346 0)) (?v_355 (+ 498 0)) (?v_416 (+ 501 0)) (?v_354 (+ 582 0)) (?v_411 (+ 585 0)) (?v_410 (+ 453 0)) (?v_409 (+ 140 0)) (?v_408 (+ 98 0)) (?v_407 (+ 62 0)) (?v_483 (+ 347 0)) (?v_425 (+ 267 0)) (?v_424 (+ 499 0)) (?v_423 (+ 230 0)) (?v_422 (+ 583 0)) (?v_479 (+ 173 0)) (?v_478 (+ 141 0)) (?v_477 (+ 545 0)) (?v_421 (+ 85 0)) (?v_474 (+ 64 0)) (?v_575 (+ 348 0)) (?v_485 (+ 268 0)) (?v_484 (+ 232 0)) (?v_574 (+ 174 0)) (?v_571 (+ 143 0)) (?v_570 (+ 99 0)) (?v_569 (+ 66 0)) (?v_676 (+ 350 0)) (?v_579 (+ 270 0)) (?v_577 (+ 234 0)) (?v_668 (+ 176 0)) (?v_576 (+ 166 0)) (?v_665 (+ 145 0)) (?v_664 (+ 100 0)) (?v_663 (+ 605 0)) (?v_778 (+ 352 0)) (?v_686 (+ 272 0)) (?v_684 (+ 238 0)) (?v_683 (+ 240 0)) (?v_682 (+ 199 0)) (?v_774 (+ 178 0)) (?v_773 (+ 147 0)) (?v_771 (+ 102 0)) (?v_770 (+ 67 0)) (?v_781 (+ 274 0)) (?v_780 (+ 249 0)) (?v_779 (+ 241 0)) (?v_69 (ite ?v_307 0 (* (- 1) i1531)))) (let ((?v_42 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_69) ?v_71) 0)))) (let ((?v_43 (ite ?v_44 124 (ite ?v_48 52 (ite ?v_68 126 (ite ?v_53 207 (ite ?v_56 21 (ite (= ?v_36 ?v_86) 41 (ite ?v_77 54 (ite ?v_209 90 (ite (= ?v_36 ?v_67) (ite ?v_42 130 (ite (not ?v_42) 203 ?v_36)) (ite ?v_82 210 ?v_36)))))))))))) (let ((?v_58 (= ?v_43 ?v_8)) (?v_70 (= ?v_43 ?v_51)) (?v_301 (* (- 1) i1589))) (let ((?v_57 (= (- 1) (+ (+ 0 (+ 0 (- 1) (ite (not ?v_55) 0 ?v_301)) (ite (not ?v_56) 0 i1651)) 0))) (?v_62 (= ?v_43 ?v_113)) (?v_79 (= ?v_43 ?v_89)) (?v_208 (= ?v_43 ?v_90)) (?v_74 (= ?v_43 ?v_91)) (?v_63 (= ?v_43 ?v_92)) (?v_371 (= ?v_43 ?v_93))) (let ((?v_61 (ite ?v_58 43 (ite (= ?v_43 ?v_29) (ite (not ?v_46) 125 (ite ?v_46 205 ?v_43)) (ite (= ?v_43 ?v_47) (ite (not ?v_50) 53 (ite ?v_50 89 ?v_43)) (ite ?v_70 128 (ite (= ?v_43 ?v_52) (ite (not (= ?v_64 ?v_3)) 208 ?v_43) (ite (= ?v_43 (+ 21 0)) (ite ?v_57 23 (ite (not ?v_57) 26 ?v_43)) (ite ?v_62 207 (ite ?v_79 56 (ite ?v_208 91 (ite ?v_74 132 (ite ?v_63 207 (ite ?v_371 219 ?v_43))))))))))))) (?v_136 (ite (not ?v_58) ?v_59 i1727))) (let ((?v_60 (= ?v_136 ?v_3)) (?v_108 (= ?v_61 ?v_38)) (?v_84 (= ?v_61 ?v_39)) (?v_85 (ite ?v_62 i1727 (ite (not ?v_63) ?v_64 i1727))) (?v_115 (= ?v_61 ?v_65)) (?v_210 (= ?v_61 ?v_66)) (?v_78 (* (- 1) i1651))) (let ((?v_109 (ite ?v_306 ?v_69 ?v_78)) (?v_299 (not ?v_70))) (let ((?v_111 (ite ?v_299 ?v_71 i1727))) (let ((?v_72 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_109) ?v_111) 0))) (?v_128 (= ?v_61 ?v_73)) (?v_124 (ite (not ?v_74) (ite (not ?v_75) 0 i1495) i1727))) (let ((?v_76 (<= 4 (+ ?v_124 0)))) (let ((?v_81 (not ?v_76)) (?v_87 (= ?v_61 (+ 26 0))) (?v_116 (ite ?v_537 0 ?v_78)) (?v_528 (not ?v_79))) (let ((?v_119 (ite ?v_528 0 i1727))) (let ((?v_80 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_116) ?v_119) 0))) (?v_213 (= ?v_61 ?v_121))) (let ((?v_83 (ite (= ?v_61 ?v_10) (ite (not ?v_60) 46 (ite ?v_60 122 ?v_61)) (ite ?v_108 126 (ite ?v_84 207 (ite (= ?v_61 ?v_52) (ite (not (= ?v_85 ?v_3)) 208 ?v_61) (ite ?v_115 54 (ite ?v_210 90 (ite (= ?v_61 ?v_67) (ite ?v_72 130 (ite (not ?v_72) 203 ?v_61)) (ite ?v_128 210 (ite (= ?v_61 (+ 23 0)) (ite ?v_76 24 (ite ?v_81 25 ?v_61)) (ite ?v_87 29 (ite (= ?v_61 ?v_114) (ite ?v_80 57 (ite (not ?v_80) 89 ?v_61)) (ite ?v_213 473 (ite (= ?v_61 ?v_122) (ite ?v_81 133 (ite ?v_76 201 ?v_61)) (ite (not (= ?v_61 ?v_126)) ?v_61 (ite (not (<= ?v_129 ?v_3)) 223 ?v_61))))))))))))))))) (let ((?v_95 (= ?v_83 ?v_20)) (?v_98 (= ?v_83 ?v_22)) (?v_110 (= ?v_83 ?v_51)) (?v_103 (ite (not ?v_84) ?v_85 i1874)) (?v_106 (ite (not ?v_87) 0 1))) (let ((?v_88 (= ?v_106 ?v_3)) (?v_294 (= ?v_83 ?v_66)) (?v_127 (= ?v_83 ?v_73)) (?v_118 (= ?v_83 ?v_89)) (?v_207 (= ?v_83 ?v_90)) (?v_123 (= ?v_83 ?v_91)) (?v_101 (= ?v_83 ?v_92)) (?v_370 (= ?v_83 ?v_93)) (?v_104 (= ?v_83 (+ 24 0))) (?v_105 (= ?v_83 (+ 25 0))) (?v_359 (= ?v_83 ?v_142)) (?v_130 (= ?v_83 ?v_144)) (?v_102 (= ?v_83 ?v_145)) (?v_132 (= ?v_83 ?v_146))) (let ((?v_94 (ite ?v_95 48 (ite ?v_98 124 (ite ?v_110 128 (ite (= ?v_83 ?v_52) (ite (not (= ?v_103 ?v_3)) 208 ?v_83) (ite (= ?v_83 ?v_86) (ite (not ?v_88) 35 (ite ?v_88 41 ?v_83)) (ite ?v_294 90 (ite ?v_127 210 (ite ?v_118 56 (ite ?v_207 91 (ite ?v_123 132 (ite ?v_101 207 (ite ?v_370 219 (ite ?v_104 29 (ite ?v_105 29 (ite ?v_359 58 (ite (= ?v_83 ?v_143) 92 (ite ?v_130 135 (ite ?v_102 207 (ite ?v_132 225 ?v_83))))))))))))))))))))) (let ((?v_135 (= ?v_94 ?v_8)) (?v_177 (ite (not ?v_95) ?v_96 i2029))) (let ((?v_97 (<= 4 (+ ?v_177 0))) (?v_152 (ite (not ?v_98) ?v_99 i2029))) (let ((?v_100 (= ?v_152 ?v_3)) (?v_139 (ite ?v_101 i2029 (ite (not ?v_102) ?v_103 i2029))) (?v_107 (= (ite ?v_104 1 (ite ?v_105 0 ?v_106)) ?v_3)) (?v_305 (not ?v_108)) (?v_117 (* (- 1) i1874))) (let ((?v_190 (ite ?v_305 ?v_109 ?v_117)) (?v_298 (not ?v_110))) (let ((?v_192 (ite ?v_298 ?v_111 i2029))) (let ((?v_112 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_190) ?v_192) 0))) (?v_140 (= ?v_94 ?v_73)) (?v_138 (= ?v_94 ?v_113)) (?v_292 (= ?v_94 ?v_90)) (?v_369 (= ?v_94 ?v_93)) (?v_536 (not ?v_115))) (let ((?v_310 (ite ?v_536 ?v_116 ?v_117)) (?v_527 (not ?v_118))) (let ((?v_312 (ite ?v_527 ?v_119 i2029))) (let ((?v_120 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_310) ?v_312) 0))) (?v_212 (= ?v_94 ?v_121)) (?v_163 (ite (not ?v_123) ?v_124 i2029))) (let ((?v_125 (<= 4 (+ ?v_163 0))) (?v_219 (not ?v_127)) (?v_220 (not ?v_128))) (let ((?v_141 (ite ?v_219 (ite ?v_220 ?v_129 i1874) i2029)) (?v_363 (= ?v_94 ?v_167)) (?v_206 (= ?v_94 ?v_168)) (?v_171 (ite (not ?v_130) 0 i2029))) (let ((?v_131 (= ?v_171 ?v_3)) (?v_175 (ite (not ?v_132) 0 i2029))) (let ((?v_133 (= ?v_175 ?v_3))) (let ((?v_134 (ite ?v_135 43 (ite (= ?v_94 ?v_24) (ite (not ?v_97) 50 (ite ?v_97 122 ?v_94)) (ite (= ?v_94 ?v_29) (ite (not ?v_100) 125 (ite ?v_100 205 ?v_94)) (ite (= ?v_94 ?v_52) (ite (not (= ?v_139 ?v_3)) 208 ?v_94) (ite (= ?v_94 ?v_86) (ite (not ?v_107) 35 (ite ?v_107 41 ?v_94)) (ite (= ?v_94 ?v_67) (ite ?v_112 130 (ite (not ?v_112) 203 ?v_94)) (ite ?v_140 210 (ite ?v_138 207 (ite ?v_292 91 (ite ?v_369 219 (ite (= ?v_94 ?v_114) (ite ?v_120 57 (ite (not ?v_120) 89 ?v_94)) (ite ?v_212 473 (ite (= ?v_94 ?v_122) (ite (not ?v_125) 133 (ite ?v_125 201 ?v_94)) (ite (= ?v_94 ?v_126) (ite (not (<= ?v_141 ?v_3)) 223 ?v_94) (ite ?v_363 449 (ite ?v_206 93 (ite (= ?v_94 ?v_169) (ite (not ?v_131) 138 (ite ?v_131 170 ?v_94)) (ite (not (= ?v_94 ?v_173)) ?v_94 (ite (not ?v_133) 227 (ite ?v_133 263 ?v_94)))))))))))))))))))))) (let ((?v_147 (= ?v_134 ?v_8)) (?v_148 (ite (not ?v_135) ?v_136 i2201))) (let ((?v_137 (= ?v_148 ?v_3)) (?v_151 (= ?v_134 ?v_22)) (?v_154 (= ?v_134 ?v_37)) (?v_189 (= ?v_134 ?v_38)) (?v_157 (= ?v_134 ?v_39)) (?v_161 (ite (not ?v_138) ?v_139 i2201)) (?v_340 (= ?v_134 ?v_66)) (?v_165 (= ?v_134 ?v_73)) (?v_158 (= ?v_134 ?v_113)) (?v_162 (= ?v_134 ?v_91)) (?v_159 (= ?v_134 ?v_92)) (?v_368 (= ?v_134 ?v_93)) (?v_282 (= ?v_134 ?v_121)) (?v_218 (not ?v_140))) (let ((?v_166 (ite ?v_218 ?v_141 i2201)) (?v_358 (= ?v_134 ?v_142)) (?v_170 (= ?v_134 ?v_144)) (?v_160 (= ?v_134 ?v_145)) (?v_174 (= ?v_134 ?v_146)) (?v_205 (= ?v_134 ?v_200)) (?v_491 (= ?v_134 ?v_201)) (?v_588 (= ?v_134 ?v_202)) (?v_179 (= ?v_134 ?v_203)) (?v_181 (= ?v_134 ?v_204))) (let ((?v_150 (ite ?v_147 43 (ite (= ?v_134 ?v_10) (ite (not ?v_137) 46 (ite ?v_137 122 ?v_134)) (ite ?v_151 124 (ite ?v_154 52 (ite ?v_189 126 (ite ?v_157 207 (ite (= ?v_134 ?v_52) (ite (not (= ?v_161 ?v_3)) 208 ?v_134) (ite ?v_340 90 (ite ?v_165 210 (ite ?v_158 207 (ite ?v_162 132 (ite ?v_159 207 (ite ?v_368 219 (ite ?v_282 473 (ite (= ?v_134 ?v_126) (ite (not (<= ?v_166 ?v_3)) 223 ?v_134) (ite ?v_358 58 (ite (= ?v_134 ?v_143) 92 (ite ?v_170 135 (ite ?v_160 207 (ite ?v_174 225 (ite (= ?v_134 ?v_199) 59 (ite ?v_205 95 (ite ?v_491 139 (ite ?v_588 171 (ite ?v_179 229 (ite ?v_181 265 ?v_134))))))))))))))))))))))))))) (?v_149 (= (ite (not ?v_147) ?v_148 i2370) ?v_3))) (let ((?v_184 (= ?v_150 ?v_20)) (?v_186 (= ?v_150 ?v_22)) (?v_187 (ite (not ?v_151) ?v_152 i2370))) (let ((?v_153 (= ?v_187 ?v_3)) (?v_275 (ite (not ?v_154) ?v_155 i2370))) (let ((?v_156 (= ?v_275 ?v_3)) (?v_191 (= ?v_150 ?v_51)) (?v_234 (ite ?v_157 i2370 (ite ?v_158 i2370 (ite ?v_159 i2370 (ite (not ?v_160) ?v_161 i2370))))) (?v_194 (= ?v_150 ?v_73)) (?v_338 (= ?v_150 ?v_90)) (?v_367 (= ?v_150 ?v_93)) (?v_315 (ite (not ?v_162) ?v_163 i2370))) (let ((?v_164 (<= 4 (+ ?v_315 0))) (?v_217 (not ?v_165))) (let ((?v_195 (ite ?v_217 ?v_166 i2370)) (?v_196 (= ?v_150 ?v_146)) (?v_362 (= ?v_150 ?v_167)) (?v_285 (= ?v_150 ?v_168)) (?v_238 (ite (not ?v_170) ?v_171 i2370))) (let ((?v_172 (= ?v_238 ?v_3)) (?v_197 (ite (not ?v_174) ?v_175 i2370))) (let ((?v_176 (= ?v_197 ?v_3)) (?v_357 (= ?v_150 ?v_243)) (?v_178 (<= ?v_177 ?v_3)) (?v_488 (= ?v_150 ?v_247)) (?v_593 (= ?v_150 ?v_248)) (?v_251 (ite (not ?v_179) 0 i2370))) (let ((?v_180 (= ?v_251 ?v_3)) (?v_255 (ite (not ?v_181) 0 i2370))) (let ((?v_182 (= ?v_255 ?v_3))) (let ((?v_183 (ite (= ?v_150 ?v_10) (ite (not ?v_149) 46 (ite ?v_149 122 ?v_150)) (ite ?v_184 48 (ite ?v_186 124 (ite (= ?v_150 ?v_29) (ite (not ?v_153) 125 (ite ?v_153 205 ?v_150)) (ite (= ?v_150 ?v_47) (ite (not ?v_156) 53 (ite ?v_156 89 ?v_150)) (ite ?v_191 128 (ite (= ?v_150 ?v_52) (ite (not (= ?v_234 ?v_3)) 208 ?v_150) (ite ?v_194 210 (ite ?v_338 91 (ite ?v_367 219 (ite (= ?v_150 ?v_122) (ite (not ?v_164) 133 (ite ?v_164 201 ?v_150)) (ite (= ?v_150 ?v_126) (ite (not (<= ?v_195 ?v_3)) 223 ?v_150) (ite (= ?v_150 ?v_143) 92 (ite ?v_196 225 (ite ?v_362 449 (ite ?v_285 93 (ite (= ?v_150 ?v_169) (ite (not ?v_172) 138 (ite ?v_172 170 ?v_150)) (ite (= ?v_150 ?v_173) (ite (not ?v_176) 227 (ite ?v_176 263 ?v_150)) (ite ?v_357 60 (ite (= ?v_150 ?v_244) (ite (not ?v_178) 97 (ite ?v_178 115 ?v_150)) (ite ?v_488 629 (ite ?v_593 172 (ite (= ?v_150 ?v_249) (ite (not ?v_180) 584 (ite ?v_180 263 ?v_150)) (ite (not (= ?v_150 ?v_253)) ?v_150 (ite (not ?v_182) 500 (ite ?v_182 344 ?v_150)))))))))))))))))))))))))))) (let ((?v_225 (= ?v_183 ?v_20)) (?v_228 (= ?v_183 ?v_22)) (?v_226 (ite (not ?v_184) ?v_177 i2560))) (let ((?v_185 (<= 4 (+ ?v_226 0))) (?v_229 (ite (not ?v_186) ?v_187 i2560))) (let ((?v_188 (= ?v_229 ?v_3)) (?v_303 (= ?v_183 ?v_38)) (?v_231 (= ?v_183 ?v_39)) (?v_309 (= ?v_183 ?v_65)) (?v_512 (= ?v_183 ?v_66)) (?v_304 (not ?v_189))) (let ((?v_618 (ite ?v_304 ?v_190 (* (- 1) i2370))) (?v_297 (not ?v_191))) (let ((?v_625 (ite ?v_297 ?v_192 i2560))) (let ((?v_193 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_618) ?v_625) 0))) (?v_236 (= ?v_183 ?v_73)) (?v_366 (= ?v_183 ?v_93)) (?v_342 (= ?v_183 ?v_121)) (?v_216 (not ?v_194))) (let ((?v_215 (ite ?v_216 ?v_195 i2560)) (?v_237 (= ?v_183 ?v_144)) (?v_232 (= ?v_183 ?v_145)) (?v_240 (= ?v_183 ?v_146)) (?v_331 (= ?v_183 ?v_168)) (?v_241 (ite (not ?v_196) ?v_197 i2560))) (let ((?v_198 (= ?v_241 ?v_3)) (?v_281 (= ?v_183 ?v_200)) (?v_490 (= ?v_183 ?v_201)) (?v_587 (= ?v_183 ?v_202)) (?v_250 (= ?v_183 ?v_203)) (?v_254 (= ?v_183 ?v_204)) (?v_356 (= ?v_183 ?v_327)) (?v_286 (not ?v_206)) (?v_287 (not ?v_207)) (?v_288 (not ?v_208)) (?v_290 (not ?v_210))) (let ((?v_295 (ite ?v_290 ?v_291 i1875))) (let ((?v_293 (ite ?v_287 (ite ?v_288 0 ?v_291) ?v_295)) (?v_211 (ite ?v_289 0 (* (- 1) i1652)))) (let ((?v_337 (ite ?v_290 ?v_211 (* (- 1) i1875)))) (let ((?v_335 (ite ?v_287 (ite ?v_288 0 ?v_211) ?v_337))) (let ((?v_333 (ite ?v_286 0 ?v_335)) (?v_284 (not ?v_213))) (let ((?v_343 (ite ?v_212 i1140 (ite ?v_284 0 i1140)))) (let ((?v_235 (ite (not ?v_205) 0 (+ 0 ?v_333 ?v_343)))) (let ((?v_214 (= ?v_235 ?v_3)) (?v_233 (= ?v_183 ?v_257)) (?v_589 (= ?v_183 ?v_346)) (?v_348 (ite ?v_216 (ite ?v_217 (ite ?v_218 (ite ?v_219 (ite ?v_220 (ite ?v_221 0 (ite ?v_260 0 (- 2147483647))) (ite ?v_261 0 (- 2147483647))) (ite ?v_262 0 (- 2147483647))) (ite ?v_263 0 (- 2147483647))) (ite ?v_264 0 (- 2147483647))) (ite ?v_265 0 (- 2147483647))))) (let ((?v_222 (<= ?v_215 (+ ?v_348 0)))) (let ((?v_223 (not ?v_222)) (?v_269 (= ?v_183 ?v_353))) (let ((?v_224 (ite ?v_225 48 (ite ?v_228 124 (ite (= ?v_183 ?v_24) (ite (not ?v_185) 50 (ite ?v_185 122 ?v_183)) (ite (= ?v_183 ?v_29) (ite (not ?v_188) 125 (ite ?v_188 205 ?v_183)) (ite ?v_303 126 (ite ?v_231 207 (ite ?v_309 54 (ite ?v_512 90 (ite (= ?v_183 ?v_67) (ite ?v_193 130 (ite (not ?v_193) 203 ?v_183)) (ite ?v_236 210 (ite ?v_366 219 (ite ?v_342 473 (ite (= ?v_183 ?v_126) (ite (not (<= ?v_215 ?v_3)) 223 ?v_183) (ite ?v_237 135 (ite ?v_232 207 (ite ?v_240 225 (ite ?v_331 93 (ite (= ?v_183 ?v_173) (ite (not ?v_198) 227 (ite ?v_198 263 ?v_183)) (ite (= ?v_183 ?v_199) 59 (ite ?v_281 95 (ite ?v_490 139 (ite ?v_587 171 (ite ?v_250 229 (ite ?v_254 265 (ite ?v_356 62 (ite (= ?v_183 ?v_328) (ite ?v_214 98 (ite (not ?v_214) 115 ?v_183)) (ite ?v_233 207 (ite (= ?v_183 ?v_345) 140 (ite ?v_589 453 (ite (= ?v_183 ?v_347) (ite ?v_223 585 (ite ?v_222 582 ?v_183)) (ite (= ?v_183 ?v_351) (ite ?v_223 501 (ite ?v_222 498 ?v_183)) (ite ?v_269 346 ?v_183)))))))))))))))))))))))))))))))))) (let ((?v_271 (= ?v_224 ?v_22)) (?v_245 (ite (not ?v_225) ?v_226 i2747))) (let ((?v_227 (<= 4 (+ ?v_245 0))) (?v_272 (ite (not ?v_228) ?v_229 i2747))) (let ((?v_230 (= ?v_272 ?v_3)) (?v_274 (= ?v_224 ?v_37)) (?v_302 (= ?v_224 ?v_38)) (?v_277 (= ?v_224 ?v_39)) (?v_296 (= ?v_224 ?v_51)) (?v_280 (ite ?v_231 i2747 (ite ?v_232 i2747 (ite (not ?v_233) ?v_234 ?v_235)))) (?v_311 (= ?v_224 ?v_89)) (?v_510 (= ?v_224 ?v_90)) (?v_314 (= ?v_224 ?v_91)) (?v_278 (= ?v_224 ?v_92)) (?v_365 (= ?v_224 ?v_93)) (?v_259 (not ?v_236))) (let ((?v_266 (ite ?v_259 ?v_215 i2747))) (let ((?v_317 (not (<= ?v_266 ?v_3))) (?v_318 (= ?v_224 ?v_146)) (?v_452 (ite (not ?v_237) ?v_238 i2747))) (let ((?v_239 (= ?v_452 ?v_3)) (?v_319 (ite (not ?v_240) ?v_241 i2747))) (let ((?v_242 (= ?v_319 ?v_3)) (?v_329 (= ?v_224 ?v_200)) (?v_321 (= ?v_224 ?v_203)) (?v_324 (= ?v_224 ?v_204)) (?v_438 (= ?v_224 ?v_243)) (?v_246 (<= ?v_245 ?v_3))) (let ((?v_258 (not ?v_246)) (?v_487 (= ?v_224 ?v_247)) (?v_592 (= ?v_224 ?v_248)) (?v_322 (ite (not ?v_250) ?v_251 i2747))) (let ((?v_252 (= ?v_322 ?v_3)) (?v_325 (ite (not ?v_254) ?v_255 i2747))) (let ((?v_256 (= ?v_325 ?v_3)) (?v_279 (= ?v_224 ?v_257)) (?v_553 (= ?v_224 ?v_408)) (?v_489 (= ?v_224 ?v_409)) (?v_412 (ite ?v_259 (ite ?v_216 (ite ?v_217 (ite ?v_218 (ite ?v_219 (ite ?v_220 (ite ?v_221 0 (ite ?v_260 1 2147483647)) (ite ?v_261 1 2147483647)) (ite ?v_262 1 2147483647)) (ite ?v_263 1 2147483647)) (ite ?v_264 1 2147483647)) (ite ?v_265 1 2147483647)) (ite ?v_349 1 2147483647)))) (let ((?v_267 (<= ?v_412 (+ ?v_266 0)))) (let ((?v_268 (not ?v_267)) (?v_420 (ite (not ?v_269) 0 i2747))) (let ((?v_270 (ite ?v_271 124 (ite (= ?v_224 ?v_24) (ite (not ?v_227) 50 (ite ?v_227 122 ?v_224)) (ite (= ?v_224 ?v_29) (ite (not ?v_230) 125 (ite ?v_230 205 ?v_224)) (ite ?v_274 52 (ite ?v_302 126 (ite ?v_277 207 (ite ?v_296 128 (ite (= ?v_224 ?v_52) (ite (not (= ?v_280 ?v_3)) 208 ?v_224) (ite ?v_311 56 (ite ?v_510 91 (ite ?v_314 132 (ite ?v_278 207 (ite ?v_365 219 (ite (= ?v_224 ?v_126) (ite ?v_317 223 ?v_224) (ite (= ?v_224 ?v_143) 92 (ite ?v_318 225 (ite (= ?v_224 ?v_169) (ite (not ?v_239) 138 (ite ?v_239 170 ?v_224)) (ite (= ?v_224 ?v_173) (ite (not ?v_242) 227 (ite ?v_242 263 ?v_224)) (ite ?v_329 95 (ite ?v_321 229 (ite ?v_324 265 (ite ?v_438 60 (ite (= ?v_224 ?v_244) (ite ?v_258 97 (ite ?v_246 115 ?v_224)) (ite ?v_487 629 (ite ?v_592 172 (ite (= ?v_224 ?v_249) (ite (not ?v_252) 584 (ite ?v_252 263 ?v_224)) (ite (= ?v_224 ?v_253) (ite (not ?v_256) 500 (ite ?v_256 344 ?v_224)) (ite ?v_279 207 (ite (= ?v_224 ?v_407) (ite ?v_258 64 (ite ?v_246 85 ?v_224)) (ite ?v_553 545 (ite ?v_489 141 (ite (= ?v_224 ?v_410) 173 (ite (= ?v_224 ?v_411) 582 (ite (= ?v_224 ?v_354) (ite ?v_268 583 (ite ?v_267 230 ?v_224)) (ite (= ?v_224 ?v_416) 498 (ite (= ?v_224 ?v_355) (ite ?v_268 499 (ite ?v_267 267 ?v_224)) (ite (not (= ?v_224 ?v_418)) ?v_224 (ite (not (= ?v_420 ?v_3)) 347 ?v_224)))))))))))))))))))))))))))))))))))))))) (let ((?v_373 (= ?v_270 ?v_22)) (?v_374 (ite (not ?v_271) ?v_272 i2954))) (let ((?v_273 (= ?v_374 ?v_3)) (?v_377 (= ?v_270 ?v_37)) (?v_388 (= ?v_270 ?v_38)) (?v_380 (= ?v_270 ?v_39)) (?v_378 (ite (not ?v_274) ?v_275 i2954))) (let ((?v_276 (= ?v_378 ?v_3)) (?v_386 (= ?v_270 ?v_51)) (?v_283 (* (- 1) i1140))) (let ((?v_688 (ite ?v_282 ?v_283 (ite ?v_212 ?v_283 (ite ?v_284 0 ?v_283)))) (?v_332 (not ?v_285)) (?v_334 (not ?v_292)) (?v_336 (not ?v_294))) (let ((?v_694 (ite ?v_336 ?v_295 i2030))) (let ((?v_692 (ite ?v_334 ?v_293 ?v_694))) (let ((?v_699 (ite ?v_332 (ite ?v_286 0 ?v_293) ?v_692))) (let ((?v_330 (ite (not ?v_281) ?v_235 (- (+ 0 ?v_688 ?v_699))))) (let ((?v_385 (ite ?v_277 i2954 (ite ?v_278 i2954 (ite (not ?v_279) ?v_280 ?v_330)))) (?v_624 (not ?v_296)) (?v_531 (* (- 1) i2954)) (?v_530 (* (- 1) i2029)) (?v_529 (* (- 1) i1727))) (let ((?v_387 (ite ?v_624 (ite ?v_297 (ite ?v_298 (ite ?v_299 (ite ?v_300 0 ?v_301) ?v_529) ?v_530) (* (- 1) i2560)) ?v_531)) (?v_616 (not ?v_302)) (?v_617 (not ?v_303))) (let ((?v_389 (ite ?v_616 (ite ?v_617 (ite ?v_304 (ite ?v_305 (ite ?v_306 (ite ?v_307 0 i1531) i1651) i1874) i2370) i2747) i2954))) (let ((?v_308 (= (+ 0 ?v_387 (+ 0 1 ?v_389)) ?v_390)) (?v_402 (= ?v_270 ?v_73)) (?v_535 (not ?v_309)) (?v_619 (* (- 1) i2747))) (let ((?v_629 (ite ?v_535 ?v_310 ?v_619)) (?v_526 (not ?v_311))) (let ((?v_632 (ite ?v_526 ?v_312 i2954))) (let ((?v_313 (= (- 1) (+ (+ 0 (+ 0 (- 1) ?v_629) ?v_632) 0))) (?v_514 (= ?v_270 ?v_121)) (?v_427 (ite (not ?v_314) ?v_315 i2954))) (let ((?v_316 (<= 4 (+ ?v_427 0))) (?v_392 (= ?v_270 ?v_146)) (?v_508 (= ?v_270 ?v_168)) (?v_393 (ite (not ?v_318) ?v_319 i2954))) (let ((?v_320 (= ?v_393 ?v_3)) (?v_607 (= ?v_270 ?v_201)) (?v_718 (= ?v_270 ?v_202)) (?v_395 (= ?v_270 ?v_203)) (?v_398 (= ?v_270 ?v_204)) (?v_396 (ite (not ?v_321) ?v_322 i2954))) (let ((?v_323 (= ?v_396 ?v_3)) (?v_399 (ite (not ?v_324) ?v_325 i2954))) (let ((?v_326 (= ?v_399 ?v_3)) (?v_436 (= ?v_270 ?v_327)) (?v_698 (not ?v_331)) (?v_691 (not ?v_338)) (?v_693 (not ?v_340))) (let ((?v_696 (ite ?v_693 ?v_694 i2371))) (let ((?v_700 (ite ?v_691 ?v_692 ?v_696)) (?v_360 (* (- 1) i2030))) (let ((?v_341 (ite ?v_336 ?v_337 ?v_360))) (let ((?v_339 (ite ?v_334 ?v_335 ?v_341)) (?v_361 (* (- 1) i2371))) (let ((?v_513 (ite ?v_693 ?v_341 ?v_361))) (let ((?v_511 (ite ?v_691 ?v_339 ?v_513))) (let ((?v_509 (ite ?v_698 (ite ?v_332 ?v_333 ?v_339) ?v_511)) (?v_515 (ite ?v_342 i1140 (ite ?v_282 i1140 ?v_343)))) (let ((?v_382 (ite (not ?v_329) ?v_330 (+ 0 ?v_509 ?v_515)))) (let ((?v_344 (= ?v_382 ?v_3))) (let ((?v_401 (not ?v_344)) (?v_381 (= ?v_270 ?v_257)) (?v_586 (= ?v_270 ?v_346)) (?v_404 (ite ?v_259 ?v_348 (ite ?v_349 0 (- 2147483647))))) (let ((?v_350 (<= ?v_266 (+ ?v_404 0)))) (let ((?v_352 (not ?v_350)) (?v_419 (= ?v_270 ?v_353)) (?v_441 (not ?v_357)) (?v_439 (not ?v_358)) (?v_440 (not ?v_359))) (let ((?v_442 (ite ?v_439 (ite ?v_440 0 i2030) i2371)) (?v_437 (not ?v_363))) (let ((?v_384 (ite (not ?v_356) 0 (+ 0 (ite ?v_441 0 (ite ?v_439 (ite ?v_440 0 ?v_360) ?v_361)) (ite ?v_362 i1140 (ite ?v_437 0 i1140)))))) (let ((?v_364 (= ?v_384 ?v_3)) (?v_383 (= ?v_270 ?v_421)) (?v_486 (= ?v_270 ?v_478)) (?v_591 (= ?v_270 ?v_479)) (?v_498 (= ?v_270 ?v_423)) (?v_481 (ite (not ?v_365) (ite (not ?v_366) (ite (not ?v_367) (ite (not ?v_368) (ite (not ?v_369) (ite (not ?v_370) (ite (not ?v_371) 0 i1728) i2030) i2202) i2371) i2561) i2748) i2955))) (let ((?v_372 (= (- 1) (+ ?v_481 0)))) (let ((?v_426 (not ?v_372)) (?v_500 (= ?v_270 ?v_483))) (let ((?v_376 (ite ?v_373 124 (ite (= ?v_270 ?v_29) (ite (not ?v_273) 125 (ite ?v_273 205 ?v_270)) (ite ?v_377 52 (ite ?v_388 126 (ite ?v_380 207 (ite (= ?v_270 ?v_47) (ite (not ?v_276) 53 (ite ?v_276 89 ?v_270)) (ite ?v_386 128 (ite (= ?v_270 ?v_52) (ite (not (= ?v_385 ?v_3)) 208 ?v_270) (ite (= ?v_270 ?v_67) (ite ?v_308 130 (ite (not ?v_308) 203 ?v_270)) (ite ?v_402 210 (ite (= ?v_270 ?v_114) (ite ?v_313 57 (ite (not ?v_313) 89 ?v_270)) (ite ?v_514 473 (ite (= ?v_270 ?v_122) (ite (not ?v_316) 133 (ite ?v_316 201 ?v_270)) (ite (= ?v_270 ?v_126) (ite ?v_317 223 ?v_270) (ite ?v_392 225 (ite ?v_508 93 (ite (= ?v_270 ?v_173) (ite (not ?v_320) 227 (ite ?v_320 263 ?v_270)) (ite ?v_607 139 (ite ?v_718 171 (ite ?v_395 229 (ite ?v_398 265 (ite (= ?v_270 ?v_244) (ite ?v_258 97 (ite ?v_246 115 ?v_270)) (ite (= ?v_270 ?v_249) (ite (not ?v_323) 584 (ite ?v_323 263 ?v_270)) (ite (= ?v_270 ?v_253) (ite (not ?v_326) 500 (ite ?v_326 344 ?v_270)) (ite ?v_436 62 (ite (= ?v_270 ?v_328) (ite ?v_344 98 (ite ?v_401 115 ?v_270)) (ite ?v_381 207 (ite (= ?v_270 ?v_345) 140 (ite ?v_586 453 (ite (= ?v_270 ?v_347) (ite ?v_352 585 (ite ?v_350 582 ?v_270)) (ite (= ?v_270 ?v_351) (ite ?v_352 501 (ite ?v_350 498 ?v_270)) (ite ?v_419 346 (ite (= ?v_270 ?v_354) (ite ?v_268 583 (ite ?v_267 230 ?v_270)) (ite (= ?v_270 ?v_355) (ite ?v_268 499 (ite ?v_267 267 ?v_270)) (ite (= ?v_270 ?v_474) (ite ?v_364 66 (ite (not ?v_364) 85 ?v_270)) (ite ?v_383 207 (ite (= ?v_270 ?v_477) 99 (ite ?v_486 143 (ite ?v_591 174 (ite (= ?v_270 ?v_422) 230 (ite ?v_498 232 (ite (= ?v_270 ?v_424) 267 (ite (= ?v_270 ?v_425) (ite ?v_372 268 (ite ?v_426 344 ?v_270)) (ite ?v_500 348 ?v_270))))))))))))))))))))))))))))))))))))))))))))) (?v_375 (= (ite (not ?v_373) ?v_374 i3166) ?v_3))) (let ((?v_445 (= ?v_376 ?v_38)) (?v_430 (= ?v_376 ?v_39)) (?v_379 (= (ite (not ?v_377) ?v_378 i3166) ?v_3)) (?v_443 (= ?v_376 ?v_51)) (?v_435 (ite ?v_380 i3166 (ite ?v_381 ?v_382 (ite ?v_383 ?v_384 ?v_385)))) (?v_534 (= ?v_376 ?v_65)) (?v_623 (not ?v_386)) (?v_501 (* (- 1) i3166))) (let ((?v_444 (ite ?v_623 ?v_387 ?v_501)) (?v_615 (not ?v_388))) (let ((?v_446 (ite ?v_615 ?v_389 i3166))) (let ((?v_391 (= (+ 0 ?v_444 (+ 0 1 ?v_446)) ?v_390)) (?v_450 (= ?v_376 ?v_73)) (?v_448 (= ?v_376 ?v_91)) (?v_431 (= ?v_376 ?v_92)) (?v_480 (= ?v_376 ?v_93)) (?v_451 (= ?v_376 ?v_144)) (?v_432 (= ?v_376 ?v_145)) (?v_454 (= ?v_376 ?v_146)) (?v_455 (ite (not ?v_392) ?v_393 i3166))) (let ((?v_394 (= ?v_455 ?v_3)) (?v_507 (= ?v_376 ?v_200)) (?v_457 (= ?v_376 ?v_203)) (?v_460 (= ?v_376 ?v_204)) (?v_603 (= ?v_376 ?v_247)) (?v_723 (= ?v_376 ?v_248)) (?v_458 (ite (not ?v_395) ?v_396 i3166))) (let ((?v_397 (= ?v_458 ?v_3)) (?v_461 (ite (not ?v_398) ?v_399 i3166))) (let ((?v_400 (= ?v_461 ?v_3)) (?v_433 (= ?v_376 ?v_257)) (?v_403 (not ?v_402))) (let ((?v_414 (ite ?v_403 ?v_266 i3166)) (?v_465 (ite ?v_403 ?v_404 (ite ?v_413 0 (- 2147483647))))) (let ((?v_405 (<= ?v_414 (+ ?v_465 0)))) (let ((?v_406 (not ?v_405)) (?v_472 (= ?v_376 ?v_353)) (?v_552 (= ?v_376 ?v_408)) (?v_605 (= ?v_376 ?v_409)) (?v_468 (ite ?v_403 ?v_412 (ite ?v_413 1 2147483647)))) (let ((?v_415 (<= ?v_468 (+ ?v_414 0)))) (let ((?v_417 (not ?v_415)) (?v_473 (ite (not ?v_419) ?v_420 i3166)) (?v_434 (= ?v_376 ?v_421)) (?v_496 (= ?v_376 ?v_423)) (?v_550 (= ?v_376 ?v_570)) (?v_428 (<= ?v_427 ?v_3)) (?v_585 (= ?v_376 ?v_574)) (?v_708 (= ?v_376 ?v_484)) (?v_497 (= ?v_376 ?v_485)) (?v_502 (= ?v_376 ?v_575))) (let ((?v_429 (ite (= ?v_376 ?v_29) (ite (not ?v_375) 125 (ite ?v_375 205 ?v_376)) (ite ?v_445 126 (ite ?v_430 207 (ite (= ?v_376 ?v_47) (ite (not ?v_379) 53 (ite ?v_379 89 ?v_376)) (ite ?v_443 128 (ite (= ?v_376 ?v_52) (ite (not (= ?v_435 ?v_3)) 208 ?v_376) (ite ?v_534 54 (ite (= ?v_376 ?v_66) 90 (ite (= ?v_376 ?v_67) (ite ?v_391 130 (ite (not ?v_391) 203 ?v_376)) (ite ?v_450 210 (ite ?v_448 132 (ite ?v_431 207 (ite ?v_480 219 (ite (= ?v_376 ?v_142) 58 (ite (= ?v_376 ?v_143) 92 (ite ?v_451 135 (ite ?v_432 207 (ite ?v_454 225 (ite (= ?v_376 ?v_173) (ite (not ?v_394) 227 (ite ?v_394 263 ?v_376)) (ite ?v_507 95 (ite ?v_457 229 (ite ?v_460 265 (ite ?v_603 629 (ite ?v_723 172 (ite (= ?v_376 ?v_249) (ite (not ?v_397) 584 (ite ?v_397 263 ?v_376)) (ite (= ?v_376 ?v_253) (ite (not ?v_400) 500 (ite ?v_400 344 ?v_376)) (ite (= ?v_376 ?v_328) (ite ?v_344 98 (ite ?v_401 115 ?v_376)) (ite ?v_433 207 (ite (= ?v_376 ?v_347) (ite ?v_406 585 (ite ?v_405 582 ?v_376)) (ite (= ?v_376 ?v_351) (ite ?v_406 501 (ite ?v_405 498 ?v_376)) (ite ?v_472 346 (ite (= ?v_376 ?v_407) (ite ?v_258 64 (ite ?v_246 85 ?v_376)) (ite ?v_552 545 (ite ?v_605 141 (ite (= ?v_376 ?v_410) 173 (ite (= ?v_376 ?v_411) 582 (ite (= ?v_376 ?v_354) (ite ?v_417 583 (ite ?v_415 230 ?v_376)) (ite (= ?v_376 ?v_416) 498 (ite (= ?v_376 ?v_355) (ite ?v_417 499 (ite ?v_415 267 ?v_376)) (ite (= ?v_376 ?v_418) (ite (not (= ?v_473 ?v_3)) 347 ?v_376) (ite ?v_434 207 (ite (= ?v_376 ?v_422) 230 (ite ?v_496 232 (ite (= ?v_376 ?v_424) 267 (ite (= ?v_376 ?v_425) (ite ?v_372 268 (ite ?v_426 344 ?v_376)) (ite (= ?v_376 ?v_569) 605 (ite ?v_550 100 (ite (= ?v_376 ?v_571) (ite (not ?v_428) 145 (ite ?v_428 166 ?v_376)) (ite ?v_585 176 (ite ?v_708 234 (ite ?v_497 270 (ite ?v_502 350 ?v_376)))))))))))))))))))))))))))))))))))))))))))))))))))))) (let ((?v_522 (= ?v_429 ?v_38)) (?v_504 (= ?v_429 ?v_39)) (?v_520 (= ?v_429 ?v_51)) (?v_475 (ite (not ?v_436) ?v_384 (- (+ 0 (ite ?v_362 ?v_283 (ite ?v_437 0 ?v_283)) (ite ?v_438 ?v_442 (ite ?v_441 0 ?v_442))))))) (let ((?v_519 (ite ?v_430 i3389 (ite ?v_431 i3389 (ite ?v_432 i3389 (ite ?v_433 ?v_382 (ite (not ?v_434) ?v_435 ?v_475)))))) (?v_533 (= ?v_429 ?v_65)) (?v_622 (not ?v_443)) (?v_551 (* (- 1) i3389))) (let ((?v_521 (ite ?v_622 ?v_444 ?v_551)) (?v_614 (not ?v_445))) (let ((?v_523 (ite ?v_614 ?v_446 i3389))) (let ((?v_447 (= (+ 0 ?v_521 (+ 0 1 ?v_523)) ?v_390)) (?v_541 (= ?v_429 ?v_73)) (?v_525 (= ?v_429 ?v_89)) (?v_539 (= ?v_429 ?v_91)) (?v_505 (= ?v_429 ?v_92)) (?v_566 (= ?v_429 ?v_93)) (?v_493 (ite (not ?v_448) ?v_427 i3389))) (let ((?v_449 (<= 4 (+ ?v_493 0))) (?v_464 (not ?v_450))) (let ((?v_463 (ite ?v_464 ?v_414 i3389)) (?v_689 (= ?v_429 ?v_168)) (?v_638 (ite (not ?v_451) ?v_452 i3389))) (let ((?v_453 (= ?v_638 ?v_3)) (?v_641 (ite (not ?v_454) ?v_455 i3389))) (let ((?v_456 (= ?v_641 ?v_3)) (?v_542 (= ?v_429 ?v_203)) (?v_545 (= ?v_429 ?v_204)) (?v_543 (ite (not ?v_457) ?v_458 i3389))) (let ((?v_459 (= ?v_543 ?v_3)) (?v_546 (ite (not ?v_460) ?v_461 i3389))) (let ((?v_462 (= ?v_546 ?v_3)) (?v_506 (= ?v_429 ?v_257)) (?v_717 (= ?v_429 ?v_346)) (?v_557 (ite ?v_464 ?v_465 (ite ?v_469 0 (- 2147483647))))) (let ((?v_466 (<= ?v_463 (+ ?v_557 0)))) (let ((?v_467 (not ?v_466)) (?v_564 (= ?v_429 ?v_353)) (?v_739 (= ?v_429 ?v_408)) (?v_560 (ite ?v_464 ?v_468 (ite ?v_469 1 2147483647)))) (let ((?v_470 (<= ?v_560 (+ ?v_463 0)))) (let ((?v_471 (not ?v_470)) (?v_565 (ite (not ?v_472) ?v_473 i3389)) (?v_476 (= ?v_475 ?v_3)) (?v_516 (= ?v_429 ?v_421)) (?v_602 (= ?v_429 ?v_478)) (?v_721 (= ?v_429 ?v_479)) (?v_580 (= ?v_429 ?v_423)) (?v_567 (ite (not ?v_480) ?v_481 i3390))) (let ((?v_482 (= (- 1) (+ ?v_567 0)))) (let ((?v_495 (not ?v_482)) (?v_680 (= ?v_429 ?v_483)) (?v_707 (= ?v_429 ?v_484)) (?v_581 (= ?v_429 ?v_485)) (?v_548 (= ?v_429 ?v_664)) (?v_604 (ite ?v_487 ?v_283 (ite (not ?v_488) 0 ?v_283))) (?v_608 (ite (not ?v_490) (ite (not ?v_491) 0 i2371) i2748))) (let ((?v_606 (ite (not ?v_489) 0 ?v_608))) (let ((?v_518 (ite (not ?v_486) 0 (- (+ 0 ?v_604 ?v_606))))) (let ((?v_492 (= ?v_518 ?v_3)) (?v_517 (= ?v_429 ?v_576)) (?v_494 (<= ?v_493 ?v_3)) (?v_582 (ite ?v_496 i3389 (ite (not ?v_497) (ite (not ?v_498) 0 i3166) i3389)))) (let ((?v_499 (<= 4 (+ ?v_582 0))) (?v_681 (not ?v_500)) (?v_678 (not ?v_502))) (let ((?v_503 (ite ?v_522 126 (ite ?v_504 207 (ite ?v_520 128 (ite (= ?v_429 ?v_52) (ite (not (= ?v_519 ?v_3)) 208 ?v_429) (ite ?v_533 54 (ite (= ?v_429 ?v_66) 90 (ite (= ?v_429 ?v_67) (ite ?v_447 130 (ite (not ?v_447) 203 ?v_429)) (ite ?v_541 210 (ite ?v_525 56 (ite (= ?v_429 ?v_90) 91 (ite ?v_539 132 (ite ?v_505 207 (ite ?v_566 219 (ite (= ?v_429 ?v_122) (ite (not ?v_449) 133 (ite ?v_449 201 ?v_429)) (ite (= ?v_429 ?v_126) (ite (not (<= ?v_463 ?v_3)) 223 ?v_429) (ite (= ?v_429 ?v_167) 449 (ite ?v_689 93 (ite (= ?v_429 ?v_169) (ite (not ?v_453) 138 (ite ?v_453 170 ?v_429)) (ite (= ?v_429 ?v_173) (ite (not ?v_456) 227 (ite ?v_456 263 ?v_429)) (ite ?v_542 229 (ite ?v_545 265 (ite (= ?v_429 ?v_244) (ite ?v_258 97 (ite ?v_246 115 ?v_429)) (ite (= ?v_429 ?v_249) (ite (not ?v_459) 584 (ite ?v_459 263 ?v_429)) (ite (= ?v_429 ?v_253) (ite (not ?v_462) 500 (ite ?v_462 344 ?v_429)) (ite ?v_506 207 (ite (= ?v_429 ?v_345) 140 (ite ?v_717 453 (ite (= ?v_429 ?v_347) (ite ?v_467 585 (ite ?v_466 582 ?v_429)) (ite (= ?v_429 ?v_351) (ite ?v_467 501 (ite ?v_466 498 ?v_429)) (ite ?v_564 346 (ite ?v_739 545 (ite (= ?v_429 ?v_411) 582 (ite (= ?v_429 ?v_354) (ite ?v_471 583 (ite ?v_470 230 ?v_429)) (ite (= ?v_429 ?v_416) 498 (ite (= ?v_429 ?v_355) (ite ?v_471 499 (ite ?v_470 267 ?v_429)) (ite (= ?v_429 ?v_418) (ite (not (= ?v_565 ?v_3)) 347 ?v_429) (ite (= ?v_429 ?v_474) (ite ?v_476 66 (ite (not ?v_476) 85 ?v_429)) (ite ?v_516 207 (ite (= ?v_429 ?v_477) 99 (ite ?v_602 143 (ite ?v_721 174 (ite (= ?v_429 ?v_422) 230 (ite ?v_580 232 (ite (= ?v_429 ?v_424) 267 (ite (= ?v_429 ?v_425) (ite ?v_482 268 (ite ?v_495 344 ?v_429)) (ite ?v_680 348 (ite ?v_707 234 (ite ?v_581 270 (ite (= ?v_429 ?v_663) 67 (ite ?v_548 102 (ite (= ?v_429 ?v_665) (ite ?v_492 147 (ite (not ?v_492) 166 ?v_429)) (ite ?v_517 207 (ite (= ?v_429 ?v_668) (ite (not ?v_494) 178 (ite ?v_494 199 ?v_429)) (ite (= ?v_429 ?v_577) (ite ?v_495 240 (ite ?v_482 238 ?v_429)) (ite (= ?v_429 ?v_579) (ite (not ?v_499) 272 (ite ?v_499 344 ?v_429)) (ite (not (= ?v_429 ?v_676)) ?v_429 (ite (= (- 1) (+ (+ 0 (+ 0 (- 1) (ite ?v_681 0 ?v_501)) (ite ?v_678 0 i3389)) 0)) 352 ?v_429))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (let ((?v_620 (= ?v_503 ?v_51)) (?v_697 (not ?v_508)) (?v_690 (not ?v_510)) (?v_695 (not ?v_512))) (let ((?v_701 (ite ?v_690 ?v_700 (ite ?v_695 ?v_696 i2748))) (?v_549 (ite (not ?v_507) ?v_382 (+ 0 (ite ?v_697 ?v_509 (ite ?v_690 ?v_511 (ite ?v_695 ?v_513 (* (- 1) i2748)))) (ite ?v_514 i1140 ?v_515))))) (let ((?v_611 (ite ?v_504 i3642 (ite ?v_505 i3642 (ite ?v_506 ?v_549 (ite ?v_516 ?v_475 (ite ?v_517 ?v_518 ?v_519)))))) (?v_621 (not ?v_520)) (?v_532 (* (- 1) i3642)) (?v_613 (not ?v_522))) (let ((?v_524 (= (+ 0 (ite ?v_621 ?v_521 ?v_532) (+ 0 1 (ite ?v_613 ?v_523 i3642))) ?v_390)) (?v_636 (= ?v_503 ?v_73)) (?v_630 (= ?v_503 ?v_89)) (?v_634 (= ?v_503 ?v_91)) (?v_596 (= ?v_503 ?v_92)) (?v_660 (= ?v_503 ?v_93)) (?v_631 (not ?v_525)) (?v_627 (not ?v_533)) (?v_628 (not ?v_534))) (let ((?v_538 (= (+ 0 (ite ?v_631 (ite ?v_526 (ite ?v_527 (ite ?v_528 0 ?v_529) ?v_530) ?v_531) ?v_532) (+ 0 1 (ite ?v_627 (ite ?v_628 (ite ?v_535 (ite ?v_536 (ite ?v_537 0 i1651) i1874) i2747) i3389) i3642))) ?v_390)) (?v_572 (ite (not ?v_539) ?v_493 i3642))) (let ((?v_540 (<= 4 (+ ?v_572 0))) (?v_556 (not ?v_541))) (let ((?v_555 (ite ?v_556 ?v_463 i3642)) (?v_637 (= ?v_503 ?v_144)) (?v_597 (= ?v_503 ?v_145)) (?v_640 (= ?v_503 ?v_146)) (?v_687 (= ?v_503 ?v_200)) (?v_643 (= ?v_503 ?v_203)) (?v_646 (= ?v_503 ?v_204)) (?v_644 (ite (not ?v_542) ?v_543 i3642))) (let ((?v_544 (= ?v_644 ?v_3)) (?v_647 (ite (not ?v_545) ?v_546 i3642))) (let ((?v_547 (= ?v_647 ?v_3)) (?v_743 (not ?v_550)) (?v_740 (not ?v_552)) (?v_741 (not ?v_553))) (let ((?v_599 (ite (not ?v_548) ?v_549 (+ 0 (ite ?v_743 0 ?v_551) (ite ?v_740 (ite ?v_741 0 i2954) i3389))))) (let ((?v_554 (= ?v_599 ?v_3)) (?v_598 (= ?v_503 ?v_257)) (?v_651 (ite ?v_556 ?v_557 (ite ?v_561 0 (- 2147483647))))) (let ((?v_558 (<= ?v_555 (+ ?v_651 0)))) (let ((?v_559 (not ?v_558)) (?v_658 (= ?v_503 ?v_353)) (?v_654 (ite ?v_556 ?v_560 (ite ?v_561 1 2147483647)))) (let ((?v_562 (<= ?v_654 (+ ?v_555 0)))) (let ((?v_563 (not ?v_562)) (?v_659 (ite (not ?v_564) ?v_565 i3642)) (?v_600 (= ?v_503 ?v_421)) (?v_672 (= ?v_503 ?v_423)) (?v_661 (ite (not ?v_566) ?v_567 i3643))) (let ((?v_568 (= (- 1) (+ ?v_661 0)))) (let ((?v_578 (not ?v_568)) (?v_679 (= ?v_503 ?v_483)) (?v_742 (= ?v_503 ?v_570)) (?v_573 (<= ?v_572 ?v_3)) (?v_716 (= ?v_503 ?v_574)) (?v_705 (= ?v_503 ?v_484)) (?v_673 (= ?v_503 ?v_485)) (?v_677 (= ?v_503 ?v_575)) (?v_601 (= ?v_503 ?v_576)) (?v_674 (ite ?v_580 i3642 (ite (not ?v_581) ?v_582 i3642)))) (let ((?v_583 (<= 4 (+ ?v_674 0)))) (let ((?v_595 (not ?v_583)) (?v_584 (<= ?v_245 ?v_390))) (let ((?v_772 (not ?v_584)) (?v_590 (ite (not ?v_588) 0 ?v_283))) (let ((?v_719 (ite ?v_587 ?v_283 ?v_590))) (let ((?v_720 (ite ?v_586 ?v_719 (ite (not ?v_589) 0 ?v_590))) (?v_724 (ite (not ?v_592) (ite (not ?v_593) 0 i2561) i2955))) (let ((?v_722 (ite (not ?v_591) 0 ?v_724))) (let ((?v_610 (ite (not ?v_585) 0 (- (+ 0 ?v_720 ?v_722))))) (let ((?v_594 (= ?v_610 ?v_3)) (?v_609 (= ?v_503 ?v_682)) (?v_788 (= ?v_503 ?v_683)) (?v_703 (= ?v_503 ?v_686)) (?v_706 (= ?v_503 ?v_778))) (let ((?v_612 (ite ?v_620 128 (ite (= ?v_503 ?v_52) (ite (not (= ?v_611 ?v_3)) 208 ?v_503) (ite (= ?v_503 ?v_67) (ite ?v_524 130 (ite (not ?v_524) 203 ?v_503)) (ite ?v_636 210 (ite ?v_630 56 (ite (= ?v_503 ?v_90) 91 (ite ?v_634 132 (ite ?v_596 207 (ite ?v_660 219 (ite (= ?v_503 ?v_114) (ite ?v_538 57 (ite (not ?v_538) 89 ?v_503)) (ite (= ?v_503 ?v_121) 473 (ite (= ?v_503 ?v_122) (ite (not ?v_540) 133 (ite ?v_540 201 ?v_503)) (ite (= ?v_503 ?v_126) (ite (not (<= ?v_555 ?v_3)) 223 ?v_503) (ite ?v_637 135 (ite ?v_597 207 (ite ?v_640 225 (ite (= ?v_503 ?v_199) 59 (ite ?v_687 95 (ite (= ?v_503 ?v_201) 139 (ite (= ?v_503 ?v_202) 171 (ite ?v_643 229 (ite ?v_646 265 (ite (= ?v_503 ?v_249) (ite (not ?v_544) 584 (ite ?v_544 263 ?v_503)) (ite (= ?v_503 ?v_253) (ite (not ?v_547) 500 (ite ?v_547 344 ?v_503)) (ite (= ?v_503 ?v_328) (ite ?v_554 98 (ite (not ?v_554) 115 ?v_503)) (ite ?v_598 207 (ite (= ?v_503 ?v_347) (ite ?v_559 585 (ite ?v_558 582 ?v_503)) (ite (= ?v_503 ?v_351) (ite ?v_559 501 (ite ?v_558 498 ?v_503)) (ite ?v_658 346 (ite (= ?v_503 ?v_409) 141 (ite (= ?v_503 ?v_410) 173 (ite (= ?v_503 ?v_411) 582 (ite (= ?v_503 ?v_354) (ite ?v_563 583 (ite ?v_562 230 ?v_503)) (ite (= ?v_503 ?v_416) 498 (ite (= ?v_503 ?v_355) (ite ?v_563 499 (ite ?v_562 267 ?v_503)) (ite (= ?v_503 ?v_418) (ite (not (= ?v_659 ?v_3)) 347 ?v_503) (ite ?v_600 207 (ite (= ?v_503 ?v_477) 99 (ite (= ?v_503 ?v_422) 230 (ite ?v_672 232 (ite (= ?v_503 ?v_424) 267 (ite (= ?v_503 ?v_425) (ite ?v_568 268 (ite ?v_578 344 ?v_503)) (ite ?v_679 348 (ite (= ?v_503 ?v_569) 605 (ite ?v_742 100 (ite (= ?v_503 ?v_571) (ite (not ?v_573) 145 (ite ?v_573 166 ?v_503)) (ite ?v_716 176 (ite ?v_705 234 (ite ?v_673 270 (ite ?v_677 350 (ite ?v_601 207 (ite (= ?v_503 ?v_577) (ite ?v_578 240 (ite ?v_568 238 ?v_503)) (ite (= ?v_503 ?v_579) (ite ?v_595 272 (ite ?v_583 344 ?v_503)) (ite (= ?v_503 ?v_770) 68 (ite (= ?v_503 ?v_771) (ite ?v_772 104 (ite ?v_584 115 ?v_503)) (ite (= ?v_503 ?v_773) 577 (ite (= ?v_503 ?v_774) (ite ?v_594 180 (ite (not ?v_594) 199 ?v_503)) (ite ?v_609 207 (ite ?v_788 241 (ite (= ?v_503 ?v_684) (ite ?v_583 240 (ite ?v_595 249 ?v_503)) (ite ?v_703 274 (ite ?v_706 354 ?v_503))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (?v_666 (ite (not ?v_602) ?v_518 (- (+ 0 (ite ?v_603 ?v_283 ?v_604) (ite (not ?v_605) ?v_606 (ite (not ?v_607) ?v_608 i3167))))))) (let ((?v_715 (ite ?v_596 i3915 (ite ?v_597 i3915 (ite ?v_598 ?v_599 (ite ?v_600 ?v_475 (ite ?v_601 ?v_666 (ite ?v_609 ?v_610 ?v_611))))))) (?v_626 (= (- 1) (+ (+ 0 (+ 0 (- 1) (ite ?v_613 (ite ?v_614 (ite ?v_615 (ite ?v_616 (ite ?v_617 ?v_618 ?v_619) ?v_531) ?v_501) ?v_551) ?v_532)) (ite (not ?v_620) (ite ?v_621 (ite ?v_622 (ite ?v_623 (ite ?v_624 ?v_625 i2954) i3166) i3389) i3642) i3915)) 0))) (?v_728 (= ?v_612 ?v_73)) (?v_726 (= ?v_612 ?v_91)) (?v_709 (= ?v_612 ?v_92)) (?v_756 (= ?v_612 ?v_93)) (?v_633 (= (- 1) (+ (+ 0 (+ 0 (- 1) (ite ?v_627 (ite ?v_628 ?v_629 ?v_551) ?v_532)) (ite (not ?v_630) (ite ?v_631 ?v_632 i3642) i3915)) 0))) (?v_669 (ite (not ?v_634) ?v_572 i3915))) (let ((?v_635 (<= 4 (+ ?v_669 0))) (?v_650 (not ?v_636))) (let ((?v_649 (ite ?v_650 ?v_555 i3915)) (?v_729 (= ?v_612 ?v_144)) (?v_710 (= ?v_612 ?v_145)) (?v_732 (= ?v_612 ?v_146)) (?v_730 (ite (not ?v_637) ?v_638 i3915))) (let ((?v_639 (= ?v_730 ?v_3)) (?v_733 (ite (not ?v_640) ?v_641 i3915))) (let ((?v_642 (= ?v_733 ?v_3)) (?v_735 (= ?v_612 ?v_204)) (?v_645 (= (ite (not ?v_643) ?v_644 i3915) ?v_3)) (?v_736 (ite (not ?v_646) ?v_647 i3915))) (let ((?v_648 (= ?v_736 ?v_3)) (?v_711 (= ?v_612 ?v_257)) (?v_747 (ite ?v_650 ?v_651 (ite ?v_655 0 (- 2147483647))))) (let ((?v_652 (<= ?v_649 (+ ?v_747 0)))) (let ((?v_653 (not ?v_652)) (?v_754 (= ?v_612 ?v_353)) (?v_750 (ite ?v_650 ?v_654 (ite ?v_655 1 2147483647)))) (let ((?v_656 (<= ?v_750 (+ ?v_649 0)))) (let ((?v_657 (not ?v_656)) (?v_755 (ite (not ?v_658) ?v_659 i3915)) (?v_762 (= ?v_612 ?v_423)) (?v_757 (ite (not ?v_660) ?v_661 i3916))) (let ((?v_662 (= (- 1) (+ ?v_757 0)))) (let ((?v_671 (not ?v_662)) (?v_768 (= ?v_612 ?v_483)) (?v_763 (= ?v_612 ?v_485)) (?v_766 (= ?v_612 ?v_575)) (?v_738 (= ?v_612 ?v_664)) (?v_667 (= ?v_666 ?v_3)) (?v_713 (= ?v_612 ?v_576)) (?v_670 (<= ?v_669 ?v_3)) (?v_764 (ite ?v_672 i3915 (ite (not ?v_673) ?v_674 i3915)))) (let ((?v_675 (<= 4 (+ ?v_764 0)))) (let ((?v_685 (not ?v_675)) (?v_767 (ite (not ?v_677) (ite ?v_678 0 ?v_551) (* (- 1) i3915))) (?v_769 (ite (not ?v_679) (ite (not ?v_680) (ite ?v_681 0 i3166) i3642) i3915)) (?v_714 (= ?v_612 ?v_682)) (?v_787 (= ?v_612 ?v_683)) (?v_782 (= ?v_612 ?v_686)) (?v_712 (ite (not ?v_687) ?v_599 (- (+ 0 (ite ?v_514 ?v_283 (ite ?v_342 ?v_283 ?v_688)) (ite ?v_689 ?v_701 (ite ?v_697 (ite ?v_698 ?v_699 ?v_700) ?v_701))))))) (let ((?v_702 (= ?v_712 ?v_3)) (?v_785 (= ?v_612 ?v_779)) (?v_783 (ite (not ?v_703) 0 i3915))) (let ((?v_704 (= ?v_783 ?v_3))) (let ((?v_725 (ite (= ?v_612 ?v_52) (ite (not (= ?v_715 ?v_3)) 208 ?v_612) (ite (= ?v_612 ?v_66) 90 (ite (= ?v_612 ?v_67) (ite ?v_626 130 (ite (not ?v_626) 203 ?v_612)) (ite ?v_728 210 (ite ?v_726 132 (ite ?v_709 207 (ite ?v_756 219 (ite (= ?v_612 ?v_114) (ite ?v_633 57 (ite (not ?v_633) 89 ?v_612)) (ite (= ?v_612 ?v_121) 473 (ite (= ?v_612 ?v_122) (ite (not ?v_635) 133 (ite ?v_635 201 ?v_612)) (ite (= ?v_612 ?v_126) (ite (not (<= ?v_649 ?v_3)) 223 ?v_612) (ite (= ?v_612 ?v_142) 58 (ite (= ?v_612 ?v_143) 92 (ite ?v_729 135 (ite ?v_710 207 (ite ?v_732 225 (ite (= ?v_612 ?v_169) (ite (not ?v_639) 138 (ite ?v_639 170 ?v_612)) (ite (= ?v_612 ?v_173) (ite (not ?v_642) 227 (ite ?v_642 263 ?v_612)) (ite ?v_735 265 (ite (= ?v_612 ?v_243) 60 (ite (= ?v_612 ?v_244) (ite ?v_258 97 (ite ?v_246 115 ?v_612)) (ite (= ?v_612 ?v_247) 629 (ite (= ?v_612 ?v_248) 172 (ite (= ?v_612 ?v_249) (ite (not ?v_645) 584 (ite ?v_645 263 ?v_612)) (ite (= ?v_612 ?v_253) (ite (not ?v_648) 500 (ite ?v_648 344 ?v_612)) (ite ?v_711 207 (ite (= ?v_612 ?v_347) (ite ?v_653 585 (ite ?v_652 582 ?v_612)) (ite (= ?v_612 ?v_351) (ite ?v_653 501 (ite ?v_652 498 ?v_612)) (ite ?v_754 346 (ite (= ?v_612 ?v_408) 545 (ite (= ?v_612 ?v_411) 582 (ite (= ?v_612 ?v_354) (ite ?v_657 583 (ite ?v_656 230 ?v_612)) (ite (= ?v_612 ?v_416) 498 (ite (= ?v_612 ?v_355) (ite ?v_657 499 (ite ?v_656 267 ?v_612)) (ite (= ?v_612 ?v_418) (ite (not (= ?v_755 ?v_3)) 347 ?v_612) (ite (= ?v_612 ?v_478) 143 (ite (= ?v_612 ?v_479) 174 (ite (= ?v_612 ?v_422) 230 (ite ?v_762 232 (ite (= ?v_612 ?v_424) 267 (ite (= ?v_612 ?v_425) (ite ?v_662 268 (ite ?v_671 344 ?v_612)) (ite ?v_768 348 (ite (= ?v_612 ?v_570) 100 (ite (= ?v_612 ?v_484) 234 (ite ?v_763 270 (ite ?v_766 350 (ite (= ?v_612 ?v_663) 67 (ite ?v_738 102 (ite (= ?v_612 ?v_665) (ite ?v_667 147 (ite (not ?v_667) 166 ?v_612)) (ite ?v_713 207 (ite (= ?v_612 ?v_668) (ite (not ?v_670) 178 (ite ?v_670 199 ?v_612)) (ite (= ?v_612 ?v_577) (ite ?v_671 240 (ite ?v_662 238 ?v_612)) (ite (= ?v_612 ?v_579) (ite ?v_685 272 (ite ?v_675 344 ?v_612)) (ite (= ?v_612 ?v_676) (ite (= (+ 0 ?v_767 (+ 0 1 ?v_769)) ?v_390) 352 ?v_612) (ite ?v_714 207 (ite ?v_787 241 (ite (= ?v_612 ?v_684) (ite ?v_675 240 (ite ?v_685 249 ?v_612)) (ite ?v_782 274 (ite (= ?v_612 (+ 68 0)) 70 (ite (= ?v_612 (+ 104 0)) (ite ?v_702 105 (ite (not ?v_702) 115 ?v_612)) (ite (= ?v_612 (+ 577 0)) 148 (ite (= ?v_612 (+ 180 0)) 601 (ite ?v_785 243 (ite (= ?v_612 ?v_780) 251 (ite (= ?v_612 ?v_781) (ite (not ?v_704) 275 (ite ?v_704 468 ?v_612)) (ite (not (= ?v_612 (+ 354 0))) ?v_612 (ite (not (<= 4 (+ (ite ?v_705 i3915 (ite (not ?v_706) (ite (not ?v_707) (ite (not ?v_708) 0 i3389) i3642) i3915)) 0))) 355 ?v_612)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (?v_775 (ite (not ?v_716) ?v_610 (- (+ 0 (ite ?v_717 (ite ?v_718 ?v_283 ?v_719) ?v_720) (ite (not ?v_721) ?v_722 (ite (not ?v_723) ?v_724 i3390)))))) (?v_759 (ite (not ?v_726) ?v_669 i4203))) (let ((?v_727 (<= 4 (+ ?v_759 0))) (?v_746 (not ?v_728))) (let ((?v_745 (ite ?v_746 ?v_649 i4203)) (?v_731 (= (ite (not ?v_729) ?v_730 i4203) ?v_3)) (?v_734 (= (ite (not ?v_732) ?v_733 i4203) ?v_3)) (?v_737 (= (ite (not ?v_735) ?v_736 i4203) ?v_3)) (?v_744 (= (ite (not ?v_738) ?v_712 (- (+ 0 (ite (not ?v_739) (ite ?v_740 (ite ?v_741 0 ?v_531) ?v_551) ?v_532) (ite (not ?v_742) (ite ?v_743 0 i3389) i3915)))) ?v_3))) (let ((?v_748 (<= ?v_745 (+ (ite ?v_746 ?v_747 (ite ?v_751 0 (- 2147483647))) 0)))) (let ((?v_749 (not ?v_748)) (?v_752 (<= (ite ?v_746 ?v_750 (ite ?v_751 1 2147483647)) (+ ?v_745 0)))) (let ((?v_753 (not ?v_752)) (?v_758 (= (- 1) (+ (ite (not ?v_756) ?v_757 i4204) 0)))) (let ((?v_761 (not ?v_758)) (?v_760 (<= ?v_759 ?v_3)) (?v_765 (<= 4 (+ (ite ?v_762 i4203 (ite (not ?v_763) ?v_764 i4203)) 0)))) (let ((?v_777 (not ?v_765)) (?v_786 (* (- 1) i4203)) (?v_776 (= ?v_775 ?v_3)) (?v_784 (= (ite (not ?v_782) ?v_783 i4203) ?v_3))) (let ((?v_789 (= (+ 0 (ite (not ?v_785) 0 ?v_786) (+ 0 1 (ite (not ?v_787) (ite (not ?v_788) 0 i3915) i4203))) ?v_390))) (and true (= (ite (= ?v_725 ?v_52) (ite (not (= (ite ?v_709 i4203 (ite ?v_710 i4203 (ite ?v_711 ?v_712 (ite ?v_713 ?v_666 (ite (not ?v_714) ?v_715 ?v_775))))) ?v_3)) 208 ?v_725) (ite (= ?v_725 ?v_66) 90 (ite (= ?v_725 ?v_73) 210 (ite (= ?v_725 ?v_90) 91 (ite (= ?v_725 ?v_91) 132 (ite (= ?v_725 ?v_92) 207 (ite (= ?v_725 ?v_93) 219 (ite (= ?v_725 ?v_122) (ite (not ?v_727) 133 (ite ?v_727 201 ?v_725)) (ite (= ?v_725 ?v_126) (ite (not (<= ?v_745 ?v_3)) 223 ?v_725) (ite (= ?v_725 ?v_142) 58 (ite (= ?v_725 ?v_143) 92 (ite (= ?v_725 ?v_144) 135 (ite (= ?v_725 ?v_145) 207 (ite (= ?v_725 ?v_146) 225 (ite (= ?v_725 ?v_167) 449 (ite (= ?v_725 ?v_168) 93 (ite (= ?v_725 ?v_169) (ite (not ?v_731) 138 (ite ?v_731 170 ?v_725)) (ite (= ?v_725 ?v_173) (ite (not ?v_734) 227 (ite ?v_734 263 ?v_725)) (ite (= ?v_725 ?v_201) 139 (ite (= ?v_725 ?v_202) 171 (ite (= ?v_725 ?v_203) 229 (ite (= ?v_725 ?v_204) 265 (ite (= ?v_725 ?v_253) (ite (not ?v_737) 500 (ite ?v_737 344 ?v_725)) (ite (= ?v_725 ?v_327) 62 (ite (= ?v_725 ?v_328) (ite ?v_744 98 (ite (not ?v_744) 115 ?v_725)) (ite (= ?v_725 ?v_257) 207 (ite (= ?v_725 ?v_345) 140 (ite (= ?v_725 ?v_346) 453 (ite (= ?v_725 ?v_347) (ite ?v_749 585 (ite ?v_748 582 ?v_725)) (ite (= ?v_725 ?v_351) (ite ?v_749 501 (ite ?v_748 498 ?v_725)) (ite (= ?v_725 ?v_353) 346 (ite (= ?v_725 ?v_411) 582 (ite (= ?v_725 ?v_354) (ite ?v_753 583 (ite ?v_752 230 ?v_725)) (ite (= ?v_725 ?v_416) 498 (ite (= ?v_725 ?v_355) (ite ?v_753 499 (ite ?v_752 267 ?v_725)) (ite (= ?v_725 ?v_418) (ite (not (= (ite (not ?v_754) ?v_755 i4203) ?v_3)) 347 ?v_725) (ite (= ?v_725 ?v_477) 99 (ite (= ?v_725 ?v_422) 230 (ite (= ?v_725 ?v_423) 232 (ite (= ?v_725 ?v_424) 267 (ite (= ?v_725 ?v_425) (ite ?v_758 268 (ite ?v_761 344 ?v_725)) (ite (= ?v_725 ?v_483) 348 (ite (= ?v_725 ?v_571) (ite (not ?v_760) 145 (ite ?v_760 166 ?v_725)) (ite (= ?v_725 ?v_574) 176 (ite (= ?v_725 ?v_484) 234 (ite (= ?v_725 ?v_485) 270 (ite (= ?v_725 ?v_575) 350 (ite (= ?v_725 ?v_664) 102 (ite (= ?v_725 ?v_576) 207 (ite (= ?v_725 ?v_577) (ite ?v_761 240 (ite ?v_758 238 ?v_725)) (ite (= ?v_725 ?v_579) (ite ?v_777 272 (ite ?v_765 344 ?v_725)) (ite (= ?v_725 ?v_676) (ite (= (+ 0 (ite (not ?v_766) ?v_767 ?v_786) (+ 0 1 (ite (not ?v_768) ?v_769 i4203))) ?v_390) 352 ?v_725) (ite (= ?v_725 ?v_770) 68 (ite (= ?v_725 ?v_771) (ite ?v_772 104 (ite ?v_584 115 ?v_725)) (ite (= ?v_725 ?v_773) 577 (ite (= ?v_725 ?v_774) (ite ?v_776 180 (ite (not ?v_776) 199 ?v_725)) (ite (= ?v_725 ?v_682) 207 (ite (= ?v_725 ?v_683) 241 (ite (= ?v_725 ?v_684) (ite ?v_765 240 (ite ?v_777 249 ?v_725)) (ite (= ?v_725 ?v_686) 274 (ite (= ?v_725 ?v_778) 354 (ite (= ?v_725 ?v_779) 243 (ite (= ?v_725 ?v_780) 251 (ite (= ?v_725 ?v_781) (ite (not ?v_784) 275 (ite ?v_784 468 ?v_725)) (ite (= ?v_725 (+ 70 0)) (ite ?v_772 72 (ite ?v_584 85 ?v_725)) (ite (= ?v_725 (+ 105 0)) 613 (ite (= ?v_725 (+ 148 0)) 149 (ite (= ?v_725 (+ 601 0)) 181 (ite (= ?v_725 (+ 243 0)) (ite ?v_789 245 (ite (not ?v_789) 248 ?v_725)) (ite (= ?v_725 (+ 251 0)) 263 (ite (= ?v_725 (+ 275 0)) 276 (ite (= ?v_725 (+ 468 0)) (ite ?v_749 469 (ite ?v_748 466 ?v_725)) (ite (= ?v_725 (+ 355 0)) 357 ?v_725))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) (+ 469 0))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)
projects / cvc5.git / commitdiff