* during Theory's collectModelInfo( ... ) functions.
*/
void assertSkeleton(TNode n);
+ /** set assignment exclusion set
+ *
+ * This method sets the "assignment exclusion set" for term n. This is a
+ * set of terms whose value n must be distinct from in the model.
+ *
+ * This method should be used sparingly, and in a way such that model
+ * building is still guaranteed to succeed. Term n is intended to be an
+ * assignable term, typically of finite type. Thus, for example, this method
+ * should not be called with a vector eset that is greater than the
+ * cardinality of the type of n. Additionally, this method should not be
+ * called in a way that introduces cyclic dependencies on the assignment order
+ * of terms in the model. For example, providing { y } as the assignment
+ * exclusion set of x and { x } as the assignment exclusion set of y will
+ * cause model building to fail.
+ *
+ * The vector eset should contain only terms that occur in the model, or
+ * are constants.
+ *
+ * Additionally, we (currently) require that an assignment exclusion set
+ * should not be set for two terms in the same equivalence class, or to
+ * equivalence classes with an assignable term. Otherwise an
+ * assertion will be thrown by TheoryEngineModelBuilder during model building.
+ */
+ void setAssignmentExclusionSet(TNode n, const std::vector<Node>& eset);
+ /** set assignment exclusion set group
+ *
+ * Given group = { x_1, ..., x_n }, this is semantically equivalent to calling
+ * the above method on the following pairs of arguments:
+ * x1, eset
+ * x2, eset + { x_1 }
+ * ...
+ * xn, eset + { x_1, ..., x_{n-1} }
+ * Similar restrictions should be considered as above when applying this
+ * method to ensure that model building will succeed. Notice that for
+ * efficiency, the implementation of how the above information is stored
+ * may avoid constructing n copies of eset.
+ */
+ void setAssignmentExclusionSetGroup(const std::vector<TNode>& group,
+ const std::vector<Node>& eset);
+ /** get assignment exclusion set for term n
+ *
+ * If n has been given an assignment exclusion set, then this method returns
+ * true and the set is added to eset. Otherwise, the method returns false.
+ *
+ * Additionally, if n was assigned an assignment exclusion set via a call to
+ * setAssignmentExclusionSetGroup, it adds all members that were passed
+ * in the first argument of that call to the vector group. Otherwise, it
+ * adds n itself to group.
+ */
+ bool getAssignmentExclusionSet(TNode n,
+ std::vector<Node>& group,
+ std::vector<Node>& eset);
+ /** have any assignment exclusion sets been created? */
+ bool hasAssignmentExclusionSets() const;
/** record approximation
*
* This notifies this model that the value of n was approximated in this
std::unordered_set<Kind, kind::KindHashFunction> d_not_evaluated_kinds;
/** a set of kinds that are semi-evaluated */
std::unordered_set<Kind, kind::KindHashFunction> d_semi_evaluated_kinds;
- /** map of representatives of equality engine to used representatives in
- * representative set */
+ /**
+ * Map of representatives of equality engine to used representatives in
+ * representative set
+ */
std::map<Node, Node> d_reps;
+ /** Map of terms to their assignment exclusion set. */
+ std::map<Node, std::vector<Node> > d_assignExcSet;
+ /**
+ * Map of terms to their "assignment exclusion set master". After a call to
+ * setAssignmentExclusionSetGroup, the master of each term in group
+ * (except group[0]) is set to group[0], which stores the assignment
+ * exclusion set for that group in the above map.
+ */
+ std::map<Node, Node> d_aesMaster;
+ /** Reverse of the above map */
+ std::map<Node, std::vector<Node> > d_aesSlaves;
/** stores set of representatives for each type */
RepSet d_rep_set;
/** true/false nodes */
namespace CVC4 {
namespace theory {
+void TheoryEngineModelBuilder::Assigner::initialize(
+ TypeNode tn, TypeEnumeratorProperties* tep, const std::vector<Node>& aes)
+{
+ d_te.reset(new TypeEnumerator(tn, tep));
+ d_assignExcSet.insert(d_assignExcSet.end(), aes.begin(), aes.end());
+}
+
+Node TheoryEngineModelBuilder::Assigner::getNextAssignment()
+{
+ Assert(d_te != nullptr);
+ Node n;
+ bool success = false;
+ TypeEnumerator& te = *d_te;
+ // Check if we have run out of elements. This should never happen; if it
+ // does we assert false and return null.
+ if (te.isFinished())
+ {
+ Assert(false);
+ return Node::null();
+ }
+ // must increment until we find one that is not in the assignment
+ // exclusion set
+ do
+ {
+ n = *te;
+ success = std::find(d_assignExcSet.begin(), d_assignExcSet.end(), n)
+ == d_assignExcSet.end();
+ // increment regardless of fail or succeed, to set up the next value
+ ++te;
+ } while (!success);
+ return n;
+}
+
TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
{
}
+Node TheoryEngineModelBuilder::evaluateEqc(TheoryModel* m, TNode r)
+{
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(r, m->d_equalityEngine);
+ for (; !eqc_i.isFinished(); ++eqc_i)
+ {
+ Node n = *eqc_i;
+ Trace("model-builder-debug") << "Look at term : " << n << std::endl;
+ if (!isAssignable(n))
+ {
+ Trace("model-builder-debug") << "...try to normalize" << std::endl;
+ Node normalized = normalize(m, n, true);
+ if (normalized.isConst())
+ {
+ return normalized;
+ }
+ }
+ }
+ return Node::null();
+}
+
+bool TheoryEngineModelBuilder::isAssignerActive(TheoryModel* tm, Assigner& a)
+{
+ if (a.d_isActive)
+ {
+ return true;
+ }
+ std::vector<Node>& eset = a.d_assignExcSet;
+ std::map<Node, Node>::iterator it;
+ for (unsigned i = 0, size = eset.size(); i < size; i++)
+ {
+ // Members of exclusion set must have values, otherwise we are not yet
+ // assignable.
+ Node er = eset[i];
+ if (er.isConst())
+ {
+ // already processed
+ continue;
+ }
+ // Assignable members of assignment exclusion set should be representatives
+ // of their equivalence classes. This ensures we look up the constant
+ // representatives for assignable members of assignment exclusion sets.
+ Assert(er == tm->getRepresentative(er));
+ it = d_constantReps.find(er);
+ if (it == d_constantReps.end())
+ {
+ Trace("model-build-aes")
+ << "isAssignerActive: not active due to " << er << std::endl;
+ return false;
+ }
+ // update
+ eset[i] = it->second;
+ }
+ Trace("model-build-aes") << "isAssignerActive: active!" << std::endl;
+ a.d_isActive = true;
+ return true;
+}
+
bool TheoryEngineModelBuilder::isAssignable(TNode n)
{
if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
{
Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
TheoryModel* tm = (TheoryModel*)m;
+ eq::EqualityEngine* ee = tm->d_equalityEngine;
// buildModel should only be called once per check
Assert(!tm->isBuilt());
// equality engine
// Also, record #eqc per type (for finite model finding)
std::map<TypeNode, unsigned> eqc_usort_count;
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
{
NodeSet cache;
for (; !eqcs_i.isFinished(); ++eqcs_i)
{
- eq::EqClassIterator eqc_i =
- eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine);
+ eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i), ee);
for (; !eqc_i.isFinished(); ++eqc_i)
{
addAssignableSubterms(*eqc_i, tm, cache);
d_constantReps.clear();
std::map<Node, Node> assertedReps;
TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+ // Compute type enumerator properties. This code ensures we do not
+ // enumerate terms that have uninterpreted constants that violate the
+ // bounds imposed by finite model finding. For example, if finite
+ // model finding insists that there are only 2 values { U1, U2 } of type U,
+ // then the type enumerator for list of U should enumerate:
+ // nil, (cons U1 nil), (cons U2 nil), (cons U1 (cons U1 nil)), ...
+ // instead of enumerating (cons U3 nil).
TypeEnumeratorProperties tep;
if (options::finiteModelFind())
{
}
typeConstSet.setTypeEnumeratorProperties(&tep);
}
+
// AJR: build ordered list of types that ensures that base types are
// enumerated first.
// (I think) this is only strictly necessary for finite model finding +
}
}
+ Trace("model-builder") << "Compute assignable information..." << std::endl;
+ // The set of equivalence classes that are "assignable"
+ std::unordered_set<Node, NodeHashFunction> assignableEqc;
+ // The set of equivalence classes that are "evaluable"
+ std::unordered_set<Node, NodeHashFunction> evaluableEqc;
+ // Assigner objects for relevant equivalence classes
+ std::map<Node, Assigner> eqcToAssigner;
+ // Maps equivalence classes to the equivalence class that maps to its assigner
+ // object in the above map.
+ std::map<Node, Node> eqcToAssignerMaster;
+ // Compute the above information
+ computeAssignableInfo(
+ tm, tep, assignableEqc, evaluableEqc, eqcToAssigner, eqcToAssignerMaster);
+
// Need to ensure that each EC has a constant representative.
Trace("model-builder") << "Processing EC's..." << std::endl;
{
Trace("model-builder") << " Eval phase, working on type: " << t
<< endl;
- bool assignable, evaluable, evaluated;
+ bool evaluable;
d_normalizedCache.clear();
for (i = noRepSet->begin(); i != noRepSet->end();)
{
i2 = i;
++i;
- assignable = false;
- evaluable = false;
- evaluated = false;
Trace("model-builder-debug") << "Look at eqc : " << (*i2)
<< std::endl;
- eq::EqClassIterator eqc_i =
- eq::EqClassIterator(*i2, tm->d_equalityEngine);
- for (; !eqc_i.isFinished(); ++eqc_i)
+ Node normalized;
+ // only possible to normalize if we are evaluable
+ evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
+ if (evaluable)
{
- Node n = *eqc_i;
- Trace("model-builder-debug") << "Look at term : " << n
- << std::endl;
- if (isAssignable(n))
- {
- assignable = true;
- Trace("model-builder-debug") << "...assignable" << std::endl;
- }
- else
- {
- evaluable = true;
- Trace("model-builder-debug") << "...try to normalize"
- << std::endl;
- Node normalized = normalize(tm, n, true);
- if (normalized.isConst())
- {
- typeConstSet.add(tb, normalized);
- assignConstantRep(tm, *i2, normalized);
- Trace("model-builder") << " Eval: Setting constant rep of "
- << (*i2) << " to " << normalized
- << endl;
- changed = true;
- evaluated = true;
- noRepSet->erase(i2);
- break;
- }
- }
+ normalized = evaluateEqc(tm, *i2);
}
- if (!evaluated)
+ if (!normalized.isNull())
+ {
+ Assert(normalized.isConst());
+ typeConstSet.add(tb, normalized);
+ assignConstantRep(tm, *i2, normalized);
+ Trace("model-builder") << " Eval: Setting constant rep of "
+ << (*i2) << " to " << normalized << endl;
+ changed = true;
+ noRepSet->erase(i2);
+ }
+ else
{
if (evaluable)
{
evaluableSet.insert(tb);
}
- if (assignable)
+ // If assignable, remember there is an equivalence class that is
+ // not assigned and assignable.
+ if (assignableEqc.find(*i2) != assignableEqc.end())
{
unassignedAssignable = true;
}
Trace("model-builder") << " Assign phase, working on type: " << t
<< endl;
bool assignable, evaluable CVC4_UNUSED;
+ std::map<Node, Assigner>::iterator itAssigner;
+ std::map<Node, Node>::iterator itAssignerM;
for (i = noRepSet.begin(); i != noRepSet.end();)
{
i2 = i;
++i;
- eq::EqClassIterator eqc_i =
- eq::EqClassIterator(*i2, tm->d_equalityEngine);
- assignable = false;
- evaluable = false;
- for (; !eqc_i.isFinished(); ++eqc_i)
+ // check whether it has an assigner object
+ itAssignerM = eqcToAssignerMaster.find(*i2);
+ if (itAssignerM != eqcToAssignerMaster.end())
{
- Node n = *eqc_i;
- if (isAssignable(n))
- {
- assignable = true;
- }
- else
- {
- evaluable = true;
- }
+ // Take the master's assigner. Notice we don't care which order
+ // equivalence classes are assigned. For instance, the master can
+ // be assigned after one of its slaves.
+ itAssigner = eqcToAssigner.find(itAssignerM->second);
+ }
+ else
+ {
+ itAssigner = eqcToAssigner.find(*i2);
}
+ if (itAssigner != eqcToAssigner.end())
+ {
+ assignable = isAssignerActive(tm, itAssigner->second);
+ }
+ else
+ {
+ assignable = assignableEqc.find(*i2) != assignableEqc.end();
+ }
+ evaluable = evaluableEqc.find(*i2) != evaluableEqc.end();
Trace("model-builder-debug")
<< " eqc " << *i2 << " is assignable=" << assignable
<< ", evaluable=" << evaluable << std::endl;
Assert(!t.isBoolean() || (*i2).isVar()
|| (*i2).getKind() == kind::APPLY_UF);
Node n;
- if (!t.isFinite())
+ if (itAssigner != eqcToAssigner.end())
+ {
+ Trace("model-builder-debug")
+ << "Get value from assigner for finite type..." << std::endl;
+ // if it has an assigner, get the value from the assigner.
+ n = itAssigner->second.getNextAssignment();
+ Assert(!n.isNull());
+ }
+ else if (!t.isFinite())
{
+ // if its infinite, we get a fresh value that does not occur in
+ // the model.
bool success;
do
{
}
//---
} while (!success);
+ Assert(!n.isNull());
}
else
{
+ Trace("model-builder-debug")
+ << "Get first value from finite type..." << std::endl;
+ // Otherwise, we get the first value from the type enumerator.
TypeEnumerator te(t);
n = *te;
}
- Assert(!n.isNull());
+ Trace("model-builder-debug") << "...got " << n << std::endl;
assignConstantRep(tm, *i2, n);
changed = true;
noRepSet.erase(i2);
tm->d_modelBuiltSuccess = true;
return true;
}
+void TheoryEngineModelBuilder::computeAssignableInfo(
+ TheoryModel* tm,
+ TypeEnumeratorProperties& tep,
+ std::unordered_set<Node, NodeHashFunction>& assignableEqc,
+ std::unordered_set<Node, NodeHashFunction>& evaluableEqc,
+ std::map<Node, Assigner>& eqcToAssigner,
+ std::map<Node, Node>& eqcToAssignerMaster)
+{
+ eq::EqualityEngine* ee = tm->d_equalityEngine;
+ bool computeAssigners = tm->hasAssignmentExclusionSets();
+ std::unordered_set<Node, NodeHashFunction> processed;
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(ee);
+ // A flag set to true if the current equivalence class is assignable (see
+ // assignableEqc).
+ bool assignable = false;
+ // Set to true if the current equivalence class is evaluatable (see
+ // evaluableEqc).
+ bool evaluable = false;
+ // Set to true if a term in the current equivalence class has been given an
+ // assignment exclusion set.
+ bool hasESet = false;
+ // Set to true if we found that a term in the current equivalence class has
+ // been given an assignment exclusion set, and we have not seen this term
+ // as part of a previous assignment exclusion group. In other words, when
+ // this flag is true we construct a new assigner object with the current
+ // equivalence class as its master.
+ bool foundESet = false;
+ // Look at all equivalence classes in the model
+ for (; !eqcs_i.isFinished(); ++eqcs_i)
+ {
+ Node eqc = *eqcs_i;
+ if (d_constantReps.find(eqc) != d_constantReps.end())
+ {
+ // already assigned above, skip
+ continue;
+ }
+ // reset information for the current equivalence classe
+ assignable = false;
+ evaluable = false;
+ hasESet = false;
+ foundESet = false;
+ // the assignment exclusion set for the current equivalence class
+ std::vector<Node> eset;
+ // the group to which this equivalence class belongs when exclusion sets
+ // were assigned (see the argument group of
+ // TheoryModel::getAssignmentExclusionSet).
+ std::vector<Node> group;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, ee);
+ // For each term in the current equivalence class, we update the above
+ // information. We may terminate this loop before looking at all terms if we
+ // have inferred the value of all of the information above.
+ for (; !eqc_i.isFinished(); ++eqc_i)
+ {
+ Node n = *eqc_i;
+ if (!isAssignable(n))
+ {
+ evaluable = true;
+ if (!computeAssigners)
+ {
+ if (assignable)
+ {
+ // both flags set, we are done
+ break;
+ }
+ }
+ // expressions that are not assignable should not be given assignment
+ // exclusion sets
+ Assert(!tm->getAssignmentExclusionSet(n, group, eset));
+ continue;
+ }
+ else
+ {
+ assignable = true;
+ if (!computeAssigners)
+ {
+ if (evaluable)
+ {
+ // both flags set, we are done
+ break;
+ }
+ // we don't compute assigners, skip
+ continue;
+ }
+ }
+ // process the assignment exclusion set for term n
+ // was it processed as a slave of a group?
+ if (processed.find(n) != processed.end())
+ {
+ // Should not have two assignment exclusion sets for the same
+ // equivalence class
+ Assert(!hasESet);
+ Assert(eqcToAssignerMaster.find(eqc) != eqcToAssignerMaster.end());
+ // already processed as a slave term
+ hasESet = true;
+ continue;
+ }
+ // was it assigned one?
+ if (tm->getAssignmentExclusionSet(n, group, eset))
+ {
+ // Should not have two assignment exclusion sets for the same
+ // equivalence class
+ Assert(!hasESet);
+ foundESet = true;
+ hasESet = true;
+ }
+ }
+ if (assignable)
+ {
+ assignableEqc.insert(eqc);
+ }
+ if (evaluable)
+ {
+ evaluableEqc.insert(eqc);
+ }
+ // If we found an assignment exclusion set, we construct a new assigner
+ // object.
+ if (foundESet)
+ {
+ // we don't accept assignment exclusion sets for evaluable eqc
+ Assert(!evaluable);
+ // construct the assigner
+ Assigner& a = eqcToAssigner[eqc];
+ // Take the representatives of each term in the assignment exclusion
+ // set, which ensures we can look up their value in d_constReps later.
+ std::vector<Node> aes;
+ for (const Node& e : eset)
+ {
+ // Should only supply terms that occur in the model or constants
+ // in assignment exclusion sets.
+ Assert(tm->hasTerm(e) || e.isConst());
+ Node er = tm->hasTerm(e) ? tm->getRepresentative(e) : e;
+ aes.push_back(er);
+ }
+ // initialize
+ a.initialize(eqc.getType(), &tep, aes);
+ // all others in the group are slaves of this
+ for (const Node& g : group)
+ {
+ Assert(isAssignable(g));
+ if (!tm->hasTerm(g))
+ {
+ // Ignore those that aren't in the model, in the case the user
+ // has supplied an assignment exclusion set to a variable not in
+ // the model.
+ continue;
+ }
+ Node gr = tm->getRepresentative(g);
+ if (gr != eqc)
+ {
+ eqcToAssignerMaster[gr] = eqc;
+ // remember that this term has been processed
+ processed.insert(g);
+ }
+ }
+ }
+ }
+}
void TheoryEngineModelBuilder::postProcessModel(bool incomplete, Model* m)
{
*/
void debugCheckModel(TheoryModel* m);
- /** is n assignable?
+ /** Evaluate equivalence class
*
- * A term n is assignable if its value
- * is unconstrained by a standard model.
- * Examples of assignable terms are:
+ * If this method returns a non-null node c, then c is a constant and some
+ * term in the equivalence class of r evaluates to c based on the current
+ * state of the model m.
+ */
+ Node evaluateEqc(TheoryModel* m, TNode r);
+ /** is n an assignable expression?
+ *
+ * A term n is an assignable expression if its value is unconstrained by a
+ * standard model. Examples of assignable terms are:
* - variables,
* - applications of array select,
* - applications of datatype selectors,
* - applications of uninterpreted functions.
- * Assignable terms must be first-order, that is,
- * all instances of the above terms are not
- * assignable if they have a higher-order (function) type.
+ * Assignable terms must be first-order, that is, all instances of the above
+ * terms are not assignable if they have a higher-order (function) type.
*/
bool isAssignable(TNode n);
/** add assignable subterms
*/
std::map<Node, Node> d_constantReps;
+ /** Theory engine model builder assigner class
+ *
+ * This manages the assignment of values to terms of a given type.
+ * In particular, it is a wrapper around a type enumerator that is restricted
+ * by a set of values that it cannot generate, called an "assignment exclusion
+ * set".
+ */
+ class Assigner
+ {
+ public:
+ Assigner() : d_te(nullptr), d_isActive(false) {}
+ /**
+ * Initialize this assigner to generate values of type tn, with properties
+ * tep and assignment exclusion set aes.
+ */
+ void initialize(TypeNode tn,
+ TypeEnumeratorProperties* tep,
+ const std::vector<Node>& aes);
+ /** get the next term in the enumeration
+ *
+ * This method returns the next legal term based on type enumeration, where
+ * a term is legal it does not belong to the assignment exclusion set of
+ * this assigner. If no more terms exist, this method returns null. This
+ * should never be the case due to the conditions ensured by theory solvers
+ * for finite types. If it is the case, we give an assertion failure.
+ */
+ Node getNextAssignment();
+ /** The type enumerator */
+ std::unique_ptr<TypeEnumerator> d_te;
+ /** The assignment exclusion set of this Assigner */
+ std::vector<Node> d_assignExcSet;
+ /**
+ * Is active, flag set to true when all values in d_assignExcSet are
+ * constant.
+ */
+ bool d_isActive;
+ };
+ /** Is the given Assigner ready to assign values?
+ *
+ * This returns true if all values in the assignment exclusion set of a have
+ * a known value according to the state of this model builder (via a lookup
+ * in d_constantReps). It updates the assignment exclusion vector of a to
+ * these values whenever possible.
+ */
+ bool isAssignerActive(TheoryModel* tm, Assigner& a);
+ /** compute assignable information
+ *
+ * This computes necessary information pertaining to how values should be
+ * assigned to equivalence classes in the equality engine of tm.
+ *
+ * The argument tep stores global information about how values should be
+ * assigned, such as information on how many uninterpreted constant
+ * values are available, which is restricted if finite model finding is
+ * enabled.
+ *
+ * In particular this method constructs the following, passed as arguments:
+ * (1) assignableEqc: the set of equivalence classes that are "assignable",
+ * i.e. those that have an assignable expression in them (see isAssignable),
+ * and have not already been assigned a constant,
+ * (2) evaluableEqc: the set of equivalence classes that are "evaluable", i.e.
+ * those that have an expression in them that is not assignable, and have not
+ * already been assigned a constant,
+ * (3) eqcToAssigner: assigner objects for relevant equivalence classes that
+ * require special ways of assigning values, e.g. those that take into
+ * account assignment exclusion sets,
+ * (4) eqcToAssignerMaster: a map from equivalence classes to the equivalence
+ * class that it shares an assigner object with (all elements in the range of
+ * this map are in the domain of eqcToAssigner).
+ */
+ void computeAssignableInfo(
+ TheoryModel* tm,
+ TypeEnumeratorProperties& tep,
+ std::unordered_set<Node, NodeHashFunction>& assignableEqc,
+ std::unordered_set<Node, NodeHashFunction>& evaluableEqc,
+ std::map<Node, Assigner>& eqcToAssigner,
+ std::map<Node, Node>& eqcToAssignerMaster);
//------------------------------------for codatatypes
/** is v an excluded codatatype value?
*
projects / cvc5.git / commitdiff