std::vector<Node>& subs,
QAttributes& qa)
{
- // elimination based on inequalities
- std::map<Node, std::map<bool, std::map<Node, bool> > > num_bounds;
+ Trace("var-elim-quant-debug") << "getVarElimIneq " << body << std::endl;
+ // For each variable v, we compute a set of implied bounds in the body
+ // of the quantified formula.
+ // num_bounds[x][-1] stores the entailed lower bounds for x
+ // num_bounds[x][1] stores the entailed upper bounds for x
+ // num_bounds[x][0] stores the entailed disequalities for x
+ // These bounds are stored in a map that maps the literal for the bound to
+ // its required polarity. For example, for quantified formula
+ // (forall ((x Int)) (or (= x 0) (>= x a)))
+ // we have:
+ // num_bounds[x][0] contains { x -> { (= x 0) -> false } }
+ // num_bounds[x][-1] contains { x -> { (>= x a) -> false } }
+ // This method succeeds in eliminating x if its only occurrences are in
+ // entailed disequalities, and one kind of bound. This is the case for the
+ // above quantified formula, which can be rewritten to false. The reason
+ // is that we can always chose a value for x that is arbitrarily large (resp.
+ // small) to satisfy all disequalities and inequalities for x.
+ std::map<Node, std::map<int, std::map<Node, bool>>> num_bounds;
+ // The set of variables that we know we can not eliminate
+ std::unordered_set<Node> ineligVars;
+ // compute the entailed literals
QuantPhaseReq qpr(body);
+ // map to track which literals we have already processed, and hence can be
+ // excluded from the free variables check in the latter half of this method.
+ std::map<Node, int> processed;
for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
{
// an inequality that is entailed with a given polarity
Node lit = pr.first;
- if (lit.getKind() != GEQ)
- {
- continue;
- }
bool pol = pr.second;
Trace("var-elim-quant-debug") << "Process inequality bounds : " << lit
<< ", pol = " << pol << "..." << std::endl;
+ bool canSolve =
+ lit.getKind() == GEQ
+ || (lit.getKind() == EQUAL && lit[0].getType().isReal() && !pol);
+ if (!canSolve)
+ {
+ continue;
+ }
// solve the inequality
std::map<Node, Node> msum;
if (!ArithMSum::getMonomialSumLit(lit, msum))
// not an inequality, cannot use
continue;
}
+ processed[lit] = pol ? -1 : 1;
for (const std::pair<const Node, Node>& m : msum)
{
- if (!m.first.isNull())
+ if (!m.first.isNull() && ineligVars.find(m.first) == ineligVars.end())
{
std::vector<Node>::iterator ita =
std::find(args.begin(), args.end(), m.first);
ArithMSum::isolate(m.first, msum, veq_c, val, lit.getKind());
if (ires != 0 && veq_c.isNull())
{
- bool is_upper = pol != (ires == 1);
- Trace("var-elim-ineq-debug")
- << lit << " is a " << (is_upper ? "upper" : "lower")
- << " bound for " << m.first << std::endl;
- Trace("var-elim-ineq-debug")
- << " pol/ires = " << pol << " " << ires << std::endl;
- num_bounds[m.first][is_upper][lit] = pol;
+ if (lit.getKind() == GEQ)
+ {
+ bool is_upper = pol != (ires == 1);
+ Trace("var-elim-ineq-debug")
+ << lit << " is a " << (is_upper ? "upper" : "lower")
+ << " bound for " << m.first << std::endl;
+ Trace("var-elim-ineq-debug")
+ << " pol/ires = " << pol << " " << ires << std::endl;
+ num_bounds[m.first][is_upper ? 1 : -1][lit] = pol;
+ }
+ else
+ {
+ Trace("var-elim-ineq-debug")
+ << lit << " is a disequality for " << m.first << std::endl;
+ num_bounds[m.first][0][lit] = pol;
+ }
}
else
{
<< "...ineligible " << m.first
<< " since it cannot be solved for (" << ires << ", " << veq_c
<< ")." << std::endl;
- num_bounds[m.first][true].clear();
- num_bounds[m.first][false].clear();
+ num_bounds.erase(m.first);
+ ineligVars.insert(m.first);
}
}
else
Trace("var-elim-ineq-debug")
<< "...ineligible " << v
<< " since it is contained in monomial." << std::endl;
- num_bounds[v][true].clear();
- num_bounds[v][false].clear();
+ num_bounds.erase(v);
+ ineligVars.insert(v);
}
}
}
// collect all variables that have only upper/lower bounds
std::map<Node, bool> elig_vars;
- for (const std::pair<const Node, std::map<bool, std::map<Node, bool> > >& nb :
+ for (const std::pair<const Node, std::map<int, std::map<Node, bool>>>& nb :
num_bounds)
{
- if (nb.second.find(true) == nb.second.end())
+ if (nb.second.find(1) == nb.second.end())
{
Trace("var-elim-ineq-debug")
<< "Variable " << nb.first << " has only lower bounds." << std::endl;
elig_vars[nb.first] = false;
}
- else if (nb.second.find(false) == nb.second.end())
+ else if (nb.second.find(-1) == nb.second.end())
{
Trace("var-elim-ineq-debug")
<< "Variable " << nb.first << " has only upper bounds." << std::endl;
}
std::vector<Node> inactive_vars;
std::map<Node, std::map<int, bool> > visited;
- std::map<Node, int> exclude;
- for (const std::pair<const Node, bool>& pr : qpr.d_phase_reqs)
- {
- if (pr.first.getKind() == GEQ)
- {
- exclude[pr.first] = pr.second ? -1 : 1;
- Trace("var-elim-ineq-debug")
- << "...exclude " << pr.first << " at polarity " << exclude[pr.first]
- << std::endl;
- }
- }
// traverse the body, invalidate variables if they occur in places other than
// the bounds they occur in
std::unordered_map<TNode, std::unordered_set<int>> evisited;
bool hasPol = ecur_pol != 0;
if (hasPol)
{
- std::map<Node, int>::iterator itx = exclude.find(ecur);
- if (itx != exclude.end() && itx->second == ecur_pol)
+ std::map<Node, int>::iterator itx = processed.find(ecur);
+ if (itx != processed.end() && itx->second == ecur_pol)
{
// already processed this literal as a bound
rec = false;
} while (!evisit.empty() && !elig_vars.empty());
bool ret = false;
+ NodeManager* nm = NodeManager::currentNM();
for (const std::pair<const Node, bool>& ev : elig_vars)
{
Node v = ev.first;
<< v << " is eligible for elimination." << std::endl;
// do substitution corresponding to infinite projection, all literals
// involving unbounded variable go to true/false
- for (const std::pair<const Node, bool>& nb : num_bounds[v][elig_vars[v]])
+ // disequalities of eligible variables are also eliminated
+ std::map<int, std::map<Node, bool>>& nbv = num_bounds[v];
+ for (size_t i = 0; i < 2; i++)
{
- Trace("var-elim-ineq-debug")
- << " subs : " << nb.first << " -> " << nb.second << std::endl;
- bounds.push_back(nb.first);
- subs.push_back(NodeManager::currentNM()->mkConst(nb.second));
+ size_t nindex = i == 0 ? (elig_vars[v] ? 1 : -1) : 0;
+ for (const std::pair<const Node, bool>& nb : nbv[nindex])
+ {
+ Trace("var-elim-ineq-debug")
+ << " subs : " << nb.first << " -> " << nb.second << std::endl;
+ bounds.push_back(nb.first);
+ subs.push_back(nm->mkConst(nb.second));
+ }
}
// eliminate from args
std::vector<Node>::iterator ita = std::find(args.begin(), args.end(), v);
{
return body;
}
+ Trace("var-elim-quant-debug")
+ << "computeVarElimination " << body << std::endl;
Node prev;
while (prev != body && !args.empty())
{
projects / cvc5.git / commitdiff