diff options
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/quantifiers/bv_inverter.cpp | 222 | ||||
-rw-r--r-- | src/theory/quantifiers/bv_inverter.h | 81 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.cpp | 67 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_instantiator.h | 167 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.cpp | 139 | ||||
-rw-r--r-- | src/theory/quantifiers/ceg_t_instantiator.h | 20 |
6 files changed, 358 insertions, 338 deletions
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<TypeNode, Node>::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<Node, Node, NodeHashFunction>::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<Node>& side_conditions) -{ - std::unordered_map<TNode, Node, TNodeHashFunction> visited; - std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it; - std::stack<TNode> 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<Node> 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<TypeNode, Node>::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<unsigned>& path) { @@ -329,7 +199,7 @@ Node BvInverter::getPathToPv( Node BvInverter::solve_bv_lit(Node sv, Node lit, std::vector<unsigned>& 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<unsigned>& 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<Node>& 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<unsigned>& path, - BvInverterModelQuery* m, BvInverterStatus& status); + Node solve_bv_lit(Node sv, + Node lit, + std::vector<unsigned>& path, + BvInverterQuery* m, + BvInverterStatus& status); private: /** dummy variables for each type */ std::map<TypeNode, Node> d_solve_var; - /** stores the inversion skolems, for each condition */ - std::unordered_map<Node, Node, NodeHashFunction> d_inversion_skolem_cache; - /** helper function for getPathToPv */ Node getPathToPv(Node lit, Node pv, Node sv, std::vector<unsigned>& path, std::unordered_set<TNode, TNodeHashFunction>& 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<n.getNumChildren(); i++ ){ computeProgVars( n[i] ); if( d_inelig.find( n[i] )!=d_inelig.end() ){ - d_inelig[n] = true; - } - for( std::map< Node, bool >::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<Node, NodeHashFunction>::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<TypeNode, unsigned, TypeNodeHashFunction>::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<Node> 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<Node, + std::unordered_set<Node, NodeHashFunction>, + NodeHashFunction> + d_prog_var; + /** cache of the set of terms that we have established are + * ineligible for instantiation. + */ + std::unordered_set<Node, NodeHashFunction> d_inelig; + /** current assertions per theory */ + std::map<TheoryId, std::vector<Node> > d_curr_asserts; + /** map from representatives to the terms in their equivalence class */ + std::map<Node, std::vector<Node> > d_curr_eqc; + /** map from types to representatives of that type */ + std::map<TypeNode, std::vector<Node> > 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<Node> 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<TheoryId> 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<Node, std::map<Node, Node> > d_aux_eq; + /** the variables we are instantiating + * These are the inst constants of the quantified formula + * we are processing. + */ + std::vector<Node> d_vars; + /** set form of d_vars */ + std::unordered_set<Node, NodeHashFunction> d_vars_set; + /** index of variables reported in instantiation */ + std::vector<unsigned> 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<Node> d_ce_atoms; + /** cache bound variables for type returned + * by getBoundVariable(...). + */ + std::unordered_map<TypeNode, std::vector<Node>, 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<TypeNode, unsigned, TypeNodeHashFunction> + d_bound_var_index; + /** collect atoms */ + void collectCeAtoms(Node n, std::map<Node, bool>& 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<lemmas.size(); i++ ){ - Trace("cegqi-bv") << " side condition : " << lemmas[i] << std::endl; - } - } - - return true; -} - -Node BvInstantiator::rewriteAssertionForSolvePv( Node pv, Node lit ) { +Node BvInstantiator::rewriteAssertionForSolvePv(CegInstantiator* ci, + Node pv, + Node lit) +{ NodeManager* nm = NodeManager::currentNM(); // result of rewriting the visited term std::unordered_map<TNode, Node, TNodeHashFunction> 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<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& 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<Node>& children, + std::unordered_map<TNode, bool, TNodeHashFunction>& 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"; } }; |