This PR removes more than half of the remaining static option accesses options::foo() from the theory solvers.
void TheoryArrays::propagateRowLemma(RowLemmaType lem)
{
Debug("pf::array") << "TheoryArrays: RowLemma Propagate called. "
- "options::arraysPropagate() = "
+ "arraysPropagate = "
<< options().arrays.arraysPropagate << std::endl;
TNode a, b, i, j;
// We could but don't do congruence for DT_SIZE and DT_HEIGHT_BOUND here.
// It also could make sense in practice to do congruence for APPLY_UF, but
// this is not done.
- if (getQuantifiersEngine() && options::sygus())
+ if (getQuantifiersEngine() && options().quantifiers.sygus)
{
quantifiers::TermDbSygus* tds =
getQuantifiersEngine()->getTermDatabaseSygus();
}
//if we want to force an assignment of constructors to all ground eqc
//d_dtfCounter++;
- if( !needSplit && options::dtForceAssignment() && d_dtfCounter%2==0 ){
+ if (!needSplit && options().datatypes.dtForceAssignment
+ && d_dtfCounter % 2 == 0)
+ {
Trace("datatypes-force-assign") << "Force assignment for " << n << std::endl;
needSplit = true;
consIndex = fconsIndex!=-1 ? fconsIndex : consIndex;
Trace("datatypes-infer") << "DtInfer : 1-cons (full) : " << t << std::endl;
}else{
Assert(consIndex != -1 || dt.isSygus());
- if( options::dtBinarySplit() && consIndex!=-1 ){
+ if (options().datatypes.dtBinarySplit && consIndex != -1)
+ {
Node test = utils::mkTester(n, consIndex, dt);
Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl;
test = rewrite(test);
Node lemma = nb;
d_im.lemma(lemma, InferenceId::DATATYPES_BINARY_SPLIT);
d_im.requirePhase(test, true);
- }else{
+ }
+ else
+ {
Trace("dt-split") << "*************Split for constructors on " << n << endl;
Node lemma = utils::mkSplit(n, dt);
Trace("dt-split-debug") << "Split lemma is : " << lemma << std::endl;
InferenceId::DATATYPES_SPLIT,
LemmaProperty::SEND_ATOMS);
}
- if( !options::dtBlastSplits() ){
+ if (!options().datatypes.dtBlastSplits)
+ {
break;
}
}
throw LogicException(ss.str());
}
Trace("dt-expand") << "...well-founded ok" << std::endl;
- if (!options::dtNestedRec())
+ if (!options().datatypes.dtNestedRec)
{
if (dt.hasNestedRecursion())
{
// regress0/datatypes/dt-param-card4-bool-sat.smt2 and
// regress0/datatypes/list-bool.smt2).
bool forceLemma;
- if (options::dtPoliteOptimize())
+ if (options().datatypes.dtPoliteOptimize)
{
forceLemma = dt[index].hasFiniteExternalArgType(ttn);
}
TypeNode tn = eqc.getType();
if( tn.isDatatype() ) {
if( !tn.isCodatatype() ){
- if( options::dtCyclic() ){
+ if (options().datatypes.dtCyclic)
+ {
//do cycle checks
std::map< TNode, bool > visited;
std::map< TNode, bool > proc;
}
Trace("datatypes-cycle-check") << "Check uniqueness" << std::endl;
//process codatatypes
- if( cdt_eqc.size()>1 && options::cdtBisimilar() ){
+ if (cdt_eqc.size() > 1 && options().datatypes.cdtBisimilar)
+ {
printModelDebug("dt-cdt-debug");
Trace("dt-cdt-debug") << "Process " << cdt_eqc.size() << " co-datatypes" << std::endl;
std::vector< std::vector< Node > > part_out;
Node sv = d_inverter->getSolveVariable(pv.getType());
Node pvs = ci->getModelValue(pv);
Trace("cegqi-bv") << "Get path to " << pv << " : " << lit << std::endl;
- Node slit =
- d_inverter->getPathToPv(lit, pv, sv, pvs, path, options::cegqiBvSolveNl());
+ Node slit = d_inverter->getPathToPv(
+ lit, pv, sv, pvs, path, options().quantifiers.cegqiBvSolveNl);
if (!slit.isNull())
{
CegInstantiatorBvInverterQuery m(ci);
{
return Node::null();
}
- else if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::KEEP
+ else if (options().quantifiers.cegqiBvIneqMode
+ == options::CegqiBvIneqMode::KEEP
|| (pol && k == EQUAL))
{
return lit;
Trace("cegqi-bv") << " " << sm << " <> " << tm << std::endl;
Node ret;
- if (options::cegqiBvIneqMode() == options::CegqiBvIneqMode::EQ_SLACK)
+ if (options().quantifiers.cegqiBvIneqMode
+ == options::CegqiBvIneqMode::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::cegqiBv())
+ if (options().quantifiers.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::cegqiFullEffort();
+ return effort < CEG_INST_EFFORT_FULL || options().quantifiers.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::cegqiBvInterleaveValue() && Random::getRandom().pickWithProb(0.5))
+ if (options().quantifiers.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::cegqiMultiInst();
+ bool tryMultipleInst = firstVar && options().quantifiers.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::cegqiBvLinearize() && contains_pv[lhs] && contains_pv[rhs])
+ if (options().quantifiers.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_ADD)
{
- if (options::cegqiBvLinearize() && contains_pv[n])
+ if (options().quantifiers.cegqiBvLinearize && contains_pv[n])
{
Node result;
if (n.getKind() == BITVECTOR_MULT)
}
else
{
- if (options::fmfFreshDistConst())
+ if (options().quantifiers.fmfFreshDistConst)
{
mbt = d_treg.getTermDatabase()->getOrMakeTypeFreshVariable(tn);
}
d_range(r),
d_ranges_proxied(userContext())
{
- if( options::fmfBoundLazy() ){
+ if (options().quantifiers.fmfBoundLazy)
+ {
SkolemManager* sm = NodeManager::currentNM()->getSkolemManager();
d_proxy_range = isProxy ? r : sm->mkDummySkolem("pbir", r.getType());
- }else{
+ }
+ else
+ {
d_proxy_range = r;
}
if( !isProxy ){
Trace("bound-int") << "check ownership quantifier " << f << std::endl;
// determine if we should look at the quantified formula at all
- if (!options::fmfBound())
+ if (!options().quantifiers.fmfBound)
{
// only applying it to internal quantifiers
QuantAttributes& qattr = d_qreg.getQuantAttributes();
FirstOrderModelFmc* fmfmc = static_cast<FirstOrderModelFmc*>(fm);
if (effort == 0)
{
- if (options::mbqiMode() == options::MbqiMode::NONE)
+ if (options().quantifiers.mbqiMode == options::MbqiMode::NONE)
{
// just exhaustive instantiate
Node c = mkCondDefault(fmfmc, f);
d_star_insts[f].push_back(i);
continue;
}
- if (options::fmfBound() || options::stringExp())
+ if (options().quantifiers.fmfBound || options().strings.stringExp)
{
std::vector<Node> cond;
cond.push_back(d_quant_cond[f]);
{
Trace("fmc-debug-inst") << "** Added instantiation." << std::endl;
d_addedLemmas++;
- if (d_qstate.isInConflict() || options::fmfOneInstPerRound())
+ if (d_qstate.isInConflict() || options().quantifiers.fmfOneInstPerRound)
{
break;
}
{
Trace("fmc-exh-debug") << " ...success.";
addedLemmas++;
- if (d_qstate.isInConflict() || options::fmfOneInstPerRound())
+ if (d_qstate.isInConflict()
+ || options().quantifiers.fmfOneInstPerRound)
{
break;
}
bool FullModelChecker::useSimpleModels() {
- return options::fmfFmcSimple();
+ return options().quantifiers.fmfFmcSimple;
}
void FullModelChecker::registerQuantifiedFormula(Node q)
{
}
bool QModelBuilder::optUseModel() {
- return options::mbqiMode() != options::MbqiMode::NONE || options::fmfBound()
- || options::stringExp();
+ return options().quantifiers.mbqiMode != options::MbqiMode::NONE
+ || options().quantifiers.fmfBound || options().strings.stringExp;
}
bool QModelBuilder::preProcessBuildModel(TheoryModel* m) {
bool QModelBuilder::preProcessBuildModelStd(TheoryModel* m) {
d_addedLemmas = 0;
d_triedLemmas = 0;
- if (options::fmfFunWellDefinedRelevant())
+ if (options().quantifiers.fmfFunWellDefinedRelevant)
{
//traverse equality engine
std::map< TypeNode, bool > eqc_usort;
itCount = funDefCount.find(f);
}
if (itf == d_funDefMap.end()
- || itCount->second > options::sygusRecFunEvalLimit())
+ || itCount->second > options().quantifiers.sygusRecFunEvalLimit)
{
Trace("fd-eval")
<< "FunDefEvaluator: "
}
void InstStrategyEnum::presolve()
{
- d_fullSaturateLimit = options::fullSaturateLimit();
+ d_fullSaturateLimit = options().quantifiers.fullSaturateLimit;
}
bool InstStrategyEnum::needsCheck(Theory::Effort e)
{
{
return false;
}
- if (options::fullSaturateInterleave())
+ if (options().quantifiers.fullSaturateInterleave)
{
// if interleaved, we run at the same time as E-matching
if (d_qstate.getInstWhenNeedsCheck(e))
return true;
}
}
- if (options::fullSaturateQuant())
+ if (options().quantifiers.fullSaturateQuant)
{
if (e >= Theory::EFFORT_LAST_CALL)
{
bool fullEffort = false;
if (d_fullSaturateLimit != 0)
{
- if (options::fullSaturateInterleave())
+ if (options().quantifiers.fullSaturateInterleave)
{
// we only add when interleaved with other strategies
doCheck = quant_e == QEFFORT_STANDARD && d_qim.hasPendingLemma();
}
- if (options::fullSaturateQuant() && !doCheck)
+ if (options().quantifiers.fullSaturateQuant && !doCheck)
{
if (!d_qstate.getValuation().needCheck())
{
Trace("fs-engine") << "---Full Saturation Round, effort = " << e << "---"
<< std::endl;
}
- unsigned rstart = options::fullSaturateQuantRd() ? 0 : 1;
+ unsigned rstart = options().quantifiers.fullSaturateQuantRd ? 0 : 1;
unsigned rend = fullEffort ? 1 : rstart;
unsigned addedLemmas = 0;
// First try in relevant domain of all quantified formulas, if no
if (process(q, fullEffort, r == 0))
{
// don't need to mark this if we are not stratifying
- if (!options::fullSaturateStratify())
+ if (!options().quantifiers.fullSaturateStratify)
{
alreadyProc[q] = true;
}
}
}
if (d_qstate.isInConflict()
- || (addedLemmas > 0 && options::fullSaturateStratify()))
+ || (addedLemmas > 0 && options().quantifiers.fullSaturateStratify))
{
// we break if we are in conflict, or if we added any lemma at this
// effort level and we stratify effort levels.
TermTupleEnumeratorEnv ttec;
ttec.d_fullEffort = fullEffort;
- ttec.d_increaseSum = options::fullSaturateSum();
+ ttec.d_increaseSum = options().quantifiers.fullSaturateSum;
// make the enumerator, which is either relevant domain or term database
// based on the flag isRd.
std::unique_ptr<TermTupleEnumeratorInterface> enumerator(
{
TermTupleEnumeratorEnv ttec;
ttec.d_fullEffort = true;
- ttec.d_increaseSum = options::fullSaturateSum();
+ ttec.d_increaseSum = options().quantifiers.fullSaturateSum;
TermPools* tp = d_treg.getTermPools();
std::shared_ptr<TermTupleEnumeratorInterface> enumerator(
mkTermTupleEnumeratorPool(q, &ttec, tp, p));
}
else
{
- if (options::quantDynamicSplit() == options::QuantDSplitMode::AGG)
+ if (options().quantifiers.quantDynamicSplit
+ == options::QuantDSplitMode::AGG)
{
// split if it is a finite datatype
doSplit = isFinite;
}
- else if (options::quantDynamicSplit()
+ else if (options().quantifiers.quantDynamicSplit
== options::QuantDSplitMode::DEFAULT)
{
if (!qbi.isFiniteBound(q, q[0][i]))
QuantifiersRegistry::QuantifiersRegistry(Env& env)
: QuantifiersUtil(env),
d_quantAttr(),
- d_quantBoundInf(options::fmfTypeCompletionThresh(),
- options::finiteModelFind()),
+ d_quantBoundInf(options().quantifiers.fmfTypeCompletionThresh,
+ options().quantifiers.finiteModelFind),
d_quantPreproc(env)
{
}
void QueryGenerator::checkQuery(Node qy, unsigned spIndex)
{
// external query
- if (options::sygusQueryGenDumpFiles()
+ if (options().quantifiers.sygusQueryGenDumpFiles
== options::SygusQueryDumpFilesMode::ALL)
{
dumpQuery(qy, spIndex);
}
- if (options::sygusQueryGenCheck())
+ if (options().quantifiers.sygusQueryGenCheck)
{
Trace("sygus-qgen-check") << " query: check " << qy << "..." << std::endl;
// make the satisfiability query
ss << "but cvc5 answered unsat!" << std::endl;
AlwaysAssert(false) << ss.str();
}
- if (options::sygusQueryGenDumpFiles()
+ if (options().quantifiers.sygusQueryGenDumpFiles
== options::SygusQueryDumpFilesMode::UNSOLVED)
{
if (r.asSatisfiabilityResult().isSat() != Result::SAT)
* In detail, given a stream of expressions t_1, ..., t_{n-1}, upon generating
* term t_n, we consider a query (not) t_n = t_i to be an interesting query
* if it is satisfied by at most D points, where D is a predefined threshold
- * given by options::sygusQueryGenThresh(). If t_n has type Bool, we
+ * given by the sygusQueryGenThresh option. If t_n has type Bool, we
* additionally consider the case where t_n is satisfied (or not satisfied) by
* fewer than D points.
*
}
Node lem;
ProofGenerator* pg = nullptr;
- if (isProofEnabled() && !options::dtStcInduction()
- && !options::intWfInduction())
+ if (isProofEnabled() && !options().quantifiers.dtStcInduction
+ && !options().quantifiers.intWfInduction)
{
ProofNodeManager * pnm = d_env.getProofNodeManager();
// if using proofs and not using induction, we use the justified
}
// check which solutions would have been filtered if the current had come
// first
- if (options::sygusFilterSolRevSubsume())
+ if (options().quantifiers.sygusFilterSolRevSubsume)
{
std::vector<Node> nsubsume;
for (const Node& s : d_curr_sols)
d_parent(parent)
{
d_initialized = false;
- options::SygusUnifPiMode mode = options::sygusUnifPi();
+ options::SygusUnifPiMode mode = options().quantifiers.sygusUnifPi;
d_useCondPool = mode == options::SygusUnifPiMode::CENUM
|| mode == options::SygusUnifPiMode::CENUM_IGAIN;
}
Trace("cegqi") << "SynthConjecture : convert to deep embedding..."
<< std::endl;
std::map<TypeNode, std::unordered_set<Node>> extra_cons;
- if( options::sygusAddConstGrammar() ){
+ if (options().quantifiers.sygusAddConstGrammar)
+ {
Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl;
collectTerms( q[1], extra_cons );
}
TNode templ_arg = itta->second;
Assert(!templ_arg.isNull());
// if there is a template for this argument, make a sygus type on top of it
- if( options::sygusTemplEmbedGrammar() ){
+ if (options().quantifiers.sygusTemplEmbedGrammar)
+ {
Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
<< " with arg " << templ_arg << std::endl;
Trace("cegqi-debug") << " embed this template as a grammar..." << std::endl;
* Get include_cons for mkSygusDefaultType.
* mkSygusDefaultType() is a function to make default grammar. It has an
* arguemnt include_cons, which will restrict what operators we want in the
- * grammar. The return value depends on options::produceInterpols(). In
+ * grammar. The return value depends on the produceInterpols option. In
* ASSUMPTIONS option, it will return the operators from axioms. In CONJECTURE
* option, it will return the operators from conj. In SHARED option, it will
* return the oprators shared by axioms and conj. In ALL option, it will
* Set up the grammar for the interpol-to-synthesis.
*
* The user-defined grammar will be encoded by itpGType. The options for
- * grammar is given by options::produceInterpols(). In DEFAULT option, it will
+ * grammar is given by the produceInterpols option. In DEFAULT option, it will
* set up the grammar from itpGType. And if itpGType is null, it will set up
* the default grammar, which is built according to a policy handled by
* getIncludeCons().
Trace("sygus-pbe") << "Initialize PBE : " << n << std::endl;
NodeManager* nm = NodeManager::currentNM();
- if (!options::sygusUnifPbe())
+ if (!options().quantifiers.sygusUnifPbe)
{
// we are not doing unification
return false;
}
}
-bool SygusPbe::allowPartialModel() { return !options::sygusPbeMultiFair(); }
+bool SygusPbe::allowPartialModel()
+{
+ return !options().quantifiers.sygusPbeMultiFair;
+}
bool SygusPbe::constructCandidates(const std::vector<Node>& enums,
const std::vector<Node>& enum_values,
}
}
// Assume two enumerators of types T1 and T2.
- // If options::sygusPbeMultiFair() is true,
+ // If the sygusPbeMultiFair option is true,
// we ensure that all values of type T1 and size n are enumerated before
// any term of type T2 of size n+d, and vice versa, where d is
- // set by options::sygusPbeMultiFairDiff(). If d is zero, then our
+ // set by the sygusPbeMultiFairDiff option. If d is zero, then our
// enumeration is such that all terms of T1 or T2 of size n are considered
// before any term of size n+1.
- int diffAllow = options::sygusPbeMultiFairDiff();
+ int diffAllow = options().quantifiers.sygusPbeMultiFairDiff;
std::vector<unsigned> enum_consider;
for (unsigned i = 0, esize = enums.size(); i < esize; i++)
{
{
Assert(szs[i] >= min_term_size);
int diff = szs[i] - min_term_size;
- if (!options::sygusPbeMultiFair() || diff <= diffAllow)
+ if (!options().quantifiers.sygusPbeMultiFair || diff <= diffAllow)
{
enum_consider.push_back(i);
}
// make the satisfiability query
std::unique_ptr<SolverEngine> repcChecker;
// initialize the subsolver using the standard method
- initializeSubsolver(
- repcChecker,
- d_env.getOptions(),
- d_env.getLogicInfo(),
- Options::current().quantifiers.sygusRepairConstTimeoutWasSetByUser,
- options::sygusRepairConstTimeout());
+ initializeSubsolver(repcChecker,
+ d_env.getOptions(),
+ d_env.getLogicInfo(),
+ options().quantifiers.sygusRepairConstTimeoutWasSetByUser,
+ options().quantifiers.sygusRepairConstTimeout);
// renable options disabled by sygus
repcChecker->setOption("miniscope-quant", "true");
repcChecker->setOption("miniscope-quant-fv", "true");
Node SygusUnifIo::constructSolutionNode(std::vector<Node>& lemmas)
{
Node c = d_candidate;
- if (!d_solution.isNull() && !options::sygusStream())
+ if (!d_solution.isNull() && !options().quantifiers.sygusStream)
{
// already has a solution
return d_solution;
// based on the strategy inferred for each function, determine if we are
// using a unification strategy that is compatible our approach.
StrategyRestrictions restrictions;
- if (options::sygusBoolIteReturnConst())
+ if (options().quantifiers.sygusBoolIteReturnConst)
{
restrictions.d_iteReturnBoolConst = true;
}
d_cand_to_hd_count[f] = 0;
}
// check whether we are using condition enumeration
- options::SygusUnifPiMode mode = options::sygusUnifPi();
+ options::SygusUnifPiMode mode = options().quantifiers.sygusUnifPi;
d_useCondPool = mode == options::SygusUnifPiMode::CENUM
|| mode == options::SygusUnifPiMode::CENUM_IGAIN;
d_useCondPoolIGain = mode == options::SygusUnifPiMode::CENUM_IGAIN;
void SynthEngine::assignConjecture(Node q)
{
Trace("sygus-engine") << "SynthEngine::assignConjecture " << q << std::endl;
- if (options::sygusQePreproc())
+ if (options().quantifiers.sygusQePreproc)
{
Node lem = d_sqp.preprocess(q);
if (!lem.isNull())
void SynthEngine::checkOwnership(Node q)
{
// take ownership of quantified formulas with sygus attribute, and function
- // definitions when options::sygusRecFun is true.
+ // definitions when the sygusRecFun option is true.
QuantAttributes& qa = d_qreg.getQuantAttributes();
- if (qa.isSygus(q) || (qa.isFunDef(q) && options::sygusRecFun()))
+ if (qa.isSygus(q) || (qa.isFunDef(q) && options().quantifiers.sygusRecFun))
{
d_qreg.setOwner(q, this, 2);
}
}
if (d_qreg.getQuantAttributes().isFunDef(q))
{
- Assert(options::sygusRecFun());
+ Assert(options().quantifiers.sygusRecFun);
// If it is a recursive function definition, add it to the function
// definition evaluator class.
Trace("cegqi") << "Registering function definition : " << q << "\n";
return;
}
Trace("cegqi") << "Register conjecture : " << q << std::endl;
- if (options::sygusQePreproc())
+ if (options().quantifiers.sygusQePreproc)
{
d_waiting_conj.push_back(q);
}
// determine if we are actively-generated
bool isActiveGen = false;
- if (options::sygusActiveGenMode() != options::SygusActiveGenMode::NONE)
+ if (options().quantifiers.sygusActiveGenMode
+ != options::SygusActiveGenMode::NONE)
{
if (erole == ROLE_ENUM_MULTI_SOLUTION || erole == ROLE_ENUM_CONSTRAINED)
{
{
// If the enumerator is the single function-to-synthesize, if auto is
// enabled, we infer whether it is better to enable active generation.
- if (options::sygusActiveGenMode() == options::SygusActiveGenMode::AUTO)
+ if (options().quantifiers.sygusActiveGenMode
+ == options::SygusActiveGenMode::AUTO)
{
// We use active generation if the grammar of the enumerator does not
// have ITE and does not have Boolean connectives. Experimentally, it
// sygus stream are to find many solutions to an easy problem, where
// the bottleneck often becomes the large number of "exclude the current
// solution" clauses.
- if (options::sygusStream()
+ if (options().quantifiers.sygusStream
|| (!eti.hasIte() && !eti.hasBoolConnective()))
{
isActiveGen = true;
// Currently, actively-generated enumerators are either basic or variable
// agnostic.
bool isVarAgnostic = isActiveGen
- && options::sygusActiveGenMode()
+ && options().quantifiers.sygusActiveGenMode
== options::SygusActiveGenMode::VAR_AGNOSTIC;
d_enum_var_agnostic[e] = isVarAgnostic;
if (isVarAgnostic)
// constant, we are done
return res;
}
- if (options::sygusRecFun())
+ if (options().quantifiers.sygusRecFun)
{
if (d_funDefEval->hasDefinitions())
{
}
return true;
}
- if (!options::sygusSymBreakAgg())
+ if (!options().datatypes.sygusSymBreakAgg)
{
return false;
}
Assert(varlist.size() == args.size());
Node res;
- if (tryEval && options::sygusEvalOpt())
+ if (tryEval && options().quantifiers.sygusEvalOpt)
{
// Try evaluating, which is much faster than substitution+rewriting.
// This may fail if there is a subterm of bn under the
TermDbSygus* db = d_treg.getTermDatabaseSygus();
SygusExplain syexplain(db);
NodeManager* nm = NodeManager::currentNM();
- options::SygusInstMode mode = options::sygusInstMode();
+ options::SygusInstMode mode = options().quantifiers.sygusInstMode;
for (const Node& q : d_active_quant)
{
std::unordered_set<Node> term_irrelevant;
/* Collect relevant local ground terms for each variable type. */
- if (options::sygusInstScope() == options::SygusInstScope::IN
- || options::sygusInstScope() == options::SygusInstScope::BOTH)
+ if (options().quantifiers.sygusInstScope == options::SygusInstScope::IN
+ || options().quantifiers.sygusInstScope == options::SygusInstScope::BOTH)
{
std::unordered_map<TypeNode, std::unordered_set<Node>> relevant_terms;
for (const Node& var : q[0])
}
/* Collect relevant global ground terms for each variable type. */
- if (options::sygusInstScope() == options::SygusInstScope::OUT
- || options::sygusInstScope() == options::SygusInstScope::BOTH)
+ if (options().quantifiers.sygusInstScope == options::SygusInstScope::OUT
+ || options().quantifiers.sygusInstScope == options::SygusInstScope::BOTH)
{
for (const Node& var : q[0])
{
d_qim(nullptr),
d_qreg(qr),
d_termsContext(),
- d_termsContextUse(options::termDbCd() ? context() : &d_termsContext),
+ d_termsContextUse(options().quantifiers.termDbCd ? context()
+ : &d_termsContext),
d_processed(d_termsContextUse),
d_typeMap(d_termsContextUse),
d_ops(d_termsContextUse),
d_consistent_ee = true;
d_true = NodeManager::currentNM()->mkConst(true);
d_false = NodeManager::currentNM()->mkConst(false);
- if (!options::termDbCd())
+ if (!options().quantifiers.termDbCd)
{
// when not maintaining terms in a context-dependent manner, we clear during
// each presolve, which requires maintaining a single outermost level
Node k = sm->mkDummySkolem(ss.str(), tn, "is a termDb fresh variable");
Trace("mkVar") << "TermDb:: Make variable " << k << " : " << tn
<< std::endl;
- if (options::instMaxLevel() != -1)
+ if (options().quantifiers.instMaxLevel != -1)
{
QuantAttributes::setInstantiationLevelAttr(k, 0);
}
return d_has_map.find( n )!=d_has_map.end();
}
//some assertions are not sent to EE
- if (options::termDbMode() == options::TermDbMode::ALL)
+ if (options().quantifiers.termDbMode == options::TermDbMode::ALL)
{
return true;
}
- else if (options::termDbMode() == options::TermDbMode::RELEVANT)
+ else if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
{
return d_has_map.find( n )!=d_has_map.end();
}
- Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : " << options::termDbMode();
+ Assert(false) << "TermDb::hasTermCurrent: Unknown termDbMode : "
+ << options().quantifiers.termDbMode;
return false;
}
bool TermDb::isTermEligibleForInstantiation(TNode n, TNode f)
{
- if( options::instMaxLevel()!=-1 ){
+ if (options().quantifiers.instMaxLevel != -1)
+ {
if( n.hasAttribute(InstLevelAttribute()) ){
int64_t fml =
f.isNull() ? -1 : d_qreg.getQuantAttributes().getQuantInstLevel(f);
- unsigned ml = fml>=0 ? fml : options::instMaxLevel();
+ unsigned ml = fml >= 0 ? fml : options().quantifiers.instMaxLevel;
if( n.getAttribute(InstLevelAttribute())>ml ){
Trace("inst-add-debug") << "Term " << n << " has instantiation level " << n.getAttribute(InstLevelAttribute());
return false;
}
}else{
- if( options::instLevelInputOnly() ){
+ if (options().quantifiers.instLevelInputOnly)
+ {
Trace("inst-add-debug") << "Term " << n << " does not have an instantiation level." << std::endl;
return false;
}
}
void TermDb::presolve() {
- if (options::incrementalSolving() && !options::termDbCd())
+ if (options().base.incrementalSolving && !options().quantifiers.termDbCd)
{
d_termsContext.pop();
d_termsContext.push();
}
//compute has map
- if (options::termDbMode() == options::TermDbMode::RELEVANT)
+ if (options().quantifiers.termDbMode == options::TermDbMode::RELEVANT)
{
d_has_map.clear();
d_term_elig_eqc.clear();
* It returns whether the term n should be indexed in the current context.
*
* If the argument useMode is true, then this method returns a value based on
- * the option options::termDbMode().
+ * the option termDbMode.
* Otherwise, it returns the lookup in the map d_has_map.
*/
bool hasTermCurrent(Node n, bool useMode = true);
// post-construction.
d_quantEngine = d_qengine.get();
- if (options::macrosQuant())
+ if (options().quantifiers.macrosQuant)
{
d_qmacros.reset(new QuantifiersMacros(d_qreg));
}
if (d_qmacros != nullptr)
{
bool reqGround =
- options::macrosQuantMode() != options::MacrosQuantMode::ALL;
+ options().quantifiers.macrosQuantMode != options::MacrosQuantMode::ALL;
Node eq = d_qmacros->solve(tin.getProven(), reqGround);
if (!eq.isNull())
{
bool addedLemma = false;
bool needAddLemma = false;
// check negated star / positive wand
- if (options::sepCheckNeg())
+ if (options().sep.sepCheckNeg)
{
// get active labels
std::map<Node, bool> active_lbl;
- if (options::sepMinimalRefine())
+ if (options().sep.sepMinimalRefine)
{
for( NodeList::const_iterator i = d_spatial_assertions.begin(); i != d_spatial_assertions.end(); ++i ) {
Node fact = (*i);
tn_is_monotonic = tn.getCardinality().isInfinite();
}
//add a reference type for maximum occurrences of empty in a constraint
- if( options::sepDisequalC() && tn_is_monotonic ){
+ if (options().sep.sepDisequalC && tn_is_monotonic)
+ {
for( unsigned r=0; r<d_type_references_card[tn].size(); r++ ){
Node e = d_type_references_card[tn][r];
//ensure that it is distinct from all other references so far
}
d_type_references_all[tn].push_back( e );
}
- }else{
+ }
+ else
+ {
//break symmetries TODO
d_type_references_all[tn].insert( d_type_references_all[tn].end(), d_type_references_card[tn].begin(), d_type_references_card[tn].end() );
unsigned ind)
{
Trace("sep-inst-debug") << "Instantiate label " << n << " " << lbl << " " << lbl_v << std::endl;
- if( options::sepMinimalRefine() && lbl!=o_lbl && active_lbl.find( lbl )!=active_lbl.end() ){
+ if (options().sep.sepMinimalRefine && lbl != o_lbl
+ && active_lbl.find(lbl) != active_lbl.end())
+ {
Trace("sep-inst") << "...do not instantiate " << o_lbl << " since it has an active sublabel " << lbl << std::endl;
return Node::null();
- }else{
+ }
+ else
+ {
if( Trace.isOn("sep-inst") ){
if( n.getKind()==kind::SEP_STAR || n.getKind()==kind::SEP_WAND || n.getKind()==kind::SEP_PTO || n.getKind()==kind::SEP_EMP ){
for( unsigned j=0; j<ind; j++ ){ Trace("sep-inst") << " "; }
Assert(bchildren.size() > 1);
conj.push_back( NodeManager::currentNM()->mkNode( kind::AND, bchildren ) );
- if( options::sepChildRefine() ){
+ if (options().sep.sepChildRefine)
+ {
//child-specific refinements (TODO: use ?)
for( unsigned i=0; i<children.size(); i++ ){
std::vector< Node > tchildren;
int32_t lentTestSuccess = -1;
Node lenConstraint;
- if (options::stringCheckEntailLen())
+ if (options().strings.stringCheckEntailLen)
{
// If length entailment checks are enabled, we can save the case split by
// inferring that `x` has to be longer than `y` or vice-versa.
TypeNode stype = veci[loop_index].getType();
- if (options::stringProcessLoopMode() == options::ProcessLoopMode::ABORT)
+ if (options().strings.stringProcessLoopMode
+ == options::ProcessLoopMode::ABORT)
{
throw LogicException("Looping word equation encountered.");
}
- else if (options::stringProcessLoopMode() == options::ProcessLoopMode::NONE
+ else if (options().strings.stringProcessLoopMode
+ == options::ProcessLoopMode::NONE
|| stype.isSequence())
{
// note we cannot convert looping word equations into regular expressions if
}
else
{
- if (options::stringProcessLoopMode()
+ if (options().strings.stringProcessLoopMode
== options::ProcessLoopMode::SIMPLE_ABORT)
{
throw LogicException("Normal looping word equation encountered.");
}
- else if (options::stringProcessLoopMode()
+ else if (options().strings.stringProcessLoopMode
== options::ProcessLoopMode::SIMPLE)
{
d_im.setIncomplete(IncompleteId::STRINGS_LOOP_SKIP);
return;
}
- if (options::stringsDeqExt())
+ if (options().strings.stringsDeqExt)
{
processDeqExtensionality(ni, nj);
return;
<< " get symbolic definition..." << std::endl;
Node nrs;
// only use symbolic definitions if option is set
- if (options::stringInferSym())
+ if (options().strings.stringInferSym)
{
nrs = d_termReg.getSymbolicDefinition(sn, exps);
}
processConflict(ii);
return;
}
- else if (asLemma || options::stringInferAsLemmas() || !ii.isFact())
+ else if (asLemma || options().strings.stringInferAsLemmas || !ii.isFact())
{
Trace("strings-infer-debug") << "...as lemma" << std::endl;
addPendingLemma(std::unique_ptr<InferInfo>(new InferInfo(ii)));
return;
}
- if (options::stringInferSym())
+ if (options().strings.stringInferSym)
{
std::vector<Node> unproc;
for (const Node& ac : ii.d_premises)
utils::flattenOp(AND, ec, exp);
}
std::vector<Node> noExplain;
- if (!options::stringRExplainLemmas())
+ if (!options().strings.stringRExplainLemmas)
{
// if we aren't regressing the explanation, we add all literals to
// noExplain and ignore ii.d_ant.
}
else
{
- if (!options::stringExp())
+ if (!options().strings.stringExp)
{
throw LogicException(
"Strings Incomplete (due to Negative Membership) by default, "
bool RegExpSolver::checkEqcIntersect(const std::vector<Node>& mems)
{
// do not compute intersections if the re intersection mode is none
- if (options::stringRegExpInterMode() == options::RegExpInterMode::NONE)
+ if (options().strings.stringRegExpInterMode == options::RegExpInterMode::NONE)
{
return true;
}
}
RegExpConstType rct = d_regexp_opr.getRegExpConstType(m[1]);
if (rct == RE_C_VARIABLE
- || (options::stringRegExpInterMode()
+ || (options().strings.stringRegExpInterMode
== options::RegExpInterMode::CONSTANT
&& rct != RE_C_CONRETE_CONSTANT))
{
// on option.
continue;
}
- if (options::stringRegExpInterMode()
+ if (options().strings.stringRegExpInterMode
== options::RegExpInterMode::ONE_CONSTANT)
{
if (!mi.isNull() && rcti >= RE_C_CONSTANT && rct >= RE_C_CONSTANT)
<< "TheoryString::preregister : " << n << std::endl;
// check for logic exceptions
Kind k = n.getKind();
- if (!options::stringExp())
+ if (!options().strings.stringExp)
{
if (k == STRING_INDEXOF || k == STRING_INDEXOF_RE || k == STRING_ITOS
|| k == STRING_STOI || k == STRING_REPLACE || k == STRING_SUBSTR
{
d_functionsTerms.push_back(n);
}
- if (options::stringFMF())
+ if (options().strings.stringFMF)
{
if (tn.isStringLike())
{
TypeNode tn = n.getType();
if (!tn.isStringLike())
{
- if (options::stringEagerLen())
+ if (options().strings.stringEagerLen)
{
do_register = effort == 0;
}
d_statistics),
d_rsolver(
env, d_state, d_im, d_termReg, d_csolver, d_esolver, d_statistics),
- d_regexp_elim(options::regExpElimAgg(), d_pnm, userContext()),
+ d_regexp_elim(options().strings.regExpElimAgg, d_pnm, userContext()),
d_stringsFmf(env, valuation, d_termReg)
{
d_termReg.finishInit(&d_im);
// witness is used to eliminate str.from_code
d_valuation.setUnevaluatedKind(WITNESS);
- bool eagerEval = options::stringEagerEval();
+ bool eagerEval = options().strings.stringEagerEval;
// The kinds we are treating as function application in congruence
d_equalityEngine->addFunctionKind(kind::STRING_LENGTH, eagerEval);
d_equalityEngine->addFunctionKind(kind::STRING_CONCAT, eagerEval);
}
void TheoryStrings::presolve() {
- Debug("strings-presolve") << "TheoryStrings::Presolving : get fmf options " << (options::stringFMF() ? "true" : "false") << std::endl;
+ Debug("strings-presolve")
+ << "TheoryStrings::Presolving : get fmf options "
+ << (options().strings.stringFMF ? "true" : "false") << std::endl;
d_strat.initializeStrategy();
// if strings fmf is enabled, register the strategy
- if (options::stringFMF())
+ if (options().strings.stringFMF)
{
d_stringsFmf.presolve();
// This strategy is local to a check-sat call, since we refresh the strategy
}
bool TheoryStrings::needsCheckLastEffort() {
- if( options::stringGuessModel() ){
+ if (options().strings.stringGuessModel)
+ {
return d_esolver.hasExtendedFunctions();
}
return false;
}
TrustNode ret;
Node atomRet = atom;
- if (options::regExpElim() && atom.getKind() == STRING_IN_REGEXP)
+ if (options().strings.regExpElim && atom.getKind() == STRING_IN_REGEXP)
{
// aggressive elimination of regular expression membership
ret = d_regexp_elim.eliminateTrusted(atomRet);
d_min_pos_tn_master_card_set(context(), false),
d_rel_eqc(context())
{
- if (options::ufssMode() == options::UfssMode::FULL && options::ufssFairness())
+ if (options().uf.ufssMode == options::UfssMode::FULL
+ && options().uf.ufssFairness)
{
// Register the strategy with the decision manager of the theory.
// We are guaranteed that the decision manager is ready since we
Trace("uf-ss") << "Assert " << n << " " << isDecision << std::endl;
bool polarity = n.getKind() != kind::NOT;
TNode lit = polarity ? n : n[0];
- if (options::ufssMode() == options::UfssMode::FULL)
+ if (options().uf.ufssMode == options::UfssMode::FULL)
{
if( lit.getKind()==CARDINALITY_CONSTRAINT ){
const CardinalityConstraint& cc =
uint32_t nCard = cc.getUpperBound().getUnsignedInt();
Trace("uf-ss-debug") << "...check cardinality constraint : " << tn
<< std::endl;
- if (options::ufssFairnessMonotone())
+ if (options().uf.ufssFairnessMonotone)
{
SortInference* si = d_state.getSortInference();
Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
}
if (!d_state.isInConflict())
{
- if (options::ufssMode() == options::UfssMode::FULL)
+ if (options().uf.ufssMode == options::UfssMode::FULL)
{
Trace("uf-ss-solver")
<< "CardinalityExtension: check " << level << std::endl;
}
}
}
- else if (options::ufssMode() == options::UfssMode::NO_MINIMAL)
+ else if (options().uf.ufssMode == options::UfssMode::NO_MINIMAL)
{
if( level==Theory::EFFORT_FULL ){
// split on an equality between two equivalence classes (at most one per type)
void CardinalityExtension::preRegisterTerm(TNode n)
{
- if (options::ufssMode() != options::UfssMode::FULL)
+ if (options().uf.ufssMode != options::UfssMode::FULL)
{
return;
}
/** check */
void CardinalityExtension::checkCombinedCardinality()
{
- Assert(options::ufssMode() == options::UfssMode::FULL);
- if( options::ufssFairness() ){
+ Assert(options().uf.ufssMode == options::UfssMode::FULL);
+ if (options().uf.ufssFairness)
+ {
Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
uint32_t totalCombinedCard = 0;
uint32_t maxMonoSlave = 0;
TypeNode maxSlaveType;
for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
uint32_t max_neg = it->second->getMaximumNegativeCardinality();
- if( !options::ufssFairnessMonotone() ){
+ if (!options().uf.ufssFairnessMonotone)
+ {
totalCombinedCard += max_neg;
- }else{
+ }
+ else
+ {
std::map< TypeNode, bool >::iterator its = d_tn_mono_slave.find( it->first );
if( its==d_tn_mono_slave.end() || !its->second ){
totalCombinedCard += max_neg;
}
}
Trace("uf-ss-com-card-debug") << "Check combined cardinality, total combined card : " << totalCombinedCard << std::endl;
- if( options::ufssFairnessMonotone() ){
+ if (options().uf.ufssFairnessMonotone)
+ {
Trace("uf-ss-com-card-debug") << "Max slave monotonic negated cardinality : " << maxMonoSlave << std::endl;
if (!d_min_pos_tn_master_card_set.get()
&& maxMonoSlave > d_min_pos_tn_master_card.get())
for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin();
it != d_rep_model.end(); ++it ){
bool doAdd = true;
- if( options::ufssFairnessMonotone() ){
+ if (options().uf.ufssFairnessMonotone)
+ {
std::map< TypeNode, bool >::iterator its =
d_tn_mono_slave.find( it->first );
if( its!=d_tn_mono_slave.end() && its->second ){
/**
* Decision strategy for combined cardinality constraints. This asserts
* the minimal combined cardinality constraint positively in the SAT
- * context. It is enabled by options::ufssFairness(). For details, see
+ * context. It is enabled by the ufssFairness option. For details, see
* the extension to multiple sorts in Section 6.3 of Reynolds et al,
* "Constraint Solving for Finite Model Finding in SMT Solvers", TPLP 2017.
*/
}
++eqcs_i;
}
- if (!options::ufHoExt())
+ if (!options().uf.ufHoExt)
{
// we are not applying extensionality, thus we are incomplete if functions
// are present
{
esi.d_notify = &d_notify;
esi.d_name = d_instanceName + "theory::uf::ee";
- if (options::finiteModelFind()
- && options::ufssMode() != options::UfssMode::NONE)
+ if (options().quantifiers.finiteModelFind
+ && options().uf.ufssMode != options::UfssMode::NONE)
{
// need notifications about sorts
esi.d_notifyNewClass = true;
d_valuation.setUnevaluatedKind(kind::COMBINED_CARDINALITY_CONSTRAINT);
// Initialize the cardinality constraints solver if the logic includes UF,
// finite model finding is enabled, and it is not disabled by
- // options::ufssMode().
- if (options::finiteModelFind()
- && options::ufssMode() != options::UfssMode::NONE)
+ // the ufssMode option.
+ if (options().quantifiers.finiteModelFind
+ && options().uf.ufssMode != options::UfssMode::NONE)
{
d_thss.reset(new CardinalityExtension(d_env, d_state, d_im, this));
}
// TimerStat::CodeTimer codeTimer(d_presolveTimer);
Debug("uf") << "uf: begin presolve()" << endl;
- if(options::ufSymmetryBreaker()) {
+ if (options().uf.ufSymmetryBreaker)
+ {
vector<Node> newClauses;
d_symb.apply(newClauses);
for(vector<Node>::const_iterator i = newClauses.begin();
}
}
- if(options::ufSymmetryBreaker()) {
+ if (options().uf.ufSymmetryBreaker)
+ {
d_symb.assertFormula(n);
}
} /* TheoryUF::ppStaticLearn() */
projects / cvc5.git / commitdiff