* 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
// 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
/**
* 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.
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;
}
}
}
-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)
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)
{
Node BvInverter::solve_bv_lit(Node sv,
Node lit,
std::vector<unsigned>& path,
- BvInverterModelQuery* m,
+ BvInverterQuery* m,
BvInverterStatus& status)
{
Assert(!path.empty());
}
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())
{
}
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())
{
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())
{
/* 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;
}
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;
}
/* 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;
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;
}
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
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
/* 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;
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
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
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
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]);
}
}
}
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;
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;
}
}
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;
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;
//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() ){
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) {}
}
};
-//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
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 );
}
};
+/** 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
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 );
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
*
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; }
};
}
// 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;
};
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);
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 ){
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;
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;
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);
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();
+}
/** 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.
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"; }
};
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
--- /dev/null
+; 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)
--- /dev/null
+; 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)
--- /dev/null
+; 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)
+
projects / cvc5.git / commitdiff