From 13e452be03bef09e2f54f42e2bc42383505ffcea Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 1 Nov 2017 13:35:07 -0500 Subject: [PATCH] CBQI BV choice expressions (#1296) * Use Hilbert choice expressions for cbqi bv. Failing in debug due to TNode issues currently. * Minor * Make unique bound variables for choice functions in BvInstantor, clean up. * Incorporate missing optimizations * Clang format * Unused field. * Minor * Fix, add regression. * Fix regression. * Fix bug that led to incorrect cleanup of instantiations. * Add missing regression * Improve handling of choice rewriting. * Fix * Clang format * Use canonical variables for choice functions in cbqi bv. * Add regression * Clang format. * Address review. * Clang format --- src/smt/term_formula_removal.cpp | 2 +- src/smt/term_formula_removal.h | 2 +- src/theory/quantifiers/bv_inverter.cpp | 222 ++++-------------- src/theory/quantifiers/bv_inverter.h | 81 +++---- src/theory/quantifiers/ceg_instantiator.cpp | 67 ++++-- src/theory/quantifiers/ceg_instantiator.h | 167 ++++++++++--- src/theory/quantifiers/ceg_t_instantiator.cpp | 139 ++++++----- src/theory/quantifiers/ceg_t_instantiator.h | 20 +- test/regress/regress0/quantifiers/Makefile.am | 5 +- test/regress/regress0/quantifiers/NUM878.smt2 | 7 + .../quantifiers/ari118-bv-2occ-x.smt2 | 8 + .../regress0/quantifiers/psyco-107-bv.smt2 | 162 +++++++++++++ 12 files changed, 541 insertions(+), 341 deletions(-) create mode 100644 test/regress/regress0/quantifiers/NUM878.smt2 create mode 100644 test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 create mode 100644 test/regress/regress0/quantifiers/psyco-107-bv.smt2 diff --git a/src/smt/term_formula_removal.cpp b/src/smt/term_formula_removal.cpp index 01cf59c15..c2f9facce 100644 --- a/src/smt/term_formula_removal.cpp +++ b/src/smt/term_formula_removal.cpp @@ -150,7 +150,7 @@ Node RemoveTermFormulas::run(TNode node, std::vector& output, // The new assertion is the assumption that the body // of the choice operator holds for the Skolem - newAssertion = node[1].substitute(node[0], skolem); + newAssertion = node[1].substitute(node[0][0], skolem); } //if a non-variable Boolean term, replace it diff --git a/src/smt/term_formula_removal.h b/src/smt/term_formula_removal.h index f84f9dc37..371ca1f58 100644 --- a/src/smt/term_formula_removal.h +++ b/src/smt/term_formula_removal.h @@ -50,7 +50,7 @@ public: /** * By introducing skolem variables, this function removes all occurrences of: - * (1) term ITEs + * (1) term ITEs, * (2) terms of type Boolean that are not Boolean term variables, * (3) lambdas, and * (4) Hilbert choice expressions. diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp index 957385a14..d777dc4f8 100644 --- a/src/theory/quantifiers/bv_inverter.cpp +++ b/src/theory/quantifiers/bv_inverter.cpp @@ -52,21 +52,7 @@ Node BvInverter::getSolveVariable(TypeNode tn) std::map::iterator its = d_solve_var.find(tn); if (its == d_solve_var.end()) { - std::stringstream ss; - if (tn.isFunction()) - { - Assert(tn.getNumChildren() == 2); - Assert(tn[0].isBoolean()); - ss << "slv_f"; - } - else - { - ss << "slv"; - } - Node k = NodeManager::currentNM()->mkSkolem(ss.str(), tn); - // marked as a virtual term (it is eligible for instantiation) - VirtualTermSkolemAttribute vtsa; - k.setAttribute(vtsa, true); + Node k = NodeManager::currentNM()->mkSkolem("slv", tn); d_solve_var[tn] = k; return k; } @@ -76,75 +62,50 @@ Node BvInverter::getSolveVariable(TypeNode tn) } } -Node BvInverter::getInversionSkolemFor(Node cond, TypeNode tn) +Node BvInverter::getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m) { // condition should be rewritten - Assert(Rewriter::rewrite(cond) == cond); - std::unordered_map::iterator it = - d_inversion_skolem_cache.find(cond); - if (it == d_inversion_skolem_cache.end()) + Node new_cond = Rewriter::rewrite(cond); + if (new_cond != cond) { - Node skv; - if (cond.getKind() == EQUAL) + Trace("cegqi-bv-skvinv-debug") << "Condition " << cond + << " was rewritten to " << new_cond + << std::endl; + } + Node c; + // optimization : if condition is ( x = v ) should just return v and not + // introduce a Skolem this can happen when we ask for the multiplicative + // inversion with bv1 + TNode solve_var = getSolveVariable(tn); + if (new_cond.getKind() == EQUAL) + { + for (unsigned i = 0; i < 2; i++) { - // optimization : if condition is ( x = v ) should just return v and not - // introduce a Skolem this can happen when we ask for the multiplicative - // inversion with bv1 - Node x = getSolveVariable(tn); - for (unsigned i = 0; i < 2; i++) + if (new_cond[i] == solve_var) { - if (cond[i] == x) - { - skv = cond[1 - i]; - Trace("cegqi-bv-skvinv") - << "SKVINV : " << skv << " is trivially associated with conditon " - << cond << std::endl; - break; - } + c = new_cond[1 - i]; + Trace("cegqi-bv-skvinv") << "SKVINV : " << c + << " is trivially associated with conditon " + << new_cond << std::endl; + break; } } - if (skv.isNull()) - { - // TODO : compute the value if the condition is deterministic, e.g. calc - // multiplicative inverse of 2 constants - skv = NodeManager::currentNM()->mkSkolem( - "skvinv", tn, "created for BvInverter"); - Trace("cegqi-bv-skvinv") - << "SKVINV : " << skv << " is the skolem associated with conditon " - << cond << std::endl; - // marked as a virtual term (it is eligible for instantiation) - VirtualTermSkolemAttribute vtsa; - skv.setAttribute(vtsa, true); - } - d_inversion_skolem_cache[cond] = skv; - return skv; - } - else - { - Assert(it->second.getType() == tn); - return it->second; } -} - -Node BvInverter::getInversionSkolemFunctionFor(TypeNode tn) -{ - NodeManager* nm = NodeManager::currentNM(); - // function maps conditions to skolems - TypeNode ftn = nm->mkFunctionType(nm->booleanType(), tn); - return getSolveVariable(ftn); -} - -Node BvInverter::getInversionNode(Node cond, TypeNode tn) -{ - // condition should be rewritten - Node new_cond = Rewriter::rewrite(cond); - if (new_cond != cond) + // TODO : compute the value if the condition is deterministic, e.g. calc + // multiplicative inverse of 2 constants + if (c.isNull()) { - Trace("bv-invert-debug") << "Condition " << cond << " was rewritten to " - << new_cond << std::endl; + NodeManager* nm = NodeManager::currentNM(); + Node x = m->getBoundVariable(tn); + Node ccond = new_cond.substitute(solve_var, x); + c = nm->mkNode(kind::CHOICE, nm->mkNode(BOUND_VAR_LIST, x), ccond); + Trace("cegqi-bv-skvinv") << "SKVINV : Make " << c << " for " << new_cond + << std::endl; } - Node f = getInversionSkolemFunctionFor(tn); - return NodeManager::currentNM()->mkNode(kind::APPLY_UF, f, new_cond); + // currently shouldn't cache since + // the return value depends on the + // state of m (which bound variable is returned). + return c; } bool BvInverter::isInvertible(Kind k, unsigned index) @@ -219,97 +180,6 @@ Node BvInverter::getPathToPv( return Node::null(); } -Node BvInverter::eliminateSkolemFunctions(TNode n, - std::vector& side_conditions) -{ - std::unordered_map visited; - std::unordered_map::iterator it; - std::stack visit; - TNode cur; - - visit.push(n); - do - { - cur = visit.top(); - visit.pop(); - it = visited.find(cur); - - if (it == visited.end()) - { - visited[cur] = Node::null(); - visit.push(cur); - for (unsigned i = 0; i < cur.getNumChildren(); i++) - { - visit.push(cur[i]); - } - } - else if (it->second.isNull()) - { - Trace("bv-invert-debug") - << "eliminateSkolemFunctions from " << cur << "..." << std::endl; - - Node ret = cur; - bool childChanged = false; - std::vector children; - if (cur.getMetaKind() == kind::metakind::PARAMETERIZED) - { - children.push_back(cur.getOperator()); - } - for (unsigned i = 0; i < cur.getNumChildren(); i++) - { - it = visited.find(cur[i]); - Assert(it != visited.end()); - Assert(!it->second.isNull()); - childChanged = childChanged || cur[i] != it->second; - children.push_back(it->second); - } - if (childChanged) - { - ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); - } - // now, check if it is a skolem function - if (ret.getKind() == APPLY_UF) - { - Node op = ret.getOperator(); - TypeNode tnp = op.getType(); - // is this a skolem function? - std::map::iterator its = d_solve_var.find(tnp); - if (its != d_solve_var.end() && its->second == op) - { - Assert(ret.getNumChildren() == 1); - Assert(ret[0].getType().isBoolean()); - - Node cond = ret[0]; - // must rewrite now to ensure we lookup the correct skolem - cond = Rewriter::rewrite(cond); - - // if so, we replace by the (finalized) skolem variable - // Notice that since we are post-rewriting, skolem functions are - // already eliminated from cond - ret = getInversionSkolemFor(cond, ret.getType()); - - // also must add (substituted) side condition to vector - // substitute ( solve variable -> inversion skolem ) - TNode solve_var = getSolveVariable(ret.getType()); - TNode tret = ret; - cond = cond.substitute(solve_var, tret); - if (std::find(side_conditions.begin(), side_conditions.end(), cond) - == side_conditions.end()) - { - side_conditions.push_back(cond); - } - } - } - Trace("bv-invert-debug") << "eliminateSkolemFunctions from " << cur - << " returned " << ret << std::endl; - visited[cur] = ret; - } - } while (!visit.empty()); - Assert(visited.find(n) != visited.end()); - Assert(!visited.find(n)->second.isNull()); - return visited[n]; -} - Node BvInverter::getPathToPv( Node lit, Node pv, Node sv, Node pvs, std::vector& path) { @@ -329,7 +199,7 @@ Node BvInverter::getPathToPv( Node BvInverter::solve_bv_lit(Node sv, Node lit, std::vector& path, - BvInverterModelQuery* m, + BvInverterQuery* m, BvInverterStatus& status) { Assert(!path.empty()); @@ -413,7 +283,7 @@ Node BvInverter::solve_bv_lit(Node sv, } status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; if (!path.empty()) { @@ -469,7 +339,7 @@ Node BvInverter::solve_bv_lit(Node sv, } status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; if (!path.empty()) { @@ -502,7 +372,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; if (!path.empty()) { @@ -599,7 +469,7 @@ Node BvInverter::solve_bv_lit(Node sv, /* t = skv (fresh skolem constant) * get the skolem node for this side condition */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); /* now solving with the skolem node as the RHS */ t = skv; break; @@ -641,7 +511,7 @@ Node BvInverter::solve_bv_lit(Node sv, } Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; break; } @@ -694,7 +564,7 @@ Node BvInverter::solve_bv_lit(Node sv, /* t = skv (fresh skolem constant) * get the skolem node for this side condition */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); /* now solving with the skolem node as the RHS */ t = skv; break; @@ -713,7 +583,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; break; } @@ -749,7 +619,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; } else @@ -793,7 +663,7 @@ Node BvInverter::solve_bv_lit(Node sv, Node sc = nm->mkNode(IMPLIES, scl, scr); status.d_conds.push_back(sc); /* t = skv (fresh skolem constant) */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); t = skv; } else @@ -863,7 +733,7 @@ Node BvInverter::solve_bv_lit(Node sv, /* t = skv (fresh skolem constant) * get the skolem node for this side condition */ - Node skv = getInversionNode(sc, solve_tn); + Node skv = getInversionNode(sc, solve_tn, m); /* now solving with the skolem node as the RHS */ t = skv; break; diff --git a/src/theory/quantifiers/bv_inverter.h b/src/theory/quantifiers/bv_inverter.h index 1c60d11ea..56f8d492b 100644 --- a/src/theory/quantifiers/bv_inverter.h +++ b/src/theory/quantifiers/bv_inverter.h @@ -28,12 +28,20 @@ namespace CVC4 { namespace theory { namespace quantifiers { -// virtual class for model queries -class BvInverterModelQuery { +/** BvInverterQuery + * + * This is a virtual class for queries + * required by the BvInverter class. + */ +class BvInverterQuery +{ public: - BvInverterModelQuery() {} - ~BvInverterModelQuery() {} + BvInverterQuery() {} + ~BvInverterQuery() {} + /** returns the current model value of n */ virtual Node getModelValue(Node n) = 0; + /** returns a bound variable of type tn */ + virtual Node getBoundVariable(TypeNode tn) = 0; }; // class for storing information about the solved status @@ -53,17 +61,26 @@ class BvInverter { public: BvInverter() {} ~BvInverter() {} - /** get dummy fresh variable of type tn, used as argument for sv */ Node getSolveVariable(TypeNode tn); - /** get inversion node, if : + /** get inversion node + * + * This expects a condition cond where: + * (exists x. cond) + * is a BV tautology where x is getSolveVariable( tn ). * - * f = getInversionSkolemFunctionFor( tn ) + * It returns a term of the form: + * (choice y. cond { x -> y }) + * where y is a bound variable and x is getSolveVariable( tn ). * - * This returns f( cond ). + * In some cases, we may return a term t + * if cond implies an equality on the solve variable. + * For example, if cond is x = t where x is + * getSolveVariable( tn ), then we return t + * instead of introducing the choice function. */ - Node getInversionNode(Node cond, TypeNode tn); + Node getInversionNode(Node cond, TypeNode tn, BvInverterQuery* m); /** Get path to pv in lit, replace that occurrence by sv and all others by * pvs. If return value R is non-null, then : lit.path = pv R.path = sv @@ -72,62 +89,26 @@ class BvInverter { Node getPathToPv(Node lit, Node pv, Node sv, Node pvs, std::vector& path); - /** eliminate skolem functions in node n - * - * This eliminates all Skolem functions from Node n and replaces them with - * finalized Skolem variables. - * - * For each skolem variable we introduce, we ensure its associated side - * condition is added to side_conditions. - * - * Apart from Skolem functions, all subterms of n should be eligible for - * instantiation. - */ - Node eliminateSkolemFunctions(TNode n, std::vector& side_conditions); - /** solve_bv_lit * solve for sv in lit, where lit.path = sv * status accumulates side conditions */ - Node solve_bv_lit(Node sv, Node lit, std::vector& path, - BvInverterModelQuery* m, BvInverterStatus& status); + Node solve_bv_lit(Node sv, + Node lit, + std::vector& path, + BvInverterQuery* m, + BvInverterStatus& status); private: /** dummy variables for each type */ std::map d_solve_var; - /** stores the inversion skolems, for each condition */ - std::unordered_map d_inversion_skolem_cache; - /** helper function for getPathToPv */ Node getPathToPv(Node lit, Node pv, Node sv, std::vector& path, std::unordered_set& visited); // is operator k invertible? bool isInvertible(Kind k, unsigned index); - - /** get inversion skolem for condition - * precondition : exists x. cond( x ) is a tautology in BV, - * where x is getSolveVariable( tn ). - * returns fresh skolem k of type tn, where we may assume cond( k ). - */ - Node getInversionSkolemFor(Node cond, TypeNode tn); - - /** get inversion skolem function for type tn. - * This is a function of type ( Bool -> tn ) that is used for explicitly - * storing side conditions inside terms. For all ( cond, tn ), if : - * - * f = getInversionSkolemFunctionFor( tn ) - * k = getInversionSkolemFor( cond, tn ) - * then: - * f( cond ) is a placeholder for k. - * - * In the call eliminateSkolemFunctions, we replace all f( cond ) with k and - * add cond{ x -> k } to side_conditions. The advantage is that f( cond ) - * explicitly contains the side condition so it automatically updates with - * substitutions. - */ - Node getInversionSkolemFunctionFor(TypeNode tn); }; } // namespace quantifiers diff --git a/src/theory/quantifiers/ceg_instantiator.cpp b/src/theory/quantifiers/ceg_instantiator.cpp index 57bfb2d14..e7749cd92 100644 --- a/src/theory/quantifiers/ceg_instantiator.cpp +++ b/src/theory/quantifiers/ceg_instantiator.cpp @@ -46,24 +46,35 @@ CegInstantiator::~CegInstantiator() { void CegInstantiator::computeProgVars( Node n ){ if( d_prog_var.find( n )==d_prog_var.end() ){ d_prog_var[n].clear(); - if( std::find( d_vars.begin(), d_vars.end(), n )!=d_vars.end() ){ - d_prog_var[n][n] = true; + if (n.getKind() == kind::CHOICE) + { + Assert(d_prog_var.find(n[0][0]) == d_prog_var.end()); + d_prog_var[n[0][0]].clear(); + } + if (d_vars_set.find(n) != d_vars_set.end()) + { + d_prog_var[n].insert(n); }else if( !d_out->isEligibleForInstantiation( n ) ){ - d_inelig[n] = true; + d_inelig.insert(n); return; } for( unsigned i=0; i::iterator it = d_prog_var[n[i]].begin(); it != d_prog_var[n[i]].end(); ++it ){ - d_prog_var[n][it->first] = true; - } - //selectors applied to program variables are also variables - if( n.getKind()==APPLY_SELECTOR_TOTAL && d_prog_var[n].find( n[0] )!=d_prog_var[n].end() ){ - d_prog_var[n][n] = true; + d_inelig.insert(n); } + // all variables in child are contained in this + d_prog_var[n].insert(d_prog_var[n[i]].begin(), d_prog_var[n[i]].end()); + } + // selectors applied to program variables are also variables + if (n.getKind() == APPLY_SELECTOR_TOTAL + && d_prog_var[n].find(n[0]) != d_prog_var[n].end()) + { + d_prog_var[n].insert(n); + } + if (n.getKind() == kind::CHOICE) + { + d_prog_var.erase(n[0][0]); } } } @@ -113,7 +124,8 @@ void CegInstantiator::unregisterInstantiationVariable( Node v ) { bool CegInstantiator::doAddInstantiation( SolvedForm& sf, unsigned i, unsigned effort ){ if( i==d_vars.size() ){ //solved for all variables, now construct instantiation - bool needsPostprocess = false; + bool needsPostprocess = + sf.d_vars.size() > d_vars.size() || !d_var_order_index.empty(); std::vector< Instantiator * > pp_inst; std::map< Instantiator *, Node > pp_inst_to_var; std::vector< Node > lemmas; @@ -522,8 +534,13 @@ bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector bool CegInstantiator::canApplyBasicSubstitution( Node n, std::vector< Node >& non_basic ){ Assert( d_prog_var.find( n )!=d_prog_var.end() ); if( !non_basic.empty() ){ - for( std::map< Node, bool >::iterator it = d_prog_var[n].begin(); it != d_prog_var[n].end(); ++it ){ - if( std::find( non_basic.begin(), non_basic.end(), it->first )!=non_basic.end() ){ + for (std::unordered_set::iterator it = + d_prog_var[n].begin(); + it != d_prog_var[n].end(); + ++it) + { + if (std::find(non_basic.begin(), non_basic.end(), *it) != non_basic.end()) + { return false; } } @@ -699,6 +716,7 @@ bool CegInstantiator::check() { for( unsigned r=0; r<2; r++ ){ SolvedForm sf; d_stack_vars.clear(); + d_bound_var_index.clear(); //try to add an instantiation if( doAddInstantiation( sf, 0, r==0 ? 0 : 2 ) ){ return true; @@ -979,6 +997,26 @@ Node CegInstantiator::getModelValue( Node n ) { return d_qe->getModel()->getValue( n ); } +Node CegInstantiator::getBoundVariable(TypeNode tn) +{ + unsigned index = 0; + std::unordered_map::iterator itb = + d_bound_var_index.find(tn); + if (itb != d_bound_var_index.end()) + { + index = itb->second; + } + d_bound_var_index[tn] = index + 1; + while (index >= d_bound_var[tn].size()) + { + std::stringstream ss; + ss << "x" << index; + Node x = NodeManager::currentNM()->mkBoundVar(ss.str(), tn); + d_bound_var[tn].push_back(x); + } + return d_bound_var[tn][index]; +} + void CegInstantiator::collectCeAtoms( Node n, std::map< Node, bool >& visited ) { if( n.getKind()==FORALL ){ d_is_nested_quant = true; @@ -1010,6 +1048,7 @@ void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, st //Assert( d_vars.empty() ); d_vars.clear(); d_vars.insert( d_vars.end(), ce_vars.begin(), ce_vars.end() ); + d_vars_set.insert(ce_vars.begin(), ce_vars.end()); //determine variable order: must do Reals before Ints if( !d_vars.empty() ){ diff --git a/src/theory/quantifiers/ceg_instantiator.h b/src/theory/quantifiers/ceg_instantiator.h index 0808b5ed0..1e59bfb43 100644 --- a/src/theory/quantifiers/ceg_instantiator.h +++ b/src/theory/quantifiers/ceg_instantiator.h @@ -40,8 +40,11 @@ public: class Instantiator; -//stores properties for a variable to solve for in CEGQI -// For LIA, this includes the coefficient of the variable, and the bound type for the variable +/** Term Properties + * stores properties for a variable to solve for in CEGQI + * For LIA, this includes the coefficient of the variable, and the bound type + * for the variable. + */ class TermProperties { public: TermProperties() : d_type(0) {} @@ -76,9 +79,10 @@ public: } }; -//Solved form -// This specifies a substitution: -// { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| } +/** Solved form + * This specifies a substitution: + * { d_props[i].getModifiedTerm(d_vars[i]) -> d_subs[i] | i = 0...|d_vars| } + */ class SolvedForm { public: // list of variables @@ -89,7 +93,7 @@ public: std::vector< TermProperties > d_props; // the variables that have non-basic information regarding how they are substituted // an example is for linear arithmetic, we store "substitution with coefficients". - std::vector< Node > d_non_basic; + std::vector d_non_basic; // push the substitution pv_prop.getModifiedTerm(pv) -> n void push_back( Node pv, Node n, TermProperties& pv_prop ){ d_vars.push_back( pv ); @@ -134,35 +138,105 @@ public: } }; +/** Ceg instantiator + * + * This class manages counterexample-guided quantifier instantiation + * for a single quantified formula. + */ class CegInstantiator { -private: - QuantifiersEngine * d_qe; - CegqiOutput * d_out; + private: + /** quantified formula associated with this instantiator */ + QuantifiersEngine* d_qe; + /** output channel of this instantiator */ + CegqiOutput* d_out; + /** whether we are using delta for virtual term substitution + * (for quantified LRA). + */ bool d_use_vts_delta; + /** whether we are using infinity for virtual term substitution + * (for quantified LRA). + */ bool d_use_vts_inf; - //program variable contains cache - std::map< Node, std::map< Node, bool > > d_prog_var; - std::map< Node, bool > d_inelig; - //current assertions - std::map< TheoryId, std::vector< Node > > d_curr_asserts; - std::map< Node, std::vector< Node > > d_curr_eqc; - std::map< TypeNode, std::vector< Node > > d_curr_type_eqc; - //auxiliary variables - std::vector< Node > d_aux_vars; - // relevant theory ids - std::vector< TheoryId > d_tids; - //literals to equalities for aux vars - std::map< Node, std::map< Node, Node > > d_aux_eq; - //the CE variables - std::vector< Node > d_vars; - //index of variables reported in instantiation - std::vector< unsigned > d_var_order_index; - //atoms of the CE lemma + /** cache from nodes to the set of variables it contains + * (from the quantified formula we are instantiating). + */ + std::unordered_map, + NodeHashFunction> + d_prog_var; + /** cache of the set of terms that we have established are + * ineligible for instantiation. + */ + std::unordered_set d_inelig; + /** current assertions per theory */ + std::map > d_curr_asserts; + /** map from representatives to the terms in their equivalence class */ + std::map > d_curr_eqc; + /** map from types to representatives of that type */ + std::map > d_curr_type_eqc; + /** auxiliary variables + * These variables include the result of removing ITE + * terms from the quantified formula we are processing. + * These variables must be eliminated from constraints + * as a preprocess step to check(). + */ + std::vector d_aux_vars; + /** relevant theory ids + * A list of theory ids that contain at least one + * constraint in the body of the quantified formula we + * are processing. + */ + std::vector d_tids; + /** literals to equalities for aux vars + * This stores entries of the form + * L -> ( k -> t ) + * where + * k is a variable in d_aux_vars, + * L is a literal that if asserted implies that our + * instantiation should map { k -> t }. + * For example, if a term of the form + * ite( C, t1, t2 ) + * was replaced by k, we get this (top-level) assertion: + * ite( C, k=t1, k=t2 ) + * The vector d_aux_eq contains the exact form of + * the literals in the above constraint that they would + * appear in assertions, meaning d_aux_eq may contain: + * t1=k -> ( k -> t1 ) + * t2=k -> ( k -> t2 ) + * where t1=k and t2=k are the rewritten form of + * k=t1 and k=t2 respectively. + */ + std::map > d_aux_eq; + /** the variables we are instantiating + * These are the inst constants of the quantified formula + * we are processing. + */ + std::vector d_vars; + /** set form of d_vars */ + std::unordered_set d_vars_set; + /** index of variables reported in instantiation */ + std::vector d_var_order_index; + /** are we handled a nested quantified formula? */ bool d_is_nested_quant; - std::vector< Node > d_ce_atoms; - //collect atoms - void collectCeAtoms( Node n, std::map< Node, bool >& visited ); -private: + /** the atoms of the CE lemma */ + std::vector d_ce_atoms; + /** cache bound variables for type returned + * by getBoundVariable(...). + */ + std::unordered_map, TypeNodeHashFunction> + d_bound_var; + /** current index of bound variables for type. + * The next call to getBoundVariable(...) for + * type tn returns the d_bound_var_index[tn]^th + * element of d_bound_var[tn], or a fresh variable + * if not in bounds. + */ + std::unordered_map + d_bound_var_index; + /** collect atoms */ + void collectCeAtoms(Node n, std::map& visited); + + private: //map from variables to their instantiators std::map< Node, Instantiator * > d_instantiator; //cache of current substitutions tried between register/unregister @@ -170,7 +244,7 @@ private: std::map< Node, unsigned > d_curr_index; //stack of temporary variables we are solving (e.g. subfields of datatypes) std::vector< Node > d_stack_vars; - //used instantiators + /** for each variable, the instantiator used for that variable */ std::map< Node, Instantiator * > d_active_instantiators; //register variable void registerInstantiationVariable( Node v, unsigned index ); @@ -224,10 +298,16 @@ public: CegqiOutput * getOutput() { return d_out; } //get quantifiers engine QuantifiersEngine* getQuantifiersEngine() { return d_qe; } - -//interface for instantiators -public: + //------------------------------interface for instantiators + /** push stack variable + * This adds a new variable to solve for in the stack + * of variables we are processing. This stack is only + * used for datatypes, where e.g. the DtInstantiator + * solving for a list x may push the stack "variables" + * head(x) and tail(x). + */ void pushStackVariable( Node v ); + /** pop stack variable */ void popStackVariable(); /** do add instantiation increment * @@ -248,16 +328,27 @@ public: SolvedForm& sf, unsigned effort, bool revertOnSuccess = false); + /** get the current model value of term n */ Node getModelValue( Node n ); -public: + /** get bound variable for type + * + * This gets the next (canonical) bound variable of + * type tn. This can be used for instance when + * constructing instantiations that involve choice expressions. + */ + Node getBoundVariable(TypeNode tn); + //------------------------------end interface for instantiators unsigned getNumCEAtoms() { return d_ce_atoms.size(); } Node getCEAtom( unsigned i ) { return d_ce_atoms[i]; } - // is eligible + /** is n a term that is eligible for instantiation? */ bool isEligible( Node n ); - // has variable + /** does n have variable pv? */ bool hasVariable( Node n, Node pv ); + /** are we using delta for LRA virtual term substitution? */ bool useVtsDelta() { return d_use_vts_delta; } + /** are we using infinity for LRA virtual term substitution? */ bool useVtsInfinity() { return d_use_vts_inf; } + /** are we processing a nested quantified formula? */ bool hasNestedQuantification() { return d_is_nested_quant; } }; diff --git a/src/theory/quantifiers/ceg_t_instantiator.cpp b/src/theory/quantifiers/ceg_t_instantiator.cpp index 60566da1b..756c63cb4 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.cpp +++ b/src/theory/quantifiers/ceg_t_instantiator.cpp @@ -846,16 +846,21 @@ bool EprInstantiator::processEqualTerms( CegInstantiator * ci, SolvedForm& sf, N } // this class can be used to query the model value through the CegInstaniator class -class CegInstantiatorBvInverterModelQuery : public BvInverterModelQuery { -public: - CegInstantiatorBvInverterModelQuery( CegInstantiator * ci ) : - BvInverterModelQuery(), d_ci( ci ){} - ~CegInstantiatorBvInverterModelQuery(){} - // get the model value of n +class CegInstantiatorBvInverterQuery : public BvInverterQuery +{ + public: + CegInstantiatorBvInverterQuery(CegInstantiator* ci) + : BvInverterQuery(), d_ci(ci) + { + } + ~CegInstantiatorBvInverterQuery() {} + /** return the model value of n */ Node getModelValue( Node n ) { return d_ci->getModelValue( n ); } -protected: + /** get bound variable of type tn */ + Node getBoundVariable(TypeNode tn) { return d_ci->getBoundVariable(tn); } + protected: // pointer to class that is able to query model values CegInstantiator * d_ci; }; @@ -891,10 +896,12 @@ void BvInstantiator::processLiteral(CegInstantiator* ci, SolvedForm& sf, std::vector< unsigned > path; Node sv = d_inverter->getSolveVariable( pv.getType() ); Node pvs = ci->getModelValue( pv ); + Trace("cegqi-bv") << "Get path to pv : " << lit << std::endl; Node slit = d_inverter->getPathToPv( lit, pv, sv, pvs, path ); if( !slit.isNull() ){ - CegInstantiatorBvInverterModelQuery m( ci ); + CegInstantiatorBvInverterQuery m(ci); unsigned iid = d_inst_id_counter; + Trace("cegqi-bv") << "Solve lit to bv inverter : " << slit << std::endl; Node inst = d_inverter->solve_bv_lit( sv, slit, path, &m, d_inst_id_to_status[iid] ); if( !inst.isNull() ){ inst = Rewriter::rewrite(inst); @@ -1010,7 +1017,7 @@ bool BvInstantiator::processAssertion(CegInstantiator* ci, SolvedForm& sf, if( options::cbqiBv() ){ // get the best rewritten form of lit for solving for pv // this should remove instances of non-invertible operators, and "linearize" lit with respect to pv as much as possible - Node rlit = rewriteAssertionForSolvePv( pv, lit ); + Node rlit = rewriteAssertionForSolvePv(ci, pv, lit); if( Trace.isOn("cegqi-bv") ){ Trace("cegqi-bv") << "BvInstantiator::processAssertion : solve " << pv << " in " << lit << std::endl; if( lit!=rlit ){ @@ -1139,32 +1146,10 @@ bool BvInstantiator::processAssertions(CegInstantiator* ci, SolvedForm& sf, return false; } - -bool BvInstantiator::needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { - // we may need to post-process the instantiation since inversion skolems need to be finalized - // TODO : technically skolem functions can appear in datatypes with bit-vector fields. We need to eliminate them there too. - return true; -} - -bool BvInstantiator::postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ) { - Trace("cegqi-bv") << "BvInstantiator::postProcessInstantiation " << pv << std::endl; - Assert( std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )!=sf.d_vars.end() ); - unsigned index = std::find( sf.d_vars.begin(), sf.d_vars.end(), pv )-sf.d_vars.begin(); - Trace("cegqi-bv") << " postprocess : " << pv << " -> " << sf.d_subs[index] << std::endl; - // eliminate skolem functions from the substitution - unsigned prev_lem_size = lemmas.size(); - sf.d_subs[index] = d_inverter->eliminateSkolemFunctions( sf.d_subs[index], lemmas ); - if( Trace.isOn("cegqi-bv") ){ - Trace("cegqi-bv") << " got : " << pv << " -> " << sf.d_subs[index] << std::endl; - for( unsigned i=prev_lem_size; i visited; @@ -1180,10 +1165,34 @@ Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) { it = visited.find(cur); if (it == visited.end()) { - visited[cur] = Node::null(); - visit.push(cur); - for (unsigned i = 0; i < cur.getNumChildren(); i++) { - visit.push(cur[i]); + if (cur.getKind() == CHOICE) + { + // must replace variables of choice functions + // with new variables to avoid variable + // capture when considering substitutions + // with multiple literals. + Node bv = ci->getBoundVariable(cur[0][0].getType()); + TNode var = cur[0][0]; + Node sbody = cur[1].substitute(var, bv); + // we cannot cache the results of subterms + // of this choice expression since we are + // now in the context { cur[0][0] -> bv }, + // hence we make a separate call to + // rewriteAssertionForSolvePv here, + // where the recursion depth is the maximum + // depth of nested choice expressions. + Node rsbody = rewriteAssertionForSolvePv(ci, pv, sbody); + visited[cur] = + nm->mkNode(CHOICE, nm->mkNode(BOUND_VAR_LIST, bv), rsbody); + } + else + { + visited[cur] = Node::null(); + visit.push(cur); + for (unsigned i = 0; i < cur.getNumChildren(); i++) + { + visit.push(cur[i]); + } } } else if (it->second.isNull()) { Node ret; @@ -1201,24 +1210,11 @@ Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) { children.push_back(it->second); contains_pv = contains_pv || visited_contains_pv[cur[i]]; } - - // [1] rewrite cases of non-invertible operators - - // if cur is urem( x, y ) where x contains pv but y does not, then - // rewrite urem( x, y ) ---> x - udiv( x, y )*y - if (cur.getKind()==BITVECTOR_UREM_TOTAL) { - if( visited_contains_pv[cur[0]] && !visited_contains_pv[cur[1]] ){ - ret = nm->mkNode( BITVECTOR_SUB, children[0], - nm->mkNode( BITVECTOR_MULT, - nm->mkNode( BITVECTOR_UDIV_TOTAL, children[0], children[1] ), - children[1] ) ); - } - } - - // [2] try to rewrite non-linear literals -> linear literals - - - // return original if the above steps do not produce a result + + // rewrite the term + ret = rewriteTermForSolvePv(pv, cur, children, visited_contains_pv); + + // return original if the above function does not produce a result if (ret.isNull()) { if (childChanged) { ret = NodeManager::currentNM()->mkNode(cur.getKind(), children); @@ -1236,3 +1232,32 @@ Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) { return visited[lit]; } +Node BvInstantiator::rewriteTermForSolvePv( + Node pv, + Node n, + std::vector& children, + std::unordered_map& contains_pv) +{ + NodeManager* nm = NodeManager::currentNM(); + + // [1] rewrite cases of non-invertible operators + + // if n is urem( x, y ) where x contains pv but y does not, then + // rewrite urem( x, y ) ---> x - udiv( x, y )*y + if (n.getKind() == BITVECTOR_UREM_TOTAL) + { + if (contains_pv[n[0]] && !contains_pv[n[1]]) + { + return nm->mkNode( + BITVECTOR_SUB, + children[0], + nm->mkNode(BITVECTOR_MULT, + nm->mkNode(BITVECTOR_UDIV_TOTAL, children[0], children[1]), + children[1])); + } + } + + // [2] try to rewrite non-linear literals -> linear literals + + return Node::null(); +} diff --git a/src/theory/quantifiers/ceg_t_instantiator.h b/src/theory/quantifiers/ceg_t_instantiator.h index 9f47e7211..30dd1bffa 100644 --- a/src/theory/quantifiers/ceg_t_instantiator.h +++ b/src/theory/quantifiers/ceg_t_instantiator.h @@ -101,7 +101,23 @@ private: /** rewrite assertion for solve pv * returns a literal that is equivalent to lit that leads to best solved form for pv */ - Node rewriteAssertionForSolvePv( Node pv, Node lit ); + Node rewriteAssertionForSolvePv(CegInstantiator* ci, Node pv, Node lit); + /** rewrite term for solve pv + * This is a helper function for rewriteAssertionForSolvePv. + * If this returns non-null value ret, then this indicates + * that n should be rewritten to ret. It is called as + * a "post-rewrite", that is, after the children of n + * have been rewritten and stored in the vector children. + * + * contains_pv stores whether certain nodes contain pv. + * where we guarantee that all subterms of terms in children + * appear in the domain of contains_pv. + */ + Node rewriteTermForSolvePv( + Node pv, + Node n, + std::vector& children, + std::unordered_map& contains_pv); /** process literal, called from processAssertion * lit is the literal to solve for pv that has been rewritten according to * internal rules here. @@ -121,8 +137,6 @@ private: Node alit, unsigned effort); bool processAssertions(CegInstantiator* ci, SolvedForm& sf, Node pv, unsigned effort); - bool needsPostProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ); - bool postProcessInstantiationForVariable( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort, std::vector< Node >& lemmas ); bool useModelValue( CegInstantiator * ci, SolvedForm& sf, Node pv, unsigned effort ) { return true; } std::string identify() const { return "Bv"; } }; diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 4cfdec90e..014f06aad 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -111,7 +111,10 @@ TESTS = \ qbv-test-invert-bvult-1.smt2 \ intersection-example-onelane.proof-node22337.smt2 \ nested9_true-unreach-call.i_575.smt2 \ - small-pipeline-fixpoint-3.smt2 + small-pipeline-fixpoint-3.smt2 \ + NUM878.smt2 \ + psyco-107-bv.smt2 \ + ari118-bv-2occ-x.smt2 # regression can be solved with --finite-model-find --fmf-inst-engine diff --git a/test/regress/regress0/quantifiers/NUM878.smt2 b/test/regress/regress0/quantifiers/NUM878.smt2 new file mode 100644 index 000000000..8d78bf861 --- /dev/null +++ b/test/regress/regress0/quantifiers/NUM878.smt2 @@ -0,0 +1,7 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(assert (not (exists ((?X (_ BitVec 32))) (= (bvmul ?X ?X) ?X)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 b/test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 new file mode 100644 index 000000000..2d70dfb8e --- /dev/null +++ b/test/regress/regress0/quantifiers/ari118-bv-2occ-x.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +; two occurrences of x +(assert (not (exists ((?X (_ BitVec 32)) (?Y (_ BitVec 32))) (= (bvmul ?X ?Y) ?X)))) +(check-sat) +(exit) diff --git a/test/regress/regress0/quantifiers/psyco-107-bv.smt2 b/test/regress/regress0/quantifiers/psyco-107-bv.smt2 new file mode 100644 index 000000000..82b54a231 --- /dev/null +++ b/test/regress/regress0/quantifiers/psyco-107-bv.smt2 @@ -0,0 +1,162 @@ +; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun W_S1_V6 () Bool) +(declare-fun W_S1_V4 () Bool) +(declare-fun W_S1_V2 () Bool) +(declare-fun W_S1_V3 () Bool) +(declare-fun W_S1_V1 () Bool) +(declare-fun R_E2_V1 () Bool) +(declare-fun R_E2_V3 () Bool) +(declare-fun R_E1_V3 () Bool) +(declare-fun R_E1_V1 () Bool) +(declare-fun R_E1_V6 () Bool) +(declare-fun R_E1_V4 () Bool) +(declare-fun R_E1_V5 () Bool) +(declare-fun R_E1_V2 () Bool) +(declare-fun DISJ_W_S1_R_E1 () Bool) +(declare-fun R_S1_V6 () Bool) +(declare-fun R_S1_V4 () Bool) +(declare-fun R_S1_V5 () Bool) +(declare-fun R_S1_V2 () Bool) +(declare-fun R_S1_V3 () Bool) +(declare-fun R_S1_V1 () Bool) +(declare-fun DISJ_W_S1_R_S1 () Bool) +(declare-fun R_E2_V6 () Bool) +(declare-fun R_E2_V4 () Bool) +(declare-fun R_E2_V5 () Bool) +(declare-fun R_E2_V2 () Bool) +(declare-fun DISJ_W_S1_R_E2 () Bool) +(declare-fun W_S1_V5 () Bool) +(assert + (let + (($x59848 + (forall + ((V1_0 (_ BitVec 32)) (V3_0 (_ BitVec 32)) + (V2_0 (_ BitVec 32)) (V5_0 (_ BitVec 32)) + (V4_0 (_ BitVec 32)) (V6_0 (_ BitVec 32)) + (MW_S1_V1 Bool) (MW_S1_V3 Bool) + (MW_S1_V2 Bool) (MW_S1_V5 Bool) + (MW_S1_V4 Bool) (MW_S1_V6 Bool) + (S1_V1_!5000 (_ BitVec 32)) (S1_V3_!5001 (_ BitVec 32)) + (S1_V2_!5002 (_ BitVec 32)) (E1_!4994 (_ BitVec 32)) + (E1_!4997 (_ BitVec 32)) (E1_!4999 (_ BitVec 32)) + (S1_V5_!5003 (_ BitVec 32)) (E2_!4995 (_ BitVec 32)) + (E2_!4996 (_ BitVec 32)) (E2_!4998 (_ BitVec 32)) + (S1_V4_!5004 (_ BitVec 32)) (S1_V6_!5005 (_ BitVec 32))) + (let ((?x62719 (ite MW_S1_V6 S1_V6_!5005 V6_0))) + (let (($x60064 (= V6_0 ?x62719))) + (let ((?x61425 (ite MW_S1_V4 S1_V4_!5004 V4_0))) + (let (($x59873 (= V4_0 ?x61425))) + (let ((?x59861 (ite MW_S1_V5 S1_V5_!5003 V5_0))) + (let (($x62312 (= V5_0 ?x59861))) + (let ((?x60966 (ite MW_S1_V2 S1_V2_!5002 V2_0))) + (let (($x61331 (= V2_0 ?x60966))) + (let ((?x62280 (ite MW_S1_V3 S1_V3_!5001 E2_!4998))) + (let ((?x60903 (bvadd (_ bv1 32) ?x62280))) + (let (($x61268 (= E2_!4996 ?x60903))) + (let ((?x60065 (ite MW_S1_V1 S1_V1_!5000 E1_!4999))) + (let (($x60169 (= E1_!4994 ?x60065))) + (let (($x62661 (and $x60169 $x61268 $x61331 $x62312 $x59873 $x60064))) + (let ((?x62301 (bvadd (bvneg (_ bv1 32)) ?x61425))) + (let (($x61124 (bvsge ?x62280 ?x62301))) + (let ((?x61096 (bvadd (bvneg (_ bv1 32)) ?x60966))) + (let (($x60960 (bvsge ?x60065 ?x61096))) + (let (($x62453 (bvsle V2_0 E1_!4999))) + (let (($x61140 (not $x62453))) + (let (($x60239 (bvsle V4_0 E2_!4998))) + (let (($x61367 (not $x60239))) + (let (($x59857 (bvsle V2_0 E1_!4997))) + (let (($x62570 (not $x59857))) + (let ((?x62418 (bvadd (bvneg (_ bv1 32)) V2_0))) + (let (($x60189 (bvsge E1_!4994 ?x62418))) + (let (($x62421 (bvsge E2_!4996 V4_0))) + (let (($x60898 (bvsle V2_0 E1_!4994))) + (let (($x59938 (not $x60898))) + (let (($x62400 (bvsle V4_0 E2_!4995))) + (let (($x60971 (not $x62400))) + (let + (($x62394 + (and $x60971 $x59938 $x62421 $x60189 $x62570 $x61367 $x61140 $x60960 + $x61124))) + (let (($x62485 (not $x62394))) + (let (($x60905 (not MW_S1_V6))) + (let (($x61285 (or $x60905 W_S1_V6))) + (let (($x61317 (not MW_S1_V4))) + (let (($x60137 (or $x61317 W_S1_V4))) + (let (($x62306 (not MW_S1_V2))) + (let (($x62708 (or $x62306 W_S1_V2))) + (let (($x62310 (not MW_S1_V3))) + (let (($x60291 (or $x62310 W_S1_V3))) + (let (($x62641 (not MW_S1_V1))) + (let (($x61174 (or $x62641 W_S1_V1))) + (let (($x62627 (= E2_!4998 E2_!4995))) + (let (($x60904 (= E1_!4997 E1_!4994))) + (let (($x128 (not R_E2_V1))) + (let (($x60161 (or $x128 $x60904))) + (let (($x62415 (not $x60161))) + (let (($x62645 (or $x62415 $x62627))) + (let (($x60924 (= E2_!4996 E2_!4998))) + (let (($x62711 (= E2_!4995 V3_0))) + (let (($x130 (not R_E2_V3))) + (let (($x62623 (or $x130 $x62711))) + (let (($x60954 (= E1_!4994 E1_!4997))) + (let (($x59868 (or $x128 $x60954))) + (let (($x62319 (and $x59868 $x62623))) + (let (($x62554 (not $x62319))) + (let (($x60985 (or $x62554 $x60924))) + (let (($x62256 (= E2_!4996 E2_!4995))) + (let (($x62540 (not $x62623))) + (let (($x60968 (or $x62540 $x62256))) + (let (($x62486 (= E1_!4999 E1_!4997))) + (let (($x60109 (= E2_!4998 V3_0))) + (let (($x115 (not R_E1_V3))) + (let (($x60129 (or $x115 $x60109))) + (let (($x60976 (= E1_!4997 V1_0))) + (let (($x113 (not R_E1_V1))) + (let (($x62568 (or $x113 $x60976))) + (let (($x60942 (and $x62568 $x60129))) + (let (($x60209 (not $x60942))) + (let (($x62263 (or $x60209 $x62486))) + (let (($x60965 (= E1_!4999 E1_!4994))) + (let (($x62348 (or $x60209 $x60965))) + (let + (($x60285 + (and $x60954 $x62348 $x62263 $x60968 $x60985 $x62645 $x61174 $x60291 + $x62708 $x60137 $x61285))) + (let (($x62430 (not $x60285))) (or $x62430 $x62485 $x62661))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) + (let (($x56 (and W_S1_V6 R_E1_V6))) + (let (($x54 (and W_S1_V4 R_E1_V4))) + (let (($x50 (and W_S1_V2 R_E1_V2))) + (let (($x48 (and W_S1_V3 R_E1_V3))) + (let (($x46 (and W_S1_V1 R_E1_V1))) + (let (($x69 (or $x46 $x48 $x50 R_E1_V5 $x54 $x56))) + (let (($x70 (not $x69))) + (let (($x71 (= DISJ_W_S1_R_E1 $x70))) + (let (($x40 (and W_S1_V6 R_S1_V6))) + (let (($x38 (and W_S1_V4 R_S1_V4))) + (let (($x34 (and W_S1_V2 R_S1_V2))) + (let (($x32 (and W_S1_V3 R_S1_V3))) + (let (($x30 (and W_S1_V1 R_S1_V1))) + (let (($x66 (or $x30 $x32 $x34 R_S1_V5 $x38 $x40))) + (let (($x67 (not $x66))) + (let (($x68 (= DISJ_W_S1_R_S1 $x67))) + (let (($x24 (and W_S1_V6 R_E2_V6))) + (let (($x21 (and W_S1_V4 R_E2_V4))) + (let (($x16 (and W_S1_V2 R_E2_V2))) + (let (($x13 (and W_S1_V3 R_E2_V3))) + (let (($x10 (and W_S1_V1 R_E2_V1))) + (let (($x63 (or $x10 $x13 $x16 R_E2_V5 $x21 $x24))) + (let (($x64 (not $x63))) + (let (($x65 (= DISJ_W_S1_R_E2 $x64))) + (let (($x130 (not R_E2_V3))) + (let (($x115 (not R_E1_V3))) + (let (($x113 (not R_E1_V1))) + (let (($x60916 (and $x113 $x115))) + (let (($x62291 (or $x60916 $x130))) + (and $x62291 W_S1_V5 $x65 $x68 $x71 $x59848)))))))))))))))))))))))))))))))) +(assert R_E2_V3) +(check-sat) +(exit) + -- 2.30.2