Towards eliminating option scopes.
Also simplifies and corrects an issue in default Boolean grammar construction where included/excluded constructors were ignored.
d_secd.get(),
&d_stats,
false,
- options().quantifiers.sygusRepairConst);
+ options().quantifiers.sygusRepairConst,
+ options().quantifiers.sygusEnumFastNumConsts);
}
}
Trace("sygus-active-gen")
SygusEnumeratorCallback* sec,
SygusStatistics* s,
bool enumShapes,
- bool enumAnyConstHoles)
+ bool enumAnyConstHoles,
+ size_t numConstants)
: EnumValGenerator(env),
d_tds(tds),
d_sec(sec),
d_stats(s),
d_enumShapes(enumShapes),
d_enumAnyConstHoles(enumAnyConstHoles),
+ d_enumNumConsts(numConstants),
d_tlEnum(nullptr),
d_abortSize(-1)
{
}
initializeTermCache(tn);
// create the master enumerator
- d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn));
+ d_masterEnumInt[tn].reset(new TermEnumMasterInterp(tn, d_enumNumConsts));
// initialize the master enumerator
TermEnumMasterInterp* temi = d_masterEnumInt[tn].get();
bool ret = temi->initialize(this, tn);
return visited[n];
}
-SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn)
- : TermEnum(), d_te(tn), d_currNumConsts(0), d_nextIndexEnd(0)
+SygusEnumerator::TermEnumMasterInterp::TermEnumMasterInterp(TypeNode tn,
+ size_t numConstants)
+ : TermEnum(),
+ d_te(tn),
+ d_currNumConsts(0),
+ d_nextIndexEnd(0),
+ d_enumNumConsts(numConstants)
{
}
{
tc.pushEnumSizeIndex();
d_currSize++;
- d_currNumConsts = d_currNumConsts * options::sygusEnumFastNumConsts();
+ d_currNumConsts = d_currNumConsts * d_enumNumConsts;
d_nextIndexEnd = d_nextIndexEnd + d_currNumConsts;
}
++d_te;
* number of free variables
* @param enumAnyConstHoles If true, this enumerator will generate terms where
* free variables are the arguments to any-constant constructors.
+ * @param numConstants The number of interpreted constants to consider for
+ * each size
*/
SygusEnumerator(Env& env,
TermDbSygus* tds = nullptr,
SygusEnumeratorCallback* sec = nullptr,
SygusStatistics* s = nullptr,
bool enumShapes = false,
- bool enumAnyConstHoles = false);
+ bool enumAnyConstHoles = false,
+ size_t numConstants = 5);
~SygusEnumerator() {}
/** initialize this class with enumerator e */
void initialize(Node e) override;
/** Whether we are enumerating free variables as arguments to any-constant
* constructors */
bool d_enumAnyConstHoles;
+ /** The number of interpreted constants to consider for each size */
+ size_t d_enumNumConsts;
/** Term cache
*
* This stores a list of terms for a given sygus type. The key features of
class TermEnumMasterInterp : public TermEnum
{
public:
- TermEnumMasterInterp(TypeNode tn);
+ TermEnumMasterInterp(TypeNode tn, size_t numConstants);
/** initialize this enumerator */
bool initialize(SygusEnumerator* se, TypeNode tn);
/** get the current term of the enumerator */
unsigned d_currNumConsts;
/** the next end threshold */
unsigned d_nextIndexEnd;
+ /** The number of interpreted constants to consider for each size */
+ size_t d_enumNumConsts;
};
/** a free variable enumerator
*
#include "expr/dtype_cons.h"
#include "expr/node_algorithm.h"
#include "options/base_options.h"
-#include "options/quantifiers_options.h"
#include "theory/bv/theory_bv_utils.h"
#include "theory/datatypes/sygus_datatype_utils.h"
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
}
// make the default grammar
- tn = mkSygusDefaultType(preGrammarType,
+ tn = mkSygusDefaultType(options(),
+ preGrammarType,
sfvl,
ss.str(),
extra_cons,
return visited[n];
}
-TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name,
- std::set<TypeNode>& unres)
+TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name)
{
- TypeNode unresolved =
- NodeManager::currentNM()->mkUnresolvedDatatypeSort(name);
- unres.insert(unresolved);
- return unresolved;
+ return NodeManager::currentNM()->mkUnresolvedDatatypeSort(name);
}
void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
const std::map<TypeNode, std::unordered_set<Node>>& include_cons,
std::unordered_set<Node>& term_irrelevant,
std::vector<SygusDatatypeGenerator>& sdts,
- std::set<TypeNode>& unres)
+ options::SygusGrammarConsMode sgcm)
{
NodeManager* nm = NodeManager::currentNM();
Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
// create placeholder for boolean type (kept apart since not collected)
+ // make Boolean type
+ TypeNode bool_type = nm->booleanType();
+ // the index of Bool in types
+ size_t boolIndex = types.size();
+ types.push_back(bool_type);
+
// create placeholders for collected types
std::vector<TypeNode> unres_types;
std::map<TypeNode, TypeNode> type_to_unres;
std::map<TypeNode, std::unordered_set<Node>>::const_iterator itc;
// maps types to the index of its "any term" grammar construction
std::map<TypeNode, std::pair<unsigned, bool>> typeToGAnyTerm;
- options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
- for (unsigned i = 0, size = types.size(); i < size; ++i)
+ for (size_t i = 0, size = types.size(); i < size; ++i)
{
std::stringstream ss;
ss << fun << "_" << types[i];
sdts.back().d_include_cons = itc->second;
}
//make unresolved type
- TypeNode unres_t = mkUnresolvedType(dname, unres);
+ TypeNode unres_t = mkUnresolvedType(dname);
unres_types.push_back(unres_t);
type_to_unres[types[i]] = unres_t;
sygus_to_builtin[unres_t] = types[i];
}
- // make Boolean type
- std::stringstream ssb;
- ssb << fun << "_Bool";
- std::string dbname = ssb.str();
- sdts.push_back(SygusDatatypeGenerator(dbname));
- unsigned boolIndex = types.size();
- TypeNode bool_type = nm->booleanType();
- TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres);
- types.push_back(bool_type);
- unres_types.push_back(unres_bt);
- type_to_unres[bool_type] = unres_bt;
- sygus_to_builtin[unres_bt] = bool_type;
+ TypeNode unres_bt = type_to_unres[bool_type];
// We ensure an ordering on types such that parametric types are processed
// before their consitituents. Since parametric types were added before their
std::stringstream ssat;
ssat << sdts[i].d_sdt.getName() << "_any_term";
sdts.push_back(SygusDatatypeGenerator(ssat.str()));
- TypeNode unresAnyTerm = mkUnresolvedType(ssat.str(), unres);
+ TypeNode unresAnyTerm = mkUnresolvedType(ssat.str());
unres_types.push_back(unresAnyTerm);
// set tracking information for later addition at boolean type.
std::pair<unsigned, bool> p(sdts.size() - 1, false);
ss << fun << "_PosIReal";
std::string posIRealName = ss.str();
// make unresolved type
- TypeNode unresPosIReal = mkUnresolvedType(posIRealName, unres);
+ TypeNode unresPosIReal = mkUnresolvedType(posIRealName);
unres_types.push_back(unresPosIReal);
// make data type for positive constant integral reals
sdts.push_back(SygusDatatypeGenerator(posIRealName));
std::stringstream ss;
ss << fun << "_AnyConst";
// Make sygus datatype for any constant.
- TypeNode unresAnyConst = mkUnresolvedType(ss.str(), unres);
+ TypeNode unresAnyConst = mkUnresolvedType(ss.str());
unres_types.push_back(unresAnyConst);
sdts.push_back(SygusDatatypeGenerator(ss.str()));
sdts.back().d_sdt.addAnyConstantConstructor(types[i]);
for (unsigned i = 0; i < 4; i++)
{
Kind k = i == 0 ? NOT : (i == 1 ? AND : (i == 2 ? OR : ITE));
- // TODO #1935 ITEs are added to Boolean grammars so that we can infer
- // unification strategies. We can do away with this if we can infer
- // unification strategies from and/or/not
- if (k == ITE && options::sygusUnifPi() == options::SygusUnifPiMode::NONE)
- {
- continue;
- }
Trace("sygus-grammar-def") << "...add for " << k << std::endl;
std::vector<TypeNode> cargs;
cargs.push_back(unres_bt);
}
TypeNode CegGrammarConstructor::mkSygusDefaultType(
+ const Options& opts,
TypeNode range,
Node bvl,
const std::string& fun,
std::map<TypeNode, std::unordered_set<Node>>& include_cons,
std::unordered_set<Node>& term_irrelevant)
{
+ NodeManager* nm = NodeManager::currentNM();
Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
for (std::map<TypeNode, std::unordered_set<Node>>::iterator it =
extra_cons.begin();
{
Trace("sygus-grammar-def") << " ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
}
- std::set<TypeNode> unres;
+ // TODO #1935 ITEs are added to Boolean grammars so that we can infer
+ // unification strategies. We can do away with this if we can infer
+ // unification strategies from and/or/not
+ if (opts.quantifiers.sygusUnifPi == options::SygusUnifPiMode::NONE)
+ {
+ TypeNode btype = nm->booleanType();
+ exclude_cons[btype].insert(nm->operatorOf(ITE));
+ Trace("sygus-grammar-def") << "...exclude Boolean ITE" << std::endl;
+ }
std::vector<SygusDatatypeGenerator> sdts;
mkSygusDefaultGrammar(range,
bvl,
include_cons,
term_irrelevant,
sdts,
- unres);
+ opts.quantifiers.sygusGrammarConsMode);
// extract the datatypes from the sygus datatype generator objects
std::vector<DType> datatypes;
for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
}
Trace("sygus-grammar-def") << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
Assert(!datatypes.empty());
- std::vector<TypeNode> types =
- NodeManager::currentNM()->mkMutualDatatypeTypes(datatypes);
+ std::vector<TypeNode> types = nm->mkMutualDatatypeTypes(datatypes);
Trace("sygus-grammar-def") << "...finished" << std::endl;
Assert(types.size() == datatypes.size());
return types[0];
return templ_arg_sygus_type;
}else{
tcount++;
- std::set<TypeNode> unres;
std::vector<SygusDatatype> sdts;
std::stringstream ssd;
ssd << fun << "_templ_" << tcount;
#include "expr/attribute.h"
#include "expr/node.h"
#include "expr/sygus_datatype.h"
+#include "options/quantifiers_options.h"
#include "smt/env_obj.h"
namespace cvc5::internal {
* will be included.
*/
static TypeNode mkSygusDefaultType(
+ const Options& opts,
TypeNode range,
Node bvl,
const std::string& fun,
/**
* Make the default sygus datatype type corresponding to builtin type range.
*/
- static TypeNode mkSygusDefaultType(TypeNode range,
+ static TypeNode mkSygusDefaultType(const Options& opts,
+ TypeNode range,
Node bvl,
const std::string& fun)
{
std::map<TypeNode, std::unordered_set<Node>> exclude_cons;
std::map<TypeNode, std::unordered_set<Node>> include_cons;
std::unordered_set<Node> term_irrelevant;
- return mkSygusDefaultType(range,
+ return mkSygusDefaultType(opts,
+ range,
bvl,
fun,
extra_cons,
};
// helper for mkSygusDefaultGrammar (makes unresolved type for mutually recursive datatype construction)
- static TypeNode mkUnresolvedType(const std::string& name,
- std::set<TypeNode>& unres);
+ static TypeNode mkUnresolvedType(const std::string& name);
// collect the list of types that depend on type range
static void collectSygusGrammarTypesFor(TypeNode range,
std::vector<TypeNode>& types);
/** helper function for function mkSygusDefaultType
* Collects a set of mutually recursive datatypes "datatypes" corresponding to
* encoding type "range" to SyGuS.
- * unres is used for the resulting call to mkMutualDatatypeTypes
*/
static void mkSygusDefaultGrammar(
TypeNode range,
const std::map<TypeNode, std::unordered_set<Node>>& include_cons,
std::unordered_set<Node>& term_irrelevant,
std::vector<SygusDatatypeGenerator>& sdts,
- std::set<TypeNode>& unres);
+ options::SygusGrammarConsMode sgcm);
// helper function for mkSygusTemplateType
static TypeNode mkSygusTemplateTypeRec(Node templ,
getIncludeCons(axioms, conj, include_cons);
std::unordered_set<Node> terms_irrelevant;
itpGTypeS = CegGrammarConstructor::mkSygusDefaultType(
+ options(),
NodeManager::currentNM()->booleanType(),
d_ibvlShared,
"interpolation_grammar",
return d_parent->getModelValue(e);
}
EnumTypeInfoStrat* etis = snode.d_strats[itd->second.getStrategyIndex()];
- Node sol = itd->second.buildSol(etis->d_cons, lemmas);
+ Node sol =
+ itd->second.buildSol(etis->d_cons,
+ lemmas,
+ options().quantifiers.sygusUnifShuffleCond,
+ options().quantifiers.sygusUnifCondIndNoRepeatSol);
Assert(d_useCondPool || !sol.isNull() || !lemmas.empty());
return sol;
}
}
Node SygusUnifRl::DecisionTreeInfo::buildSol(Node cons,
- std::vector<Node>& lemmas)
+ std::vector<Node>& lemmas,
+ bool shuffleCond,
+ bool condIndNoRepeatSol)
{
if (!d_template.first.isNull())
{
<< " conditions..." << std::endl;
// reset the trie
d_pt_sep.d_trie.clear();
- return d_unif->usingConditionPool() ? buildSolAllCond(cons, lemmas)
- : buildSolMinCond(cons, lemmas);
+ return d_unif->usingConditionPool()
+ ? buildSolAllCond(cons, lemmas, shuffleCond, condIndNoRepeatSol)
+ : buildSolMinCond(cons, lemmas);
}
Node SygusUnifRl::DecisionTreeInfo::buildSolAllCond(Node cons,
- std::vector<Node>& lemmas)
+ std::vector<Node>& lemmas,
+ bool shuffleCond,
+ bool condIndNoRepeatSol)
{
// model values for evaluation heads
std::map<Node, Node> hd_mv;
// bigger, or have no impact) and which conditions will be present in the DT,
// which influences the "quality" of the solution for cases not covered in the
// current data points
- if (options::sygusUnifShuffleCond())
+ if (shuffleCond)
{
std::shuffle(d_conds.begin(), d_conds.end(), Random::getRandom());
}
Trace("sygus-unif-sol") << "...ready to build solution from DT\n";
Node sol = extractSol(cons, hd_mv);
// repeated solution
- if (options::sygusUnifCondIndNoRepeatSol()
- && d_sols.find(sol) != d_sols.end())
+ if (condIndNoRepeatSol && d_sols.find(sol) != d_sols.end())
{
return Node::null();
}
* A solution is possible when all different valued heads can be separated,
* i.e. the current set of conditions separates them in a decision tree
*/
- Node buildSol(Node cons, std::vector<Node>& lemmas);
+ Node buildSol(Node cons,
+ std::vector<Node>& lemmas,
+ bool shuffleCond,
+ bool condIndNoRepeatSol);
/** bulids a solution by considering all condition values ever enumerated */
- Node buildSolAllCond(Node cons, std::vector<Node>& lemmas);
+ Node buildSolAllCond(Node cons,
+ std::vector<Node>& lemmas,
+ bool shuffleCond,
+ bool condIndNoRepeatSol);
/** builds a solution by incrementally adding points and conditions to DT
*
* Differently from the above method, here a condition is only added to the
for (const Node& var : q[0])
{
addSpecialValues(var.getType(), extra_cons);
- TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(var.getType(),
+ TypeNode tn = CegGrammarConstructor::mkSygusDefaultType(options(),
+ var.getType(),
Node(),
var.toString(),
extra_cons,
projects / cvc5.git / commitdiff