This updates option names to be consistent across uses of counterexample-guided quantifier instantiation (ceqgi), which was previously called "counterexample-based quantifier instantiation" (cbqi), and sygus.
Notably, the trace "cegqi-engine" is changed to "sygus-engine" by this commit.
The changes were done by these commands in the given directories:
src/:
for f in $(find -name '.'); do sed -i 's/options::cbqi/options::cegqi/g' $f;sed -i 's/cegqi-engine/sygus-engine/g' $f; done;sed -i 's/"cbqi/"cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/--cbqi/--cegqi/g' $f; done
src/: and test/regress/:
for f in $(find -name '.'); do sed -i 's/cegqi-si/sygus-si/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/no-cbqi/no-cegqi/g' $f; done
test/regress/:
for f in $(find -name '.'); do sed -i 's/:cbqi/:cegqi/g' $f; done
And a few minor fixes afterwards.
This should be merged close to the time of the next stable release.
UFBV)
# most problems in UFBV are essentially BV
trywith 600 --full-saturate-quant --decision=internal
- trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
- trywith 60 --full-saturate-quant --no-cbqi-innermost --global-negate
+ trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal
+ trywith 60 --full-saturate-quant --no-cegqi-innermost --global-negate
finishwith --finite-model-find
;;
BV)
trywith 240 --full-saturate-quant
- trywith 240 --full-saturate-quant --no-cbqi-innermost
- trywith 600 --full-saturate-quant --cbqi-nested-qe --decision=internal
- trywith 60 --full-saturate-quant --no-cbqi-bv
- trywith 60 --full-saturate-quant --cbqi-bv-ineq=eq-slack
+ trywith 240 --full-saturate-quant --no-cegqi-innermost
+ trywith 600 --full-saturate-quant --cegqi-nested-qe --decision=internal
+ trywith 60 --full-saturate-quant --no-cegqi-bv
+ trywith 60 --full-saturate-quant --cegqi-bv-ineq=eq-slack
# finish 10min
- finishwith --full-saturate-quant --no-cbqi-innermost --global-negate
+ finishwith --full-saturate-quant --no-cegqi-innermost --global-negate
;;
LIA|LRA|NIA|NRA)
trywith 60 --full-saturate-quant --nl-ext-tplanes
- trywith 600 --full-saturate-quant --no-cbqi-innermost
- trywith 600 --full-saturate-quant --cbqi-nested-qe
- finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+ trywith 600 --full-saturate-quant --no-cegqi-innermost
+ trywith 600 --full-saturate-quant --cegqi-nested-qe
+ finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
;;
QF_AUFBV)
trywith 1200 --ite-simp
finishwith --full-saturate-quant --decision=internal
;;
LIA|LRA)
- finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+ finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
;;
NIA|NRA)
- finishwith --full-saturate-quant --cbqi-nested-qe --decision=internal
+ finishwith --full-saturate-quant --cegqi-nested-qe --decision=internal
;;
QF_AUFBV)
finishwith --decision=justification-stoponly --ite-simp
a.insert("bvminisat");
a.insert("bvminisat::explain");
a.insert("bvminisat::search");
- a.insert("cbqi");
- a.insert("cbqi-debug");
- a.insert("cbqi-prop-as-dec");
+ a.insert("cegqi");
+ a.insert("cegqi-debug");
+ a.insert("cegqi-prop-as-dec");
a.insert("cd_set_collection");
a.insert("cdlist");
a.insert("cdlist:cmm");
"literal-matching",
"enable-cbqi",
"no-enable-cbqi",
- "cbqi-recurse",
+ "cegqi-recurse",
"no-cbqi-recurse",
"user-pat",
"flip-decision",
[[option]]
name = "cegqiSingleInvMode"
category = "regular"
- long = "cegqi-si=MODE"
+ long = "sygus-si=MODE"
type = "CegqiSingleInvMode"
default = "NONE"
help = "mode for processing single invocation synthesis conjectures"
[[option]]
name = "cegqiSingleInvPartial"
category = "regular"
- long = "cegqi-si-partial"
+ long = "sygus-si-partial"
type = "bool"
default = "false"
read_only = true
[[option]]
name = "cegqiSingleInvReconstruct"
category = "regular"
- long = "cegqi-si-rcons=MODE"
+ long = "sygus-si-rcons=MODE"
type = "CegqiSingleInvRconsMode"
default = "ALL_LIMIT"
help = "policy for reconstructing solutions for single invocation conjectures"
[[option]]
name = "cegqiSingleInvReconstructLimit"
category = "regular"
- long = "cegqi-si-rcons-limit=N"
+ long = "sygus-si-rcons-limit=N"
type = "int"
default = "10000"
read_only = true
[[option]]
name = "cegqiSingleInvReconstructConst"
category = "regular"
- long = "cegqi-si-reconstruct-const"
+ long = "sygus-si-reconstruct-const"
type = "bool"
default = "true"
read_only = true
[[option]]
name = "cegqiSingleInvAbort"
category = "regular"
- long = "cegqi-si-abort"
+ long = "sygus-si-abort"
type = "bool"
default = "false"
read_only = true
# CEGQI applied to general quantified formulas
[[option]]
- name = "cbqi"
+ name = "cegqi"
category = "regular"
- long = "cbqi"
+ long = "cegqi"
type = "bool"
default = "false"
help = "turns on counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiFullEffort"
+ name = "cegqiFullEffort"
category = "regular"
- long = "cbqi-full"
+ long = "cegqi-full"
type = "bool"
default = "false"
help = "turns on full effort counterexample-based quantifier instantiation, which may resort to model-value instantiation"
[[option]]
- name = "cbqiSat"
+ name = "cegqiSat"
category = "regular"
- long = "cbqi-sat"
+ long = "cegqi-sat"
type = "bool"
default = "true"
help = "answer sat when quantifiers are asserted with counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiModel"
+ name = "cegqiModel"
category = "regular"
- long = "cbqi-model"
+ long = "cegqi-model"
type = "bool"
default = "true"
help = "guide instantiations by model values for counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiAll"
+ name = "cegqiAll"
category = "regular"
- long = "cbqi-all"
+ long = "cegqi-all"
type = "bool"
default = "false"
help = "apply counterexample-based instantiation to all quantified formulas"
[[option]]
- name = "cbqiMultiInst"
+ name = "cegqiMultiInst"
category = "regular"
- long = "cbqi-multi-inst"
+ long = "cegqi-multi-inst"
type = "bool"
default = "false"
help = "when applicable, do multi instantiations per quantifier per round in counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiRepeatLit"
+ name = "cegqiRepeatLit"
category = "regular"
- long = "cbqi-repeat-lit"
+ long = "cegqi-repeat-lit"
type = "bool"
default = "false"
help = "solve literals more than once in counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiInnermost"
+ name = "cegqiInnermost"
category = "regular"
- long = "cbqi-innermost"
+ long = "cegqi-innermost"
type = "bool"
default = "true"
help = "only process innermost quantified formulas in counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiNestedQE"
+ name = "cegqiNestedQE"
category = "regular"
- long = "cbqi-nested-qe"
+ long = "cegqi-nested-qe"
type = "bool"
default = "false"
help = "process nested quantified formulas with quantifier elimination in counterexample-based quantifier instantiation"
# CEGQI for arithmetic
[[option]]
- name = "cbqiUseInfInt"
+ name = "cegqiUseInfInt"
category = "regular"
- long = "cbqi-use-inf-int"
+ long = "cegqi-use-inf-int"
type = "bool"
default = "false"
help = "use integer infinity for vts in counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiUseInfReal"
+ name = "cegqiUseInfReal"
category = "regular"
- long = "cbqi-use-inf-real"
+ long = "cegqi-use-inf-real"
type = "bool"
default = "false"
help = "use real infinity for vts in counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiPreRegInst"
+ name = "cegqiPreRegInst"
category = "regular"
- long = "cbqi-prereg-inst"
+ long = "cegqi-prereg-inst"
type = "bool"
default = "false"
help = "preregister ground instantiations in counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiMinBounds"
+ name = "cegqiMinBounds"
category = "regular"
- long = "cbqi-min-bounds"
+ long = "cegqi-min-bounds"
type = "bool"
default = "false"
read_only = true
help = "use minimally constrained lower/upper bound for counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiRoundUpLowerLia"
+ name = "cegqiRoundUpLowerLia"
category = "regular"
- long = "cbqi-round-up-lia"
+ long = "cegqi-round-up-lia"
type = "bool"
default = "false"
read_only = true
help = "round up integer lower bounds in substitutions for counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiMidpoint"
+ name = "cegqiMidpoint"
category = "regular"
- long = "cbqi-midpoint"
+ long = "cegqi-midpoint"
type = "bool"
default = "false"
help = "choose substitutions based on midpoints of lower and upper bounds for counterexample-based quantifier instantiation"
[[option]]
- name = "cbqiNopt"
+ name = "cegqiNopt"
category = "regular"
- long = "cbqi-nopt"
+ long = "cegqi-nopt"
type = "bool"
default = "true"
read_only = true
# CEGQI for BV
[[option]]
- name = "cbqiBv"
+ name = "cegqiBv"
category = "regular"
- long = "cbqi-bv"
+ long = "cegqi-bv"
type = "bool"
default = "true"
help = "use word-level inversion approach for counterexample-guided quantifier instantiation for bit-vectors"
[[option]]
- name = "cbqiBvInterleaveValue"
+ name = "cegqiBvInterleaveValue"
category = "regular"
- long = "cbqi-bv-interleave-value"
+ long = "cegqi-bv-interleave-value"
type = "bool"
default = "false"
help = "interleave model value instantiation with word-level inversion approach"
[[option]]
- name = "cbqiBvIneqMode"
+ name = "cegqiBvIneqMode"
category = "regular"
- long = "cbqi-bv-ineq=MODE"
+ long = "cegqi-bv-ineq=MODE"
type = "CbqiBvIneqMode"
default = "EQ_BOUNDARY"
help = "choose mode for handling bit-vector inequalities with counterexample-guided instantiation"
help = "Solve for the inequality directly using side conditions for invertibility."
[[option]]
- name = "cbqiBvRmExtract"
+ name = "cegqiBvRmExtract"
category = "regular"
- long = "cbqi-bv-rm-extract"
+ long = "cegqi-bv-rm-extract"
type = "bool"
default = "true"
help = "replaces extract terms with variables for counterexample-guided instantiation for bit-vectors"
[[option]]
- name = "cbqiBvLinearize"
+ name = "cegqiBvLinearize"
category = "regular"
- long = "cbqi-bv-linear"
+ long = "cegqi-bv-linear"
type = "bool"
default = "true"
help = "linearize adder chains for variables"
[[option]]
- name = "cbqiBvSolveNl"
+ name = "cegqiBvSolveNl"
category = "regular"
- long = "cbqi-bv-solve-nl"
+ long = "cegqi-bv-solve-nl"
type = "bool"
default = "false"
help = "try to solve non-linear bv literals using model value projections"
[[option]]
- name = "cbqiBvConcInv"
+ name = "cegqiBvConcInv"
category = "regular"
- long = "cbqi-bv-concat-inv"
+ long = "cegqi-bv-concat-inv"
type = "bool"
default = "true"
help = "compute inverse for concat over equalities rather than producing an invertibility condition"
Node GlobalNegate::simplify(std::vector<Node>& assertions, NodeManager* nm)
{
Assert(!assertions.empty());
- Trace("cbqi-gn") << "Global negate : " << std::endl;
+ Trace("cegqi-gn") << "Global negate : " << std::endl;
// collect free variables in all assertions
std::vector<Node> free_vars;
std::vector<TNode> visit;
std::unordered_set<TNode, TNodeHashFunction> visited;
for (const Node& as : assertions)
{
- Trace("cbqi-gn") << " " << as << std::endl;
+ Trace("cegqi-gn") << " " << as << std::endl;
TNode cur = as;
// compute free variables
visit.push_back(cur);
body = nm->mkNode(FORALL, bvl, body);
}
- Trace("cbqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
+ Trace("cegqi-gn-debug") << "...got (pre-rewrite) : " << body << std::endl;
body = Rewriter::rewrite(body);
- Trace("cbqi-gn") << "...got (post-rewrite) : " << body << std::endl;
+ Trace("cegqi-gn") << "...got (post-rewrite) : " << body << std::endl;
return body;
}
}
}
- if (options::cbqiBv() && logic.isQuantified())
+ if (options::cegqiBv() && logic.isQuantified())
{
if (options::boolToBitvector() != options::BoolToBVMode::OFF)
{
{
Notice() << "SmtEngine: turning off cbqi to support instMaxLevel"
<< std::endl;
- options::cbqi.set(false);
+ options::cegqi.set(false);
}
// Do we need to track instantiations?
// Needed for sygus due to single invocation techniques.
- if (options::cbqiNestedQE()
+ if (options::cegqiNestedQE()
|| (options::proof() && !options::trackInstLemmas.wasSetByUser())
|| is_sygus)
{
}
options::sygus.set(true);
// must use Ferrante/Rackoff for real arithmetic
- if (!options::cbqiMidpoint.wasSetByUser())
+ if (!options::cegqiMidpoint.wasSetByUser())
{
- options::cbqiMidpoint.set(true);
+ options::cegqiMidpoint.set(true);
}
if (options::sygusRepairConst())
{
- if (!options::cbqi.wasSetByUser())
+ if (!options::cegqi.wasSetByUser())
{
- options::cbqi.set(true);
+ options::cegqi.set(true);
}
}
if (options::sygusInference())
{
options::instNoEntail.set(false);
}
- if (!options::cbqiFullEffort.wasSetByUser())
+ if (!options::cegqiFullEffort.wasSetByUser())
{
// should use full effort cbqi for single invocation and repair const
- options::cbqiFullEffort.set(true);
+ options::cegqiFullEffort.set(true);
}
if (options::sygusRew())
{
{
options::macrosQuant.set(false);
}
- if (!options::cbqiPreRegInst.wasSetByUser())
+ if (!options::cegqiPreRegInst.wasSetByUser())
{
- options::cbqiPreRegInst.set(true);
+ options::cegqiPreRegInst.set(true);
}
}
// counterexample-guided instantiation for non-sygus
|| logic.isTheoryEnabled(THEORY_DATATYPES)
|| logic.isTheoryEnabled(THEORY_BV)
|| logic.isTheoryEnabled(THEORY_FP)))
- || options::cbqiAll())
+ || options::cegqiAll())
{
- if (!options::cbqi.wasSetByUser())
+ if (!options::cegqi.wasSetByUser())
{
- options::cbqi.set(true);
+ options::cegqi.set(true);
}
// check whether we should apply full cbqi
if (logic.isPure(THEORY_BV))
{
- if (!options::cbqiFullEffort.wasSetByUser())
+ if (!options::cegqiFullEffort.wasSetByUser())
{
- options::cbqiFullEffort.set(true);
+ options::cegqiFullEffort.set(true);
}
}
}
- if (options::cbqi())
+ if (options::cegqi())
{
// must rewrite divk
if (!options::rewriteDivk.wasSetByUser())
if (options::incrementalSolving())
{
// cannot do nested quantifier elimination in incremental mode
- options::cbqiNestedQE.set(false);
- options::cbqiPreRegInst.set(false);
+ options::cegqiNestedQE.set(false);
+ options::cegqiPreRegInst.set(false);
}
if (logic.isPure(THEORY_ARITH) || logic.isPure(THEORY_BV))
{
{
options::instNoEntail.set(false);
}
- if (!options::instWhenMode.wasSetByUser() && options::cbqiModel())
+ if (!options::instWhenMode.wasSetByUser() && options::cegqiModel())
{
// only instantiation should happen at last call when model is avaiable
options::instWhenMode.set(options::InstWhenMode::LAST_CALL);
else
{
// only supported in pure arithmetic or pure BV
- options::cbqiNestedQE.set(false);
+ options::cegqiNestedQE.set(false);
}
// prenexing
- if (options::cbqiNestedQE())
+ if (options::cegqiNestedQE())
{
// only complete with prenex = disj_normal or normal
if (options::prenexQuant() <= options::PrenexQuantMode::DISJ_NORMAL)
{
options::quantConflictFind.set(true);
}
- if (options::cbqiNestedQE())
+ if (options::cegqiNestedQE())
{
options::prenexQuantUser.set(true);
if (!options::preSkolemQuant.wasSetByUser())
return check(lemmas);
}
- if (Trace.isOn("cegqi-engine") && !d_szinfo.empty())
+ if (Trace.isOn("sygus-engine") && !d_szinfo.empty())
{
if (lemmas.empty())
{
- Trace("cegqi-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
+ Trace("sygus-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
p : d_szinfo)
{
SygusSizeDecisionStrategy* s = p.second.get();
- Trace("cegqi-engine") << s->d_curr_search_size << " ";
+ Trace("sygus-engine") << s->d_curr_search_size << " ";
}
- Trace("cegqi-engine") << std::endl;
+ Trace("sygus-engine") << std::endl;
}
else
{
- Trace("cegqi-engine")
+ Trace("sygus-engine")
<< "*** Sygus : produced symmetry breaking lemmas" << std::endl;
for (const Node& lem : lemmas)
{
- Trace("cegqi-engine-debug") << " " << lem << std::endl;
+ Trace("sygus-engine-debug") << " " << lem << std::endl;
}
}
}
}
Assert(!d_this.isNull());
NodeManager* nm = NodeManager::currentNM();
- Trace("cegqi-engine") << "******* Sygus : allocate size literal " << s
+ Trace("sygus-engine") << "******* Sygus : allocate size literal " << s
<< " for " << d_this << std::endl;
return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
}
}
else if (k == BITVECTOR_CONCAT)
{
- if (litk == EQUAL && options::cbqiBvConcInv())
+ if (litk == EQUAL && options::cegqiBvConcInv())
{
/* Compute inverse for s1 o x, x o s2, s1 o x o s2
* (while disregarding that invertibility depends on si)
}
// compute how many bounds we will consider
unsigned rmax = 1;
- if (atom.getKind() == EQUAL && (pol || !options::cbqiModel()))
+ if (atom.getKind() == EQUAL && (pol || !options::cegqiModel()))
{
rmax = 2;
}
{
// disequalities are either strict upper or lower bounds
bool is_upper;
- if (options::cbqiModel())
+ if (options::cegqiModel())
{
// disequality is a disjunction : only consider the bound in the
// direction of the model
// take into account delta
if (uires == CEG_TT_UPPER_STRICT || uires == CEG_TT_LOWER_STRICT)
{
- if (options::cbqiModel())
+ if (options::cegqiModel())
{
Node delta_coeff =
nm->mkConst(Rational(isUpperBoundCTT(uires) ? 1 : -1));
uval = Rewriter::rewrite(uval);
}
}
- if (options::cbqiModel())
+ if (options::cegqiModel())
{
// just store bounds, will choose based on tighest bound
unsigned index = isUpperBoundCTT(uires) ? 0 : 1;
Node pv,
CegInstEffort effort)
{
- if (!options::cbqiModel())
+ if (!options::cegqiModel())
{
return false;
}
NodeManager* nm = NodeManager::currentNM();
bool use_inf =
- d_type.isInteger() ? options::cbqiUseInfInt() : options::cbqiUseInfReal();
+ d_type.isInteger() ? options::cegqiUseInfInt() : options::cegqiUseInfReal();
bool upper_first = Random::getRandom().pickWithProb(0.5);
- if (options::cbqiMinBounds())
+ if (options::cegqiMinBounds())
{
upper_first = d_mbp_bounds[1].size() < d_mbp_bounds[0].size();
}
{
return true;
}
- else if (!options::cbqiMultiInst())
+ else if (!options::cegqiMultiInst())
{
return false;
}
best_used[rr] = best;
// if using cbqiMidpoint, only add the instance based on one bound if
// the bound is non-strict
- if (!options::cbqiMidpoint() || d_type.isInteger()
+ if (!options::cegqiMidpoint() || d_type.isInteger()
|| d_mbp_vts_coeff[rr][1][best].isNull())
{
Node val = d_mbp_bounds[rr][best];
{
return true;
}
- else if (!options::cbqiMultiInst())
+ else if (!options::cegqiMultiInst())
{
return false;
}
{
return true;
}
- else if (!options::cbqiMultiInst())
+ else if (!options::cegqiMultiInst())
{
return false;
}
}
}
- if (options::cbqiMidpoint() && !d_type.isInteger())
+ if (options::cegqiMidpoint() && !d_type.isInteger())
{
Node vals[2];
bool bothBounds = true;
{
return true;
}
- else if (!options::cbqiMultiInst())
+ else if (!options::cegqiMultiInst())
{
return false;
}
// generally should not make it to this point, unless we are using a
// non-monotonic selection function
- if (!options::cbqiNopt())
+ if (!options::cegqiNopt())
{
// if not trying non-optimal bounds, return
return false;
for (unsigned j = 0, nbounds = d_mbp_bounds[rr].size(); j < nbounds; j++)
{
if ((int)j != best_used[rr]
- && (!options::cbqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull()))
+ && (!options::cegqiMidpoint() || d_mbp_vts_coeff[rr][1][j].isNull()))
{
Node val = getModelBasedProjectionValue(ci,
pv,
{
return true;
}
- else if (!options::cbqiMultiInst())
+ else if (!options::cegqiMultiInst())
{
return false;
}
<< "...bound type is : " << sf.d_props[index].d_type << std::endl;
// intger division rounding up if from a lower bound
if (sf.d_props[index].d_type == CEG_TT_UPPER
- && options::cbqiRoundUpLowerLia())
+ && options::cegqiRoundUpLowerLia())
{
sf.d_subs[index] = nm->mkNode(
PLUS,
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, options::cbqiBvSolveNl());
+ d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cegqiBvSolveNl());
if (!slit.isNull())
{
CegInstantiatorBvInverterQuery m(ci);
{
return Node::null();
}
- else if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::KEEP
+ else if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::KEEP
|| (pol && k == EQUAL))
{
return lit;
Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl;
Node ret;
- if (options::cbqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK)
+ if (options::cegqiBvIneqMode() == options::CbqiBvIneqMode::EQ_SLACK)
{
// if using slack, we convert constraints to a positive equality based on
// the current model M, e.g.:
{
// if option enabled, use approach for word-level inversion for BV
// instantiation
- if (options::cbqiBv())
+ if (options::cegqiBv())
{
// get the best rewritten form of lit for solving for pv
// this should remove instances of non-invertible operators, and
Node pv,
CegInstEffort effort)
{
- return effort < CEG_INST_EFFORT_FULL || options::cbqiFullEffort();
+ return effort < CEG_INST_EFFORT_FULL || options::cegqiFullEffort();
}
bool BvInstantiator::processAssertions(CegInstantiator* ci,
Trace("cegqi-bv") << "BvInstantiator::processAssertions for " << pv
<< std::endl;
// if interleaving, do not do inversion half the time
- if (options::cbqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
+ if (options::cegqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
{
Trace("cegqi-bv") << "...do not do instantiation for " << pv
<< " (skip, based on heuristic)" << std::endl;
// for constructing instantiations is exponential on the number of
// variables in this quantifier prefix.
bool ret = false;
- bool tryMultipleInst = firstVar && options::cbqiMultiInst();
+ bool tryMultipleInst = firstVar && options::cegqiMultiInst();
bool revertOnSuccess = tryMultipleInst;
for (unsigned j = 0, size = iti->second.size(); j < size; j++)
{
bv::utils::mkConst(BitVector(bv::utils::getSize(pv), Integer(2))));
}
- if (options::cbqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
+ if (options::cegqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
{
Node result = utils::normalizePvEqual(pv, children, contains_pv);
if (!result.isNull())
}
else if (n.getKind() == BITVECTOR_MULT || n.getKind() == BITVECTOR_PLUS)
{
- if (options::cbqiBvLinearize() && contains_pv[n])
+ if (options::cegqiBvLinearize() && contains_pv[n])
{
Node result;
if (n.getKind() == BITVECTOR_MULT)
// new lemmas
std::vector<Node> new_lems;
- if (options::cbqiBvRmExtract())
+ if (options::cegqiBvRmExtract())
{
NodeManager* nm = NodeManager::currentNM();
Trace("cegqi-bv-pp") << "-----remove extracts..." << std::endl;
if (curr < ret)
{
ret = curr;
- Trace("cbqi-debug2") << "Non-cbqi kind : " << cur.getKind()
+ Trace("cegqi-debug2") << "Non-cbqi kind : " << cur.getKind()
<< " in " << n << std::endl;
if (curr == CEG_UNHANDLED)
{
// if quantifier has a non-handled variable, then do not use cbqi
// if quantifier has an APPLY_UF term, then do not use cbqi unless EPR
CegHandledStatus ncbqiv = CegInstantiator::isCbqiQuantPrefix(q, qe);
- Trace("cbqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
+ Trace("cegqi-quant-debug") << "isCbqiQuantPrefix returned " << ncbqiv
<< std::endl;
if (ncbqiv == CEG_UNHANDLED)
{
else
{
CegHandledStatus cbqit = CegInstantiator::isCbqiTerm(q);
- Trace("cbqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl;
+ Trace("cegqi-quant-debug") << "isCbqiTerm returned " << cbqit << std::endl;
if (cbqit == CEG_UNHANDLED)
{
if (ncbqiv == CEG_HANDLED_UNCONDITIONAL)
ret = CEG_PARTIALLY_HANDLED;
}
}
- if (ret == CEG_UNHANDLED && options::cbqiAll())
+ if (ret == CEG_UNHANDLED && options::cegqiAll())
{
// try but not exclusively
ret = CEG_PARTIALLY_HANDLED;
d_vars.push_back(v);
d_vars_set.insert(v);
TypeNode vtn = v.getType();
- Trace("cbqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
+ Trace("cegqi-proc-debug") << "Collect theory ids from type " << vtn << " of "
<< v << std::endl;
// collect relevant theories for this variable
std::map<TypeNode, bool> visited;
}
// If the above call fails, resort to using value in model. We do so if:
// - we have yet to try an instantiation this round (or we are trying
- // multiple instantiations, indicated by options::cbqiMultiInst),
+ // multiple instantiations, indicated by options::cegqiMultiInst),
// - the instantiator uses model values at this effort or
// if we are solving for a subfield of a datatype (is_sv), and
// - the instantiator allows model values.
- if ((options::cbqiMultiInst() || !hasTriedInstantiation(pv))
+ if ((options::cegqiMultiInst() || !hasTriedInstantiation(pv))
&& (vinst->useModelValue(this, sf, pv, d_effort) || is_sv)
&& vinst->allowModelValue(this, sf, pv, d_effort))
{
// Quantified Linear Arithmetic by Counterexample Guided Instantiation",
// FMSD 2017. We throw an assertion failure if we detect a case where the
// strategy was not monotonic.
- if (options::cbqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
+ if (options::cegqiNestedQE() && d_qe->getLogicInfo().isPure(THEORY_ARITH)
&& d_qe->getLogicInfo().isLinear())
{
- Trace("cbqi-warn") << "Had to resort to model value." << std::endl;
+ Trace("cegqi-warn") << "Had to resort to model value." << std::endl;
Assert(false);
}
#endif
Node mv = getModelValue( pv );
TermProperties pv_prop_m;
- Trace("cbqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
+ Trace("cegqi-inst-debug") << "[4] " << i << "...try model value " << mv << std::endl;
d_curr_iphase[pv] = CEG_INST_PHASE_MVALUE;
CegInstEffort prev = d_effort;
if (d_effort < CEG_INST_EFFORT_STANDARD_MV)
d_effort = prev;
}
- Trace("cbqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
+ Trace("cegqi-inst-debug") << "[No instantiation found for " << pv << "]" << std::endl;
if (is_sv)
{
d_stack_vars.push_back( pv );
{
pvr = d_qe->getMasterEqualityEngine()->getRepresentative(pv);
}
- Trace("cbqi-inst-debug") << "[Find instantiation for " << pv
+ Trace("cegqi-inst-debug") << "[Find instantiation for " << pv
<< "], rep=" << pvr << ", instantiator is "
<< vinst->identify() << std::endl;
Node pv_value;
- if (options::cbqiModel())
+ if (options::cegqiModel())
{
pv_value = getModelValue(pv);
- Trace("cbqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
+ Trace("cegqi-bound2") << "...M( " << pv << " ) = " << pv_value << std::endl;
}
//[1] easy case : pv is in the equivalence class as another term not
// containing pv
if (vinst->hasProcessEqualTerm(this, sf, pv, d_effort))
{
- Trace("cbqi-inst-debug")
+ Trace("cegqi-inst-debug")
<< "[1] try based on equivalence class." << std::endl;
d_curr_iphase[pv] = CEG_INST_PHASE_EQC;
std::map<Node, std::vector<Node> >::iterator it_eqc = d_curr_eqc.find(pvr);
if (it_eqc != d_curr_eqc.end())
{
// std::vector< Node > eq_candidates;
- Trace("cbqi-inst-debug2")
+ Trace("cegqi-inst-debug2")
<< "...eqc has size " << it_eqc->second.size() << std::endl;
for (const Node& n : it_eqc->second)
{
if (n != pv)
{
- Trace("cbqi-inst-debug")
+ Trace("cegqi-inst-debug")
<< "...try based on equal term " << n << std::endl;
// must be an eligible term
if (isEligible(n))
{
return true;
}
- else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+ else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
{
return false;
}
{
return true;
}
- else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+ else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
{
return false;
}
}
else
{
- Trace("cbqi-inst-debug2") << "...eqc not found." << std::endl;
+ Trace("cegqi-inst-debug2") << "...eqc not found." << std::endl;
}
}
/// the variable
if (vinst->hasProcessEquality(this, sf, pv, d_effort))
{
- Trace("cbqi-inst-debug")
+ Trace("cegqi-inst-debug")
<< "[2] try based on solving equalities." << std::endl;
d_curr_iphase[pv] = CEG_INST_PHASE_EQUAL;
std::vector<Node>& cteqc = d_curr_type_eqc[pvtnb];
Assert(it_reqc != d_curr_eqc.end());
for (const Node& n : it_reqc->second)
{
- Trace("cbqi-inst-debug2") << "...look at term " << n << std::endl;
+ Trace("cegqi-inst-debug2") << "...look at term " << n << std::endl;
// must be an eligible term
if (isEligible(n))
{
if (!ns.isNull())
{
bool hasVar = d_prog_var[ns].find(pv) != d_prog_var[ns].end();
- Trace("cbqi-inst-debug2") << "... " << ns << " has var " << pv
+ Trace("cegqi-inst-debug2") << "... " << ns << " has var " << pv
<< " : " << hasVar << std::endl;
std::vector<TermProperties> term_props;
std::vector<Node> terms;
// if this term or the another has pv in it, try to solve for it
if (hasVar || lhs_v[j])
{
- Trace("cbqi-inst-debug") << "......try based on equality "
+ Trace("cegqi-inst-debug") << "......try based on equality "
<< lhs[j] << " = " << ns << std::endl;
term_props.push_back(lhs_prop[j]);
terms.push_back(lhs[j]);
{
return true;
}
- else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+ else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
{
return false;
}
}
else
{
- Trace("cbqi-inst-debug2")
+ Trace("cegqi-inst-debug2")
<< "... term " << n << " is ineligible after substitution."
<< std::endl;
}
}
else
{
- Trace("cbqi-inst-debug2")
+ Trace("cegqi-inst-debug2")
<< "... term " << n << " is ineligible." << std::endl;
}
}
{
return false;
}
- Trace("cbqi-inst-debug") << "[3] try based on assertions." << std::endl;
+ Trace("cegqi-inst-debug") << "[3] try based on assertions." << std::endl;
d_curr_iphase[pv] = CEG_INST_PHASE_ASSERTION;
std::unordered_set<Node, NodeHashFunction> lits;
for (unsigned r = 0; r < 2; r++)
{
TheoryId tid = r == 0 ? Theory::theoryOf(pvtn) : THEORY_UF;
- Trace("cbqi-inst-debug2") << " look at assertions of " << tid << std::endl;
+ Trace("cegqi-inst-debug2") << " look at assertions of " << tid << std::endl;
std::map<TheoryId, std::vector<Node> >::iterator ita =
d_curr_asserts.find(tid);
if (ita != d_curr_asserts.end())
{
lits.insert(lit);
Node plit;
- if (options::cbqiRepeatLit() || !isSolvedAssertion(lit))
+ if (options::cegqiRepeatLit() || !isSolvedAssertion(lit))
{
plit = vinst->hasProcessAssertion(this, sf, pv, lit, d_effort);
}
if (!plit.isNull())
{
- Trace("cbqi-inst-debug2") << " look at " << lit;
+ Trace("cegqi-inst-debug2") << " look at " << lit;
if (plit != lit)
{
- Trace("cbqi-inst-debug2") << "...processed to : " << plit;
+ Trace("cegqi-inst-debug2") << "...processed to : " << plit;
}
- Trace("cbqi-inst-debug2") << std::endl;
+ Trace("cegqi-inst-debug2") << std::endl;
// apply substitutions
Node slit = applySubstitutionToLiteral(plit, sf);
if (!slit.isNull())
// check if contains pv
if (hasVariable(slit, pv))
{
- Trace("cbqi-inst-debug")
+ Trace("cegqi-inst-debug")
<< "...try based on literal " << slit << "," << std::endl;
- Trace("cbqi-inst-debug") << "...from " << lit << std::endl;
+ Trace("cegqi-inst-debug") << "...from " << lit << std::endl;
if (vinst->processAssertion(this, sf, pv, slit, lit, d_effort))
{
return true;
}
- else if (!options::cbqiMultiInst() && hasTriedInstantiation(pv))
+ else if (!options::cegqiMultiInst() && hasTriedInstantiation(pv))
{
return false;
}
Node cnode = pv_prop.getCacheNode();
if( d_curr_subs_proc[pv][n].find( cnode )==d_curr_subs_proc[pv][n].end() ){
d_curr_subs_proc[pv][n][cnode] = true;
- if( Trace.isOn("cbqi-inst-debug") ){
+ if( Trace.isOn("cegqi-inst-debug") ){
for( unsigned j=0; j<sf.d_subs.size(); j++ ){
- Trace("cbqi-inst-debug") << " ";
+ Trace("cegqi-inst-debug") << " ";
}
- Trace("cbqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
+ Trace("cegqi-inst-debug") << sf.d_subs.size() << ": (" << d_curr_iphase[pv]
<< ") ";
Node mod_pv = pv_prop.getModifiedTerm( pv );
- Trace("cbqi-inst-debug") << mod_pv << " -> " << n << std::endl;
+ Trace("cegqi-inst-debug") << mod_pv << " -> " << n << std::endl;
Assert(n.getType().isSubtypeOf(pv.getType()));
}
//must ensure variables have been computed for n
std::map< int, TermProperties > prev_prop;
std::map< int, Node > prev_sym_subs;
std::vector< Node > new_non_basic;
- Trace("cbqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
+ Trace("cegqi-inst-debug2") << "Applying substitutions to previous substitution terms..." << std::endl;
for( unsigned j=0; j<sf.d_subs.size(); j++ ){
- Trace("cbqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl;
+ Trace("cegqi-inst-debug2") << " Apply for " << sf.d_subs[j] << std::endl;
Assert(d_prog_var.find(sf.d_subs[j]) != d_prog_var.end());
if( d_prog_var[sf.d_subs[j]].find( pv )!=d_prog_var[sf.d_subs[j]].end() ){
prev_subs[j] = sf.d_subs[j];
computeProgVars( sf.d_subs[j] );
Assert(d_inelig.find(sf.d_subs[j]) == d_inelig.end());
}
- Trace("cbqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
+ Trace("cegqi-inst-debug2") << "Subs " << j << " " << sf.d_subs[j] << std::endl;
}else{
- Trace("cbqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
+ Trace("cegqi-inst-debug2") << "...failed to apply substitution to " << sf.d_subs[j] << std::endl;
success = false;
break;
}
}else{
- Trace("cbqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
+ Trace("cegqi-inst-debug2") << "Skip " << j << " " << sf.d_subs[j] << std::endl;
}
}
if( success ){
- Trace("cbqi-inst-debug2") << "Adding to vectors..." << std::endl;
+ Trace("cegqi-inst-debug2") << "Adding to vectors..." << std::endl;
sf.push_back( pv, n, pv_prop );
- Trace("cbqi-inst-debug2") << "Recurse..." << std::endl;
+ Trace("cegqi-inst-debug2") << "Recurse..." << std::endl;
unsigned i = d_curr_index[pv];
success = constructInstantiation(sf, d_stack_vars.empty() ? i + 1 : i);
if (!success || revertOnSuccess)
{
- Trace("cbqi-inst-debug2") << "Removing from vectors..." << std::endl;
+ Trace("cegqi-inst-debug2") << "Removing from vectors..." << std::endl;
sf.pop_back( pv, n, pv_prop );
}
}
{
return true;
}else{
- Trace("cbqi-inst-debug2") << "Revert substitutions..." << std::endl;
+ Trace("cegqi-inst-debug2") << "Revert substitutions..." << std::endl;
//revert substitution information
for (std::map<int, Node>::iterator it = prev_subs.begin();
it != prev_subs.end();
bool CegInstantiator::doAddInstantiation( std::vector< Node >& vars, std::vector< Node >& subs, std::vector< Node >& lemmas ) {
if (vars.size() > d_input_vars.size() || !d_var_order_index.empty())
{
- Trace("cbqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
+ Trace("cegqi-inst-debug") << "Reconstructing instantiations...." << std::endl;
std::map< Node, Node > subs_map;
for( unsigned i=0; i<subs.size(); i++ ){
subs_map[vars[i]] = subs[i];
std::map<Node, Node>::iterator it = subs_map.find(d_input_vars[i]);
Assert(it != subs_map.end());
Node n = it->second;
- Trace("cbqi-inst-debug") << " " << d_input_vars[i] << " -> " << n
+ Trace("cegqi-inst-debug") << " " << d_input_vars[i] << " -> " << n
<< std::endl;
Assert(n.getType().isSubtypeOf(d_input_vars[i].getType()));
subs.push_back( n );
}
}
- if (Trace.isOn("cbqi-inst"))
+ if (Trace.isOn("cegqi-inst"))
{
- Trace("cbqi-inst") << "Ceg Instantiator produced : " << std::endl;
+ Trace("cegqi-inst") << "Ceg Instantiator produced : " << std::endl;
for (unsigned i = 0, size = d_input_vars.size(); i < size; ++i)
{
Node v = d_input_vars[i];
- Trace("cbqi-inst") << i << " (" << d_curr_iphase[v] << ") : "
+ Trace("cegqi-inst") << i << " (" << d_curr_iphase[v] << ") : "
<< v << " -> " << subs[i] << std::endl;
Assert(subs[i].getType().isSubtypeOf(v.getType()));
}
}
- Trace("cbqi-inst-debug") << "Do the instantiation...." << std::endl;
+ Trace("cegqi-inst-debug") << "Do the instantiation...." << std::endl;
bool ret = d_parent->doAddInstantiation(subs);
for( unsigned i=0; i<lemmas.size(); i++ ){
d_parent->addLemma(lemmas[i]);
n = Rewriter::rewrite(n);
computeProgVars( n );
bool is_basic = canApplyBasicSubstitution( n, non_basic );
- if( Trace.isOn("cegqi-si-apply-subs-debug") ){
- Trace("cegqi-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl;
+ if( Trace.isOn("sygus-si-apply-subs-debug") ){
+ Trace("sygus-si-apply-subs-debug") << "is_basic = " << is_basic << " " << tn << std::endl;
for( unsigned i=0; i<subs.size(); i++ ){
- Trace("cegqi-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
+ Trace("sygus-si-apply-subs-debug") << " " << vars[i] << " -> " << subs[i] << " types : " << vars[i].getType() << " -> " << subs[i].getType() << std::endl;
Assert(subs[i].getType().isSubtypeOf(vars[i].getType()));
}
}
//make sum with normalized coefficient
if( !pv_prop.d_coeff.isNull() ){
pv_prop.d_coeff = Rewriter::rewrite( pv_prop.d_coeff );
- Trace("cegqi-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
+ Trace("sygus-si-apply-subs-debug") << "Combined coeff : " << pv_prop.d_coeff << std::endl;
std::vector< Node > children;
for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){
Node c_coeff;
c = NodeManager::currentNM()->mkNode( MULT, c_coeff, msum_term[it->first] );
}
children.push_back( c );
- Trace("cegqi-si-apply-subs-debug") << "Add child : " << c << std::endl;
+ Trace("sygus-si-apply-subs-debug") << "Add child : " << c << std::endl;
}
Node nretc = children.size()==1 ? children[0] : NodeManager::currentNM()->mkNode( PLUS, children );
nretc = Rewriter::rewrite( nretc );
//result is ( nret / pv_prop.d_coeff )
nret = nretc;
}else{
- Trace("cegqi-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
+ Trace("sygus-si-apply-subs-debug") << "Failed, since result " << nretc << " contains free variable." << std::endl;
}
}else{
//implies that we have a monomial that has a free variable
- Trace("cegqi-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl;
+ Trace("sygus-si-apply-subs-debug") << "Failed to find coefficient during substitution, implies monomial with free variable." << std::endl;
}
}else{
- Trace("cegqi-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
+ Trace("sygus-si-apply-subs-debug") << "Failed to find monomial sum " << n << std::endl;
}
}
}
return true;
}
}
- Trace("cbqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
+ Trace("cegqi-engine") << " WARNING : unable to find CEGQI single invocation instantiation." << std::endl;
return false;
}
== it->second.end())
{
it->second.push_back(nn);
- Trace("cbqi-presolve") << " - " << n[i] << " = " << nn << std::endl;
+ Trace("cegqi-presolve") << " - " << n[i] << " = " << nn << std::endl;
}
}
}
Node lem = conj.size()==1 ? conj[0] : NodeManager::currentNM()->mkNode( AND, conj );
Node g = NodeManager::currentNM()->mkSkolem( "g", NodeManager::currentNM()->booleanType() );
lem = NodeManager::currentNM()->mkNode( OR, g, lem );
- Trace("cbqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
+ Trace("cegqi-presolve-debug") << "Presolve lemma : " << lem << std::endl;
Assert(!expr::hasFreeVar(lem));
d_qe->getOutputChannel().lemma( lem, false, true );
}
}
void CegInstantiator::processAssertions() {
- Trace("cbqi-proc") << "--- Process assertions, #var = " << d_vars.size()
+ Trace("cegqi-proc") << "--- Process assertions, #var = " << d_vars.size()
<< std::endl;
d_curr_asserts.clear();
d_curr_eqc.clear();
for( unsigned i=0; i<d_vars.size(); i++ ){
Node pv = d_vars[i];
TypeNode pvtn = pv.getType();
- Trace("cbqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
+ Trace("cegqi-proc-debug") << "Collect theory ids from type " << pvtn << " of " << pv << std::endl;
//collect information about eqc
if( ee->hasTerm( pv ) ){
Node pvr = ee->getRepresentative( pv );
if( d_curr_eqc.find( pvr )==d_curr_eqc.end() ){
- Trace("cbqi-proc") << "Collect equivalence class " << pvr << std::endl;
+ Trace("cegqi-proc") << "Collect equivalence class " << pvr << std::endl;
eq::EqClassIterator eqc_i = eq::EqClassIterator( pvr, ee );
while( !eqc_i.isFinished() ){
d_curr_eqc[pvr].push_back( *eqc_i );
TheoryId tid = d_tids[i];
Theory* theory = d_qe->getTheoryEngine()->theoryOf( tid );
if( theory && d_qe->getTheoryEngine()->isTheoryEnabled(tid) ){
- Trace("cbqi-proc") << "Collect assertions from theory " << tid << std::endl;
+ Trace("cegqi-proc") << "Collect assertions from theory " << tid << std::endl;
d_curr_asserts[tid].clear();
//collect all assertions from theory
for( context::CDList<Assertion>::const_iterator it = theory->facts_begin(); it != theory->facts_end(); ++ it) {
Node atom = lit.getKind()==NOT ? lit[0] : lit;
if( d_is_nested_quant || std::find( d_ce_atoms.begin(), d_ce_atoms.end(), atom )!=d_ce_atoms.end() ){
d_curr_asserts[tid].push_back( lit );
- Trace("cbqi-proc-debug") << "...add : " << lit << std::endl;
+ Trace("cegqi-proc-debug") << "...add : " << lit << std::endl;
}else{
- Trace("cbqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
+ Trace("cegqi-proc") << "...do not consider literal " << tid << " : " << lit << " since it is not part of CE body." << std::endl;
}
}
}
}
//collect equivalence classes that correspond to relevant theories
- Trace("cbqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
+ Trace("cegqi-proc-debug") << "...collect typed equivalence classes" << std::endl;
eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee );
while( !eqcs_i.isFinished() ){
Node r = *eqcs_i;
if( rtn.isInteger() || rtn.isReal() ){
rtn = rtn.getBaseType();
}
- Trace("cbqi-proc-debug") << "...type eqc: " << r << std::endl;
+ Trace("cegqi-proc-debug") << "...type eqc: " << r << std::endl;
d_curr_type_eqc[rtn].push_back( r );
if( d_curr_eqc.find( r )==d_curr_eqc.end() ){
- Trace("cbqi-proc") << "Collect equivalence class " << r << std::endl;
- Trace("cbqi-proc-debug") << " ";
+ Trace("cegqi-proc") << "Collect equivalence class " << r << std::endl;
+ Trace("cegqi-proc-debug") << " ";
eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
- Trace("cbqi-proc-debug") << *eqc_i << " ";
+ Trace("cegqi-proc-debug") << *eqc_i << " ";
d_curr_eqc[r].push_back( *eqc_i );
++eqc_i;
}
- Trace("cbqi-proc-debug") << std::endl;
+ Trace("cegqi-proc-debug") << std::endl;
}
}
++eqcs_i;
if( isEligible( n ) ){
//must contain at least one variable
if( !d_prog_var[n].empty() ){
- Trace("cbqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
+ Trace("cegqi-proc") << "...literal[" << it->first << "] : " << n << std::endl;
akeep.push_back( n );
}else{
- Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
+ Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains no relevant variables." << std::endl;
}
}else{
- Trace("cbqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
+ Trace("cegqi-proc") << "...remove literal from " << it->first << " : " << n << " since it contains ineligible terms." << std::endl;
}
}
it->second.clear();
}
}else{
if( std::find( d_ce_atoms.begin(), d_ce_atoms.end(), n )==d_ce_atoms.end() ){
- Trace("cbqi-ce-atoms") << "CE atoms : " << n << std::endl;
+ Trace("cegqi-ce-atoms") << "CE atoms : " << n << std::endl;
d_ce_atoms.push_back( n );
}
}
}
void CegInstantiator::registerCounterexampleLemma( std::vector< Node >& lems, std::vector< Node >& ce_vars ) {
- Trace("cbqi-reg") << "Register counterexample lemma..." << std::endl;
+ Trace("cegqi-reg") << "Register counterexample lemma..." << std::endl;
d_input_vars.clear();
d_input_vars.insert(d_input_vars.end(), ce_vars.begin(), ce_vars.end());
registerTheoryId(THEORY_UF);
for (unsigned i = 0; i < ce_vars.size(); i++)
{
- Trace("cbqi-reg") << " register input variable : " << ce_vars[i] << std::endl;
+ Trace("cegqi-reg") << " register input variable : " << ce_vars[i] << std::endl;
registerVariable(ce_vars[i]);
}
// preprocess with all relevant instantiator preprocessors
- Trace("cbqi-debug") << "Preprocess based on theory-specific methods..."
+ Trace("cegqi-debug") << "Preprocess based on theory-specific methods..."
<< std::endl;
std::vector<Node> pvars;
pvars.insert(pvars.end(), d_vars.begin(), d_vars.end());
p.second->registerCounterexampleLemma(lems, pvars);
}
// must register variables generated by preprocessors
- Trace("cbqi-debug") << "Register variables from theory-specific methods "
+ Trace("cegqi-debug") << "Register variables from theory-specific methods "
<< d_input_vars.size() << " " << pvars.size() << " ..."
<< std::endl;
for (unsigned i = d_input_vars.size(), size = pvars.size(); i < size; ++i)
{
- Trace("cbqi-reg") << " register theory preprocess variable : " << pvars[i]
+ Trace("cegqi-reg") << " register theory preprocess variable : " << pvars[i]
<< std::endl;
registerVariable(pvars[i]);
}
IteSkolemMap iteSkolemMap;
d_qe->getTheoryEngine()->getTermFormulaRemover()->run(lems, iteSkolemMap);
for(IteSkolemMap::iterator i = iteSkolemMap.begin(); i != iteSkolemMap.end(); ++i) {
- Trace("cbqi-reg") << " register aux variable : " << i->first << std::endl;
+ Trace("cegqi-reg") << " register aux variable : " << i->first << std::endl;
registerVariable(i->first);
}
for( unsigned i=0; i<lems.size(); i++ ){
- Trace("cbqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
+ Trace("cegqi-debug") << "Counterexample lemma (pre-rewrite) " << i << " : " << lems[i] << std::endl;
Node rlem = lems[i];
rlem = Rewriter::rewrite( rlem );
// also must preprocess to ensure that the counterexample atoms we
// collect below are identical to the atoms that we add to the CNF stream
rlem = d_qe->getTheoryEngine()->preprocess(rlem);
- Trace("cbqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
+ Trace("cegqi-debug") << "Counterexample lemma (post-rewrite) " << i << " : " << rlem << std::endl;
lems[i] = rlem;
}
// determine variable order: must do Reals before Ints
- Trace("cbqi-debug") << "Determine variable order..." << std::endl;
+ Trace("cegqi-debug") << "Determine variable order..." << std::endl;
if (!d_vars.empty())
{
std::map<Node, unsigned> voo;
}
if (doSort)
{
- Trace("cbqi-debug") << "Sort variables based on ordering." << std::endl;
+ Trace("cegqi-debug") << "Sort variables based on ordering." << std::endl;
for (std::pair<const TypeNode, std::vector<Node> >& vs : tvars)
{
vars.insert(vars.end(), vs.second.begin(), vs.second.end());
}
- Trace("cbqi-debug") << "Consider variables in this order : " << std::endl;
+ Trace("cegqi-debug") << "Consider variables in this order : " << std::endl;
for (unsigned i = 0; i < vars.size(); i++)
{
d_var_order_index[voo[vars[i]]] = i;
- Trace("cbqi-debug") << " " << vars[i] << " : " << vars[i].getType()
+ Trace("cegqi-debug") << " " << vars[i] << " : " << vars[i].getType()
<< ", index was : " << voo[vars[i]] << std::endl;
d_vars[i] = vars[i];
}
- Trace("cbqi-debug") << std::endl;
+ Trace("cegqi-debug") << std::endl;
}
else
{
d_small_const =
NodeManager::currentNM()->mkConst(Rational(1) / Rational(1000000));
d_check_vts_lemma_lc = false;
- if (options::cbqiBv())
+ if (options::cegqiBv())
{
// if doing instantiation for BV, need the inverter class
d_bv_invert.reset(new quantifiers::BvInverter);
if( !hasAddedCbqiLemma( q ) ){
NodeManager* nm = NodeManager::currentNM();
d_added_cbqi_lemma.insert( q );
- Trace("cbqi-debug") << "Do cbqi for " << q << std::endl;
+ Trace("cegqi-debug") << "Do cbqi for " << q << std::endl;
//add cbqi lemma
//get the counterexample literal
Node ceLit = getCounterexampleLiteral(q);
Node lem = NodeManager::currentNM()->mkNode( OR, ceLit.negate(), ceBody.negate() );
//require any decision on cel to be phase=true
d_quantEngine->addRequirePhase( ceLit, true );
- Debug("cbqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
+ Debug("cegqi-debug") << "Require phase " << ceLit << " = true." << std::endl;
//add counterexample lemma
lem = Rewriter::rewrite( lem );
- Trace("cbqi-lemma") << "Counterexample lemma : " << lem << std::endl;
+ Trace("cegqi-lemma") << "Counterexample lemma : " << lem << std::endl;
registerCounterexampleLemma( q, lem );
//totality lemmas for EPR
disj.push_back( ic.eqNode( itc->second[j] ) );
}
Node tlem = disj.size()==1 ? disj[0] : NodeManager::currentNM()->mkNode( kind::OR, disj );
- Trace("cbqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
+ Trace("cegqi-lemma") << "EPR totality lemma : " << tlem << std::endl;
d_quantEngine->getOutputChannel().lemma( tlem );
}else{
Assert(false);
if (!dep.empty())
{
Node dep_lemma = nm->mkNode(IMPLIES, ceLit, nm->mkNode(AND, dep));
- Trace("cbqi-lemma")
+ Trace("cegqi-lemma")
<< "Counterexample dependency lemma : " << dep_lemma << std::endl;
d_quantEngine->getOutputChannel().lemma(dep_lemma);
}
if( doCbqi( quants[i] ) ){
registerCbqiLemma( quants[i] );
}
- if( options::cbqiNestedQE() ){
+ if( options::cegqiNestedQE() ){
//record these as counterexample quantifiers
QAttributes qa;
QuantAttributes::computeQuantAttributes( quants[i], qa );
if( !qa.d_qid_num.isNull() ){
d_id_to_ce_quant[ qa.d_qid_num ] = quants[i];
d_ce_quant_to_id[ quants[i] ] = qa.d_qid_num;
- Trace("cbqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
+ Trace("cegqi-nqe") << "CE quant id = " << qa.d_qid_num << " is " << quants[i] << std::endl;
}
}
}
Assert(hasAddedCbqiLemma(q));
if( d_quantEngine->getModel()->isQuantifierActive( q ) ){
d_active_quant[q] = true;
- Debug("cbqi-debug") << "Check quantified formula " << q << "..." << std::endl;
+ Debug("cegqi-debug") << "Check quantified formula " << q << "..." << std::endl;
Node cel = getCounterexampleLiteral(q);
bool value;
if( d_quantEngine->getValuation().hasSatValue( cel, value ) ){
- Debug("cbqi-debug") << "...CE Literal has value " << value << std::endl;
+ Debug("cegqi-debug") << "...CE Literal has value " << value << std::endl;
if( !value ){
if( d_quantEngine->getValuation().isDecision( cel ) ){
- Trace("cbqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
+ Trace("cegqi-warn") << "CBQI WARNING: Bad decision on CE Literal." << std::endl;
}else{
- Trace("cbqi") << "Inactive : " << q << std::endl;
+ Trace("cegqi") << "Inactive : " << q << std::endl;
d_quantEngine->getModel()->setQuantifierActive( q, false );
d_cbqi_set_quant_inactive = true;
d_active_quant.erase( q );
d_elim_quants.insert( q );
- Trace("cbqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
+ Trace("cegqi-nqe") << "Inactive, waitlist proc/size = " << d_nested_qe_waitlist_proc[q].get() << "/" << d_nested_qe_waitlist_size[q].get() << std::endl;
//process from waitlist
while( d_nested_qe_waitlist_proc[q]<d_nested_qe_waitlist_size[q] ){
int index = d_nested_qe_waitlist_proc[q];
Node nq = d_nested_qe_waitlist[q][index];
Node nqeqn = doNestedQENode( d_nested_qe_info[nq].d_q, q, nq, d_nested_qe_info[nq].d_inst_terms, d_nested_qe_info[nq].d_doVts );
Node dqelem = nq.eqNode( nqeqn );
- Trace("cbqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
+ Trace("cegqi-lemma") << "Delayed nested quantifier elimination lemma : " << dqelem << std::endl;
d_quantEngine->getOutputChannel().lemma( dqelem );
d_nested_qe_waitlist_proc[q] = index + 1;
}
}
}
}else{
- Debug("cbqi-debug") << "...CE Literal does not have value " << std::endl;
+ Debug("cegqi-debug") << "...CE Literal does not have value " << std::endl;
}
}
}
}
//refinement: only consider innermost active quantified formulas
- if( options::cbqiInnermost() ){
+ if( options::cegqiInnermost() ){
if( !d_children_quant.empty() && !d_active_quant.empty() ){
- Trace("cbqi-debug") << "Find non-innermost quantifiers..." << std::endl;
+ Trace("cegqi-debug") << "Find non-innermost quantifiers..." << std::endl;
std::vector< Node > ninner;
for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
std::map< Node, std::vector< Node > >::iterator itc = d_children_quant.find( it->first );
if( itc!=d_children_quant.end() ){
for( unsigned j=0; j<itc->second.size(); j++ ){
if( d_active_quant.find( itc->second[j] )!=d_active_quant.end() ){
- Trace("cbqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
+ Trace("cegqi-debug") << "Do not consider " << it->first << " since it is not innermost (" << itc->second[j] << std::endl;
ninner.push_back( it->first );
break;
}
}
}
}
- Trace("cbqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
+ Trace("cegqi-debug") << "Found " << ninner.size() << " non-innermost." << std::endl;
for( unsigned i=0; i<ninner.size(); i++ ){
Assert(d_active_quant.find(ninner[i]) != d_active_quant.end());
d_active_quant.erase( ninner[i] );
}
Assert(!d_active_quant.empty());
- Trace("cbqi-debug") << "...done removing." << std::endl;
+ Trace("cegqi-debug") << "...done removing." << std::endl;
}
}
d_check_vts_lemma_lc = false;
{
Assert(!d_quantEngine->inConflict());
double clSet = 0;
- if( Trace.isOn("cbqi-engine") ){
+ if( Trace.isOn("cegqi-engine") ){
clSet = double(clock())/double(CLOCKS_PER_SEC);
- Trace("cbqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
+ Trace("cegqi-engine") << "---Cbqi Engine Round, effort = " << e << "---" << std::endl;
}
unsigned lastWaiting = d_quantEngine->getNumLemmasWaiting();
for( int ee=0; ee<=1; ee++ ){
// if( doCbqi( q ) && d_quantEngine->getModel()->isQuantifierActive( q ) ){
for( std::map< Node, bool >::iterator it = d_active_quant.begin(); it != d_active_quant.end(); ++it ){
Node q = it->first;
- Trace("cbqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
+ Trace("cegqi") << "CBQI : Process quantifier " << q[0] << " at effort " << ee << std::endl;
if( d_nested_qe.find( q )==d_nested_qe.end() ){
process( q, e, ee );
if( d_quantEngine->inConflict() ){
break;
}
}else{
- Trace("cbqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
+ Trace("cegqi-warn") << "CBQI : Cannot process already eliminated quantified formula " << q << std::endl;
Assert(false);
}
}
break;
}
}
- if( Trace.isOn("cbqi-engine") ){
+ if( Trace.isOn("cegqi-engine") ){
if( d_quantEngine->getNumLemmasWaiting()>lastWaiting ){
- Trace("cbqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
+ Trace("cegqi-engine") << "Added lemmas = " << (d_quantEngine->getNumLemmasWaiting()-lastWaiting) << std::endl;
}
double clSet2 = double(clock())/double(CLOCKS_PER_SEC);
- Trace("cbqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
+ Trace("cegqi-engine") << "Finished cbqi engine, time = " << (clSet2-clSet) << std::endl;
}
}
}
bool InstStrategyCegqi::checkComplete()
{
- if( ( !options::cbqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
+ if( ( !options::cegqiSat() && d_cbqi_set_quant_inactive ) || d_incomplete_check ){
return false;
}else{
return true;
void InstStrategyCegqi::preRegisterQuantifier(Node q)
{
// mark all nested quantifiers with id
- if (options::cbqiNestedQE())
+ if (options::cegqiNestedQE())
{
if( d_quantEngine->getOwner(q)==this )
{
}
Node qq = NodeManager::currentNM()->mkNode(FORALL, qqc);
Node mlem = NodeManager::currentNM()->mkNode(IMPLIES, q, qq);
- Trace("cbqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
+ Trace("cegqi-lemma") << "Mark quant id lemma : " << mlem << std::endl;
d_quantEngine->addLemma(mlem);
}
}
}
if( doCbqi( q ) ){
// get the instantiator
- if (options::cbqiPreRegInst())
+ if (options::cegqiPreRegInst())
{
getInstantiator(q);
}
// register the cbqi lemma
if( registerCbqiLemma( q ) ){
- Trace("cbqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
+ Trace("cegqi") << "Registered cbqi lemma for quantifier : " << q << std::endl;
}
}
}
inst = d_vtsCache->rewriteVtsSymbols(inst);
Trace("quant-vts-debug") << "...got " << inst << std::endl;
}
- if (options::cbqiNestedQE())
+ if (options::cegqiNestedQE())
{
inst = doNestedQE(q, terms, inst, doVts);
}
// in this case, q is equivalent to the quantifier-free formula C[t].
if( d_nested_qe.find( ceq )==d_nested_qe.end() ){
d_nested_qe[ceq] = d_quantEngine->getInstantiatedConjunction( ceq );
- Trace("cbqi-nqe") << "CE quantifier elimination : " << std::endl;
- Trace("cbqi-nqe") << " " << ceq << std::endl;
- Trace("cbqi-nqe") << " " << d_nested_qe[ceq] << std::endl;
+ Trace("cegqi-nqe") << "CE quantifier elimination : " << std::endl;
+ Trace("cegqi-nqe") << " " << ceq << std::endl;
+ Trace("cegqi-nqe") << " " << d_nested_qe[ceq] << std::endl;
//should not contain quantifiers
Assert(!expr::hasClosure(d_nested_qe[ceq]));
}
ret = Rewriter::rewrite( ret );
ret = d_vtsCache->rewriteVtsSymbols(ret);
}
- Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl;
- Trace("cbqi-nqe") << " " << n << std::endl;
- Trace("cbqi-nqe") << " " << ret << std::endl;
+ Trace("cegqi-nqe") << "Nested quantifier elimination: " << std::endl;
+ Trace("cegqi-nqe") << " " << n << std::endl;
+ Trace("cegqi-nqe") << " " << ret << std::endl;
return ret;
}
if( doNestedQe ){
ret = doNestedQENode( q, ceq, n, inst_terms, doVts );
}else{
- Trace("cbqi-nqe") << "Add to nested qe waitlist : " << std::endl;
+ Trace("cegqi-nqe") << "Add to nested qe waitlist : " << std::endl;
Node nr = Rewriter::rewrite( n );
- Trace("cbqi-nqe") << " " << ceq << std::endl;
- Trace("cbqi-nqe") << " " << nr << std::endl;
+ Trace("cegqi-nqe") << " " << ceq << std::endl;
+ Trace("cegqi-nqe") << " " << nr << std::endl;
int wlsize = d_nested_qe_waitlist_size[ceq] + 1;
d_nested_qe_waitlist_size[ceq] = wlsize;
if( wlsize<(int)d_nested_qe_waitlist[ceq].size() ){
d_nested_qe_info[nr].d_inst_terms.insert( d_nested_qe_info[nr].d_inst_terms.end(), inst_terms.begin(), inst_terms.end() );
d_nested_qe_info[nr].d_doVts = doVts;
//TODO: ensure this holds by restricting prenex when cbqiNestedQe is true.
- Assert(!options::cbqiInnermost());
+ Assert(!options::cegqiInnermost());
}
}
}
cinst->registerCounterexampleLemma(lems, ce_vars);
for (unsigned i = 0, size = lems.size(); i < size; i++)
{
- Trace("cbqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
+ Trace("cegqi-debug") << "Counterexample lemma " << i << " : " << lems[i]
<< std::endl;
d_quantEngine->addLemma(lems[i], false);
}
std::map<Node, CegHandledStatus>::iterator it = d_do_cbqi.find(q);
if( it==d_do_cbqi.end() ){
CegHandledStatus ret = CegInstantiator::isCbqiQuant(q, d_quantEngine);
- Trace("cbqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
+ Trace("cegqi-quant") << "doCbqi " << q << " returned " << ret << std::endl;
d_do_cbqi[q] = ret;
return ret != CEG_UNHANDLED;
}
return true;
}else{
//this should never happen for monotonic selection strategies
- Trace("cbqi-warn") << "WARNING: Existing instantiation" << std::endl;
+ Trace("cegqi-warn") << "WARNING: Existing instantiation" << std::endl;
return false;
}
}
}
void InstStrategyCegqi::presolve() {
- if (!options::cbqiPreRegInst())
+ if (!options::cegqiPreRegInst())
{
return;
}
for (std::pair<const Node, std::unique_ptr<CegInstantiator>>& ci : d_cinst)
{
- Trace("cbqi-presolve") << "Presolve " << ci.first << std::endl;
+ Trace("cegqi-presolve") << "Presolve " << ci.first << std::endl;
ci.second->presolve(ci.first);
}
}
using namespace CVC4::theory::inst;
bool CandidateGenerator::isLegalCandidate( Node n ){
- return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
+ return d_qe->getTermDatabase()->isTermActive( n ) && ( !options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(n) );
}
CandidateGeneratorQE::CandidateGeneratorQE(QuantifiersEngine* qe, Node pat)
Assert(Trigger::isSimpleTrigger(d_match_pattern));
for( unsigned i=0; i<d_match_pattern.getNumChildren(); i++ ){
if( d_match_pattern[i].getKind()==INST_CONSTANT ){
- if( !options::cbqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
+ if( !options::cegqi() || quantifiers::TermUtil::getInstConstAttr(d_match_pattern[i])==q ){
d_var_num[i] = d_match_pattern[i].getAttribute(InstVarNumAttribute());
}else{
d_var_num[i] = -1;
int index,
TypeNode v_tn)
{
- if( options::cbqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject
+ if( options::cegqi() && quantifiers::TermUtil::hasInstConstAttr(n) ){ //reject
return -2;
}else if( !n.getType().isSubtypeOf( v_tn ) ){ //reject if incorrect type
return -2;
for (unsigned j = 0; j < ts; j++)
{
Node gt = tdb->getTypeGroundTerm(ftypes[i], j);
- if (!options::cbqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
+ if (!options::cegqi() || !quantifiers::TermUtil::hasInstConstAttr(gt))
{
Node rep = qy->getRepresentative(gt);
if (reps_found.find(rep) == reps_found.end())
<< std::endl;
bad_inst = true;
}
- else if (options::cbqi())
+ else if (options::cegqi())
{
Node icf = quantifiers::TermUtil::getInstConstAttr(terms[i]);
if (!icf.isNull())
if (tdb->hasTermCurrent(r))
{
TypeNode rtn = r.getType();
- if (!options::cbqi() || !TermUtil::hasInstConstAttr(r))
+ if (!options::cegqi() || !TermUtil::hasInstConstAttr(r))
{
d_eqcs[rtn].push_back(r);
}
Assert(d_quant.isNull());
d_quant = q;
d_simp_quant = q;
- Trace("cegqi-si") << "CegSingleInv::initialize : " << q << std::endl;
+ Trace("sygus-si") << "CegSingleInv::initialize : " << q << std::endl;
// infer single invocation-ness
// get the variables
// process the single invocation-ness of the property
if (!d_sip->init(progs, qq))
{
- Trace("cegqi-si") << "...not single invocation (type mismatch)"
+ Trace("sygus-si") << "...not single invocation (type mismatch)"
<< std::endl;
return;
}
- Trace("cegqi-si") << "- Partitioned to single invocation parts : "
+ Trace("sygus-si") << "- Partitioned to single invocation parts : "
<< std::endl;
- d_sip->debugPrint("cegqi-si");
+ d_sip->debugPrint("sygus-si");
// map from program to bound variables
std::vector<Node> funcs;
return;
}
// if we are doing invariant templates, then construct the template
- Trace("cegqi-si") << "- Do transition inference..." << std::endl;
+ Trace("sygus-si") << "- Do transition inference..." << std::endl;
d_ti[q].process(qq, q[0][0]);
Trace("cegqi-inv") << std::endl;
Node prog = d_ti[q].getFunction();
.negate();
d_simp_quant = Rewriter::rewrite(d_simp_quant);
d_simp_quant = nm->mkNode(FORALL, q[0], d_simp_quant, q[2]);
- Trace("cegqi-si") << "Rewritten quantifier : " << d_simp_quant << std::endl;
+ Trace("sygus-si") << "Rewritten quantifier : " << d_simp_quant << std::endl;
// construct template argument
d_templ_arg[prog] = nm->mkSkolem("I", invariant.getType());
void CegSingleInv::finishInit(bool syntaxRestricted)
{
- Trace("cegqi-si-debug") << "Single invocation: finish init" << std::endl;
+ Trace("sygus-si-debug") << "Single invocation: finish init" << std::endl;
// do not do single invocation if grammar is restricted and
// options::CegqiSingleInvMode::ALL is not enabled
if (options::cegqiSingleInvMode() == options::CegqiSingleInvMode::USE
&& d_single_invocation && syntaxRestricted)
{
d_single_invocation = false;
- Trace("cegqi-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
+ Trace("sygus-si") << "...grammar is restricted, do not use single invocation techniques." << std::endl;
}
// we now have determined whether we will do single invocation techniques
if (!d_single_invocation)
{
d_single_inv = Node::null();
- Trace("cegqi-si") << "Formula is not single invocation." << std::endl;
+ Trace("sygus-si") << "Formula is not single invocation." << std::endl;
if (options::cegqiSingleInvAbort())
{
std::stringstream ss;
sivars.end(),
d_single_inv_arg_sk.begin(),
d_single_inv_arg_sk.end());
- Trace("cegqi-si") << "Single invocation formula is : " << d_single_inv
+ Trace("sygus-si") << "Single invocation formula is : " << d_single_inv
<< std::endl;
// check whether we can handle this quantified formula
CegHandledStatus status = CEG_HANDLED;
status = CegInstantiator::isCbqiQuant(d_single_inv);
}
}
- Trace("cegqi-si") << "CegHandledStatus is " << status << std::endl;
+ Trace("sygus-si") << "CegHandledStatus is " << status << std::endl;
if (status < CEG_HANDLED)
{
- Trace("cegqi-si") << "...do not invoke single invocation techniques since "
+ Trace("sygus-si") << "...do not invoke single invocation techniques since "
"the quantified formula does not have a handled "
"counterexample-guided instantiation strategy!"
<< std::endl;
// already solved, probably via a call to solveTrivial.
return true;
}
- Trace("cegqi-si") << "Solve using single invocation..." << std::endl;
+ Trace("sygus-si") << "Solve using single invocation..." << std::endl;
NodeManager* nm = NodeManager::currentNM();
// Mark the quantified formula with the quantifier elimination attribute to
// ensure its structure is preserved in the query below.
siSmt.setLogic(smt::currentSmtEngine()->getLogicInfo());
siSmt.assertFormula(siq.toExpr());
Result r = siSmt.checkSat();
- Trace("cegqi-si") << "Result: " << r << std::endl;
+ Trace("sygus-si") << "Result: " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() != Result::UNSAT)
{
// conjecture is infeasible or unknown
siSmt.getInstantiatedQuantifiedFormulas(qs);
Assert(qs.size() <= 1);
// track the instantiations, as solution construction is based on this
- Trace("cegqi-si") << "#instantiated quantified formulas=" << qs.size()
+ Trace("sygus-si") << "#instantiated quantified formulas=" << qs.size()
<< std::endl;
d_inst.clear();
d_instConds.clear();
Assert(qn.getKind() == FORALL);
std::vector<std::vector<Expr> > tvecs;
siSmt.getInstantiationTermVectors(q, tvecs);
- Trace("cegqi-si") << "#instantiations of " << q << "=" << tvecs.size()
+ Trace("sygus-si") << "#instantiations of " << q << "=" << tvecs.size()
<< std::endl;
std::vector<Node> vars;
for (const Node& v : qn[0])
{
inst.push_back(Node::fromExpr(t));
}
- Trace("cegqi-si") << " Instantiation: " << inst << std::endl;
+ Trace("sygus-si") << " Instantiation: " << inst << std::endl;
d_inst.push_back(inst);
Assert(inst.size() == vars.size());
Node ilem =
body.substitute(vars.begin(), vars.end(), inst.begin(), inst.end());
ilem = Rewriter::rewrite(ilem);
d_instConds.push_back(ilem);
- Trace("cegqi-si") << " Instantiation Lemma: " << ilem << std::endl;
+ Trace("sygus-si") << " Instantiation Lemma: " << ilem << std::endl;
}
}
d_isSolved = true;
// if we solved all arguments
if (args.empty() && body.isConst() && !body.getConst<bool>())
{
- Trace("cegqi-si-trivial-solve")
+ Trace("sygus-si-trivial-solve")
<< q << " is trivially solvable by substitution " << vars << " -> "
<< subs << std::endl;
std::map<Node, Node> imap;
d_isSolved = true;
return true;
}
- Trace("cegqi-si-trivial-solve")
+ Trace("sygus-si-trivial-solve")
<< q << " is not trivially solvable." << std::endl;
return false;
}
// constructors.
if (!d_usingSymCons)
{
- Trace("cegqi-engine") << " *** Do refinement lemma evaluation"
+ Trace("sygus-engine") << " *** Do refinement lemma evaluation"
<< (doGen ? " with conjecture-specific refinement"
: "")
<< "..." << std::endl;
// just check whether the refinement lemmas are satisfied, fail if not
if (checkRefinementEvalLemmas(candidates, candidate_values))
{
- Trace("cegqi-engine") << "...(actively enumerated) candidate failed "
+ Trace("sygus-engine") << "...(actively enumerated) candidate failed "
"refinement lemma evaluation."
<< std::endl;
return true;
bool doEvalUnfold = (doGen && options::sygusEvalUnfold()) || d_usingSymCons;
if (doEvalUnfold)
{
- Trace("cegqi-engine") << " *** Do evaluation unfolding..." << std::endl;
+ Trace("sygus-engine") << " *** Do evaluation unfolding..." << std::endl;
std::vector<Node> eager_terms, eager_vals, eager_exps;
for (unsigned i = 0, size = candidates.size(); i < size; ++i)
{
const std::vector<Node>& vals,
std::vector<Node>& lems)
{
- Trace("cegqi-engine") << " *** Do sample add refinement..." << std::endl;
+ Trace("sygus-engine") << " *** Do sample add refinement..." << std::endl;
if (Trace.isOn("cegis-sample"))
{
Trace("cegis-sample") << "Check sampling for candidate solution"
}
Trace("cegis-sample") << std::endl;
}
- Trace("cegqi-engine") << " *** Refine by sampling" << std::endl;
+ Trace("sygus-engine") << " *** Refine by sampling" << std::endl;
addRefinementLemma(rlem);
// if trust, we are not interested in sending out refinement lemmas
if (options::cegisSample() != options::CegisSampleMode::TRUST)
}
if (doTerminate)
{
- Trace("cegqi-engine") << "master(" << d_tn << "): complete at size "
+ Trace("sygus-engine") << "master(" << d_tn << "): complete at size "
<< d_currSize << std::endl;
tc.setComplete();
return false;
d_currSize++;
Trace("sygus-enum-debug2") << "master(" << d_tn
<< "): size++ : " << d_currSize << "\n";
- if (Trace.isOn("cegqi-engine"))
+ if (Trace.isOn("sygus-engine"))
{
// am i the master enumerator? if so, print
if (d_se->d_tlEnum == this)
{
- Trace("cegqi-engine") << "SygusEnumerator::size = " << d_currSize
+ Trace("sygus-engine") << "SygusEnumerator::size = " << d_currSize
<< std::endl;
}
}
}
}
- Trace("cegqi-engine") << "Repairing previous solution..." << std::endl;
+ Trace("sygus-engine") << "Repairing previous solution..." << std::endl;
// make the satisfiability query
bool needExport = true;
ExprManagerMapCollection varMap;
if (r.asSatisfiabilityResult().isSat() == Result::UNSAT
|| r.asSatisfiabilityResult().isUnknown())
{
- Trace("cegqi-engine") << "...failed" << std::endl;
+ Trace("sygus-engine") << "...failed" << std::endl;
return false;
}
std::vector<Node> sk_sygus_m;
Node scsk = csk.substitute(
sk_vars.begin(), sk_vars.end(), sk_sygus_m.begin(), sk_sygus_m.end());
repair_cv.push_back(scsk);
- if (Trace.isOn("sygus-repair-const") || Trace.isOn("cegqi-engine"))
+ if (Trace.isOn("sygus-repair-const") || Trace.isOn("sygus-engine"))
{
std::stringstream sss;
Printer::getPrinter(options::outputLanguage())
ss << " * " << candidates[i] << " -> " << sss.str() << std::endl;
}
}
- Trace("cegqi-engine") << "...success:" << std::endl;
- Trace("cegqi-engine") << ss.str();
+ Trace("sygus-engine") << "...success:" << std::endl;
+ Trace("sygus-engine") << ss.str();
Trace("sygus-repair-const")
<< "Repaired constants in solution : " << std::endl;
Trace("sygus-repair-const") << ss.str();
{
if (!value)
{
- Trace("cegqi-engine-debug") << "Conjecture is infeasible." << std::endl;
+ Trace("sygus-engine-debug") << "Conjecture is infeasible." << std::endl;
return false;
}
else
{
- Trace("cegqi-engine-debug") << "Feasible guard " << d_feasible_guard
+ Trace("sygus-engine-debug") << "Feasible guard " << d_feasible_guard
<< " assigned true." << std::endl;
}
}
Assert(d_repair_index < d_cinfo[cprog].d_inst.size());
fail_cvs.push_back(d_cinfo[cprog].d_inst[d_repair_index]);
}
- if (Trace.isOn("cegqi-engine"))
+ if (Trace.isOn("sygus-engine"))
{
- Trace("cegqi-engine") << "CegConjuncture : repair previous solution ";
+ Trace("sygus-engine") << "CegConjuncture : repair previous solution ";
for (const Node& fc : fail_cvs)
{
std::stringstream ss;
Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, fc);
- Trace("cegqi-engine") << ss.str() << " ";
+ Trace("sygus-engine") << ss.str() << " ";
}
- Trace("cegqi-engine") << std::endl;
+ Trace("sygus-engine") << std::endl;
}
d_repair_index++;
if (d_sygus_rconst->repairSolution(
if (!d_master->allowPartialModel() && !fullModel)
{
// we retain the values in d_ev_active_gen_waiting
- Trace("cegqi-engine-debug") << "...partial model, fail." << std::endl;
+ Trace("sygus-engine-debug") << "...partial model, fail." << std::endl;
// if we are partial due to an active enumerator, we may still succeed
// on the next call
return !activeIncomplete;
}
if (emptyModel)
{
- Trace("cegqi-engine-debug") << "...empty model, fail." << std::endl;
+ Trace("sygus-engine-debug") << "...empty model, fail." << std::endl;
return !activeIncomplete;
}
// debug print
- if (Trace.isOn("cegqi-engine"))
+ if (Trace.isOn("sygus-engine"))
{
- Trace("cegqi-engine") << " * Value is : ";
+ Trace("sygus-engine") << " * Value is : ";
for (unsigned i = 0, size = terms.size(); i < size; i++)
{
Node nv = enum_values[i];
TypeNode tn = onv.getType();
std::stringstream ss;
Printer::getPrinter(options::outputLanguage())->toStreamSygus(ss, onv);
- Trace("cegqi-engine") << terms[i] << " -> ";
+ Trace("sygus-engine") << terms[i] << " -> ";
if (nv.isNull())
{
- Trace("cegqi-engine") << "[EXC: " << ss.str() << "] ";
+ Trace("sygus-engine") << "[EXC: " << ss.str() << "] ";
}
else
{
- Trace("cegqi-engine") << ss.str() << " ";
- if (Trace.isOn("cegqi-engine-rr"))
+ Trace("sygus-engine") << ss.str() << " ";
+ if (Trace.isOn("sygus-engine-rr"))
{
Node bv = d_tds->sygusToBuiltin(nv, tn);
bv = Rewriter::rewrite(bv);
- Trace("cegqi-engine-rr") << " -> " << bv << std::endl;
+ Trace("sygus-engine-rr") << " -> " << bv << std::endl;
}
}
}
- Trace("cegqi-engine") << std::endl;
+ Trace("sygus-engine") << std::endl;
}
Assert(candidate_values.empty());
constructed_cand = d_master->constructCandidates(
if (!checkSideCondition(candidate_values))
{
excludeCurrentSolution(terms, candidate_values);
- Trace("cegqi-engine") << "...failed side condition" << std::endl;
+ Trace("sygus-engine") << "...failed side condition" << std::endl;
return false;
}
}
lem = nm->mkNode(OR, d_quant.negate(), query);
if (options::sygusVerifySubcall())
{
- Trace("cegqi-engine") << " *** Verify with subcall..." << std::endl;
+ Trace("sygus-engine") << " *** Verify with subcall..." << std::endl;
Result r =
checkWithSubsolver(query.toExpr(), d_ce_sk_vars, d_ce_sk_var_mvs);
- Trace("cegqi-engine") << " ...got " << r << std::endl;
+ Trace("sygus-engine") << " ...got " << r << std::endl;
if (r.asSatisfiabilityResult().isSat() == Result::SAT)
{
- if (Trace.isOn("cegqi-engine"))
+ if (Trace.isOn("sygus-engine"))
{
- Trace("cegqi-engine") << " * Verification lemma failed for:\n ";
+ Trace("sygus-engine") << " * Verification lemma failed for:\n ";
for (unsigned i = 0, size = d_ce_sk_vars.size(); i < size; i++)
{
- Trace("cegqi-engine")
+ Trace("sygus-engine")
<< d_ce_sk_vars[i] << " -> " << d_ce_sk_var_mvs[i] << " ";
}
- Trace("cegqi-engine") << std::endl;
+ Trace("sygus-engine") << std::endl;
}
#ifdef CVC4_ASSERTIONS
// the values for the query should be a complete model
{
Node sc = d_embedSideCondition.substitute(
d_candidates.begin(), d_candidates.end(), cvals.begin(), cvals.end());
- Trace("cegqi-engine") << "Check side condition..." << std::endl;
+ Trace("sygus-engine") << "Check side condition..." << std::endl;
Trace("cegqi-debug") << "Check side condition : " << sc << std::endl;
Result r = checkWithSubsolver(sc);
Trace("cegqi-debug") << "...got side condition : " << r << std::endl;
{
return false;
}
- Trace("cegqi-engine") << "...passed side condition" << std::endl;
+ Trace("sygus-engine") << "...passed side condition" << std::endl;
}
return true;
}
Node gstatus = d_qe->getValuation().getSatValue(g);
if (gstatus.isNull() || !gstatus.getConst<bool>())
{
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug")
<< "Enumerator " << e << " is inactive." << std::endl;
continue;
}
// if the current model value of e was not registered by the datatypes
// sygus solver, or was excluded by symmetry breaking, then it does not
// have a proper model value that we should consider, thus we return null.
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug")
<< "Enumerator " << e << " does not have proper model value."
<< std::endl;
return Node::null();
void SynthEngine::presolve()
{
- Trace("cegqi-engine") << "SynthEngine::presolve" << std::endl;
+ Trace("sygus-engine") << "SynthEngine::presolve" << std::endl;
for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
{
d_conjs[i]->presolve();
}
- Trace("cegqi-engine") << "SynthEngine::presolve finished" << std::endl;
+ Trace("sygus-engine") << "SynthEngine::presolve finished" << std::endl;
}
bool SynthEngine::needsCheck(Theory::Effort e)
{
Node q = d_waiting_conj.back();
d_waiting_conj.pop_back();
- Trace("cegqi-engine") << "--- Conjecture waiting to assign: " << q
+ Trace("sygus-engine") << "--- Conjecture waiting to assign: " << q
<< std::endl;
assignConjecture(q);
}
return;
}
- Trace("cegqi-engine") << "---Counterexample Guided Instantiation Engine---"
+ Trace("sygus-engine") << "---Counterexample Guided Instantiation Engine---"
<< std::endl;
- Trace("cegqi-engine-debug") << std::endl;
+ Trace("sygus-engine-debug") << std::endl;
Valuation& valuation = d_quantEngine->getValuation();
std::vector<SynthConjecture*> activeCheckConj;
for (unsigned i = 0, size = d_conjs.size(); i < size; i++)
}
else
{
- Trace("cegqi-engine-debug") << "...no value for quantified formula."
+ Trace("sygus-engine-debug") << "...no value for quantified formula."
<< std::endl;
}
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug")
<< "Current conjecture status : active : " << active << std::endl;
if (active && sc->needsCheck())
{
std::vector<SynthConjecture*> acnext;
do
{
- Trace("cegqi-engine-debug") << "Checking " << activeCheckConj.size()
+ Trace("sygus-engine-debug") << "Checking " << activeCheckConj.size()
<< " active conjectures..." << std::endl;
for (unsigned i = 0, size = activeCheckConj.size(); i < size; i++)
{
acnext.clear();
} while (!activeCheckConj.empty()
&& !d_quantEngine->theoryEngineNeedsCheck());
- Trace("cegqi-engine")
+ Trace("sygus-engine")
<< "Finished Counterexample Guided Instantiation engine." << std::endl;
}
void SynthEngine::assignConjecture(Node q)
{
- Trace("cegqi-engine") << "SynthEngine::assignConjecture " << q << std::endl;
+ Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
if (options::sygusQePreproc())
{
// the following does quantifier elimination as a preprocess step
{
Node q = conj->getEmbeddedConjecture();
Node aq = conj->getConjecture();
- if (Trace.isOn("cegqi-engine-debug"))
+ if (Trace.isOn("sygus-engine-debug"))
{
- conj->debugPrint("cegqi-engine-debug");
- Trace("cegqi-engine-debug") << std::endl;
+ conj->debugPrint("sygus-engine-debug");
+ Trace("sygus-engine-debug") << std::endl;
}
if (!conj->needsRefinement())
{
- Trace("cegqi-engine-debug") << "Do conjecture check..." << std::endl;
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug") << "Do conjecture check..." << std::endl;
+ Trace("sygus-engine-debug")
<< " *** Check candidate phase..." << std::endl;
std::vector<Node> cclems;
bool ret = conj->doCheck(cclems);
else
{
// this may happen if we eagerly unfold, simplify to true
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug")
<< " ...FAILED to add candidate!" << std::endl;
}
}
if (addedLemma)
{
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug")
<< " ...check for counterexample." << std::endl;
return true;
}
}
else
{
- Trace("cegqi-engine-debug")
+ Trace("sygus-engine-debug")
<< " *** Refine candidate phase..." << std::endl;
std::vector<Node> rlems;
conj->doRefine(rlems);
}
if (addedLemma)
{
- Trace("cegqi-engine-debug") << " ...refine candidate." << std::endl;
+ Trace("sygus-engine-debug") << " ...refine candidate." << std::endl;
}
}
return true;
d_inst_engine.reset(new quantifiers::InstantiationEngine(qe));
modules.push_back(d_inst_engine.get());
}
- if (options::cbqi())
+ if (options::cegqi())
{
d_i_cbqi.reset(new quantifiers::InstStrategyCegqi(qe));
modules.push_back(d_i_cbqi.get());
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --no-sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --no-sygus-repair-const
; SCRUBBER: sed -e 's/The fact in question: .*$/The fact in question: TERM/'
; EXPECT: (error "A non-linear fact was asserted to arithmetic in a linear logic.
; EXPECT: The fact in question: TERM
-; COMMAND-LINE: --cbqi
+; COMMAND-LINE: --cegqi
; EXPECT: unsat
(set-logic UFNIRA)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi --dt-rewrite-error-sel --lang=smt2.5
+; COMMAND-LINE: --cegqi --dt-rewrite-error-sel --lang=smt2.5
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(declare-datatypes () ((List (cons (head Int) (tail List)) (nil))))
(set-logic LIRA)
(set-info :status unsat)
-(set-option :cbqi-use-inf-int true)
-(set-option :cbqi-use-inf-real true)
+(set-option :cegqi-use-inf-int true)
+(set-option :cegqi-use-inf-real true)
(set-option :var-ineq-elim-quant false)
(assert (forall (( b Real )) (forall (( c Int )) (and (> c (* b 2 ))))))
(check-sat)
(set-logic UFBV)
-(set-option :cbqi-all true)
+(set-option :cegqi-all true)
(set-info :status unsat)
(declare-sort S0 0)
(declare-const S0-0 S0)
-; COMMAND-LINE: --cbqi --finite-model-find --no-check-models
+; COMMAND-LINE: --cegqi --finite-model-find --no-check-models
; EXPECT: sat
(set-logic UFLIA)
(set-info :status sat)
-; COMMAND-LINE: --cbqi --no-check-models
+; COMMAND-LINE: --cegqi --no-check-models
; EXPECT: sat
(set-logic ALL_SUPPORTED)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(declare-fun a () (_ BitVec 8))
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(synth-fun fb () Int ((Start Int)) ((Start Int ((Constant Int)))))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi --cbqi-prereg-inst --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi --cegqi-prereg-inst --sygus-out=status
(set-logic BV)
(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic LIA)
(synth-fun P ((x Int) (y Int)) Bool
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none
; EXPECT: unsat
(set-logic BV)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-unif-pi=complete --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-unif-pi=complete --sygus-out=status
(set-logic LIA)
(define-fun g ((x Int)) Int (ite (= x 1) 15 19))
(define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(define-fun letf ((z Int)) Int (+ z z))
(synth-fun f ((x Int) (y Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic BV)
(define-fun parity ((a Bool) (b Bool) (c Bool) (d Bool)) Bool
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
; EXPECT: unknown
(set-logic LIA)
(synth-fun P ((x Int)) Bool)
-; COMMAND-LINE: --cbqi -mi --no-check-models
+; COMMAND-LINE: --cegqi -mi --no-check-models
; EXPECT: sat
; EXPECT: unsat
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-nested-qe
+; COMMAND-LINE: --cegqi-nested-qe
; EXPECT: unsat
(set-logic LRA)
-; COMMAND-LINE: --cbqi --quant-anti-skolem
+; COMMAND-LINE: --cegqi --quant-anti-skolem
; EXPECT: unsat
(set-logic ALL_SUPPORTED)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi --decision=internal
+; COMMAND-LINE: --cegqi --decision=internal
; EXPECT: unsat
(set-logic LIA)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-rm-extract
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-rm-extract
; EXPECT: sat
(set-logic BV)
(declare-fun k_3 () (_ BitVec 8))
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
(set-logic BV)
(set-info :status sat)
(declare-fun _substvar_16_ () Bool)
-(set-option :cbqi-prereg-inst true)
+(set-option :cegqi-prereg-inst true)
(set-option :check-models true)
(declare-fun v2 () Bool)
(push 1)
-; COMMAND-LINE: --cbqi-use-inf-int --cbqi-use-inf-real
+; COMMAND-LINE: --cegqi-use-inf-int --cegqi-use-inf-real
; EXPECT: unsat
(set-info :smt-lib-version 2.6)
(set-logic LRA)
-; COMMAND-LINE: --cbqi-nested-qe
+; COMMAND-LINE: --cegqi-nested-qe
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cegqi-bv
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-all --no-relational-triggers
+; COMMAND-LINE: --cegqi-all --no-relational-triggers
; EXPECT: unsat
(set-logic NIA)
(declare-fun a () Int)
-; COMMAND-LINE: --cbqi-multi-inst
+; COMMAND-LINE: --cegqi-multi-inst
; EXPECT: unsat
(set-info :smt-lib-version 2.6)
(set-logic NRA)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=eq-boundary
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(declare-fun a () (_ BitVec 8))
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full --bv-div-zero-const
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; COMMAND-LINE: --cegqi-bv --cegqi-bv-ineq=keep --no-cegqi-full
; EXPECT: sat
(set-logic BV)
(set-info :status sat)
-; COMMAND-LINE: --cbqi-bv --no-check-models
+; COMMAND-LINE: --cegqi-bv --no-check-models
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all
+; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cegqi-full --sygus-out=status --sygus-si=all
(set-logic BV)
(define-fun B ((h (_ BitVec 8)) (l (_ BitVec 8)) (v (_ BitVec 8))) (_ BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
; REQUIRES: proof
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-si-sol-min-core --proof
(set-logic LIA)
(synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
(declare-var x1 Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic LIA)
(synth-fun findIdx ((y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (k1 Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 (+ Start Start) (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
(declare-var x1 Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --decision=justification
(set-logic ALL_SUPPORTED)
(declare-var m Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --sygus-si-rcons=try --sygus-out=status
(set-logic BV)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic DTLIA)
(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int) (Con Int))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard
(define-sort D (Enum (a b)))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --sygus-active-gen=enum
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --sygus-active-gen=enum
(set-logic ALL_SUPPORTED)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic BV)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic BV)
(define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x #x00000001))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-add-const-grammar
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-add-const-grammar
(set-logic LIA)
(synth-fun lc ((x Int)) Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic ALL_SUPPORTED)
(declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(synth-fun max ((x Int) (y Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --nl-ext-tplanes
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --nl-ext-tplanes
(set-logic NIA)
(synth-fun max ((x Int) (y Int)) Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cbqi-prereg-inst --cegqi-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-si-abort --decision=internal --cegqi-prereg-inst --sygus-si-rcons=try --sygus-out=status
(set-logic BV)
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct\r
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-fair=direct\r
; EXPECT: unsat\r
(set-logic SLIA)\r
\r
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --sygus-arg-relevant
; EXPECT: unsat
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --sygus-qe-preproc
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status --sygus-qe-preproc
(set-logic LIA)
(synth-fun f ((x Int)) Int)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term-concise
(set-logic LRA)
(synth-fun f ((x Real) (y Real)) Real)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none
(set-logic LRA)
; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-repair-const --lang=sygus2
+; COMMAND-LINE: --sygus-out=status --sygus-si=none --sygus-repair-const --lang=sygus2
(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term
(set-logic ALL)
(synth-fun f ((x String) (y String)) Int)
(declare-var x String)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int) (Term Int))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int) (Term Int))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIA)
(synth-fun f ((x Int)) Int
((Start Int) (Term Int))
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
;; f1 is x plus 2 ;; f2 is 2x plus 5
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=all --sygus-out=status
(set-logic LIA)
(define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
(synth-fun f1 ((x Int)) Int
-; COMMAND-LINE: --cbqi-all --no-check-models
+; COMMAND-LINE: --cegqi-all --no-check-models
; EXPECT: sat
;AJR:BROKEN
(set-logic UFBV)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status
(set-logic LIRA)
(define-fun
__node_init_top_0 (
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-repair-const --sygus-arg-relevant
; EXPECT: unsat
(set-logic LIA)
-; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --sygus-si=none --sygus-out=status --no-sygus-add-const-grammar --sygus-arg-relevant
; EXPECT: unsat
(set-logic LIA)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --no-sygus-pbe
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-si=none --no-sygus-pbe
(set-logic LRA)
; EXPECT: unsat
-; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-si=none --sygus-grammar-cons=any-term --sygus-active-gen=none
(set-logic ALL)
(synth-fun f ((x String) (y String)) Int)
(declare-var x String)
d_em = new ExprManager();
d_nm = NodeManager::fromExprManager(d_em);
d_smt = new SmtEngine(d_em);
- d_smt->setOption("cbqi-full", CVC4::SExpr(true));
+ d_smt->setOption("cegqi-full", CVC4::SExpr(true));
d_smt->setOption("produce-models", CVC4::SExpr(true));
d_scope = new SmtScope(d_smt);
projects / cvc5.git / commitdiff