* Move type set to its own file and document.
* Move theory engine model builder to its own class.
* Working on documentation.
* Document Theory Model.
* Minor
* Document theory model builder.
* Clang format
* Address review.
theory/theory_engine.h \
theory/theory_model.cpp \
theory/theory_model.h \
+ theory/theory_model_builder.cpp \
+ theory/theory_model_builder.h \
theory/theory_registrar.h \
theory/theory_test_utils.h \
theory/type_enumerator.h \
+ theory/type_set.cpp \
+ theory/type_set.h \
theory/unconstrained_simplifier.cpp \
theory/unconstrained_simplifier.h \
theory/valuation.cpp \
#define __CVC4__THEORY__QUANTIFIERS__MODEL_BUILDER_H
#include "theory/quantifiers_engine.h"
-#include "theory/theory_model.h"
+#include "theory/theory_model_builder.h"
#include "theory/uf/theory_uf_model.h"
namespace CVC4 {
printAssertions("theory::assertions-model");
}
//checks for theories requiring the model go at last call
- d_curr_model->setNeedsBuild();
+ d_curr_model->reset();
for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
if( theoryId!=THEORY_QUANTIFIERS ){
Theory* theory = d_theoryTable[theoryId];
**/
#include "theory/theory_model.h"
+#include "options/quantifiers_options.h"
#include "options/smt_options.h"
#include "options/uf_options.h"
-#include "options/quantifiers_options.h"
#include "smt/smt_engine.h"
-#include "theory/quantifiers_engine.h"
-#include "theory/theory_engine.h"
-#include "theory/type_enumerator.h"
-#include "theory/uf/theory_uf_model.h"
using namespace std;
using namespace CVC4::kind;
}
void TheoryModel::reset(){
+ d_modelBuilt = false;
d_modelCache.clear();
d_comment_str.clear();
d_sep_heap = Node::null();
return funcs_to_assign;
}
-TheoryEngineModelBuilder::TheoryEngineModelBuilder( TheoryEngine* te ) : d_te( te ){
-
-}
-
-
-bool TheoryEngineModelBuilder::isAssignable(TNode n)
-{
- if( n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL ){
- // selectors are always assignable (where we guarantee that they are not evaluatable here)
- if( !options::ufHo() ){
- Assert( !n.getType().isFunction() );
- return true;
- }else{
- // might be a function field
- return !n.getType().isFunction();
- }
- }else{
- // non-function variables, and fully applied functions
- if( !options::ufHo() ){
- // no functions exist, all functions are fully applied
- Assert( n.getKind() != kind::HO_APPLY );
- Assert( !n.getType().isFunction() );
- return n.isVar() || n.getKind() == kind::APPLY_UF;
- }else{
- //Assert( n.getKind() != kind::APPLY_UF );
- return ( n.isVar() && !n.getType().isFunction() ) || n.getKind() == kind::APPLY_UF ||
- ( n.getKind() == kind::HO_APPLY && n[0].getType().getNumChildren()==2 );
- }
- }
-}
-
-
-void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cache)
-{
- if (n.getKind()==FORALL || n.getKind()==EXISTS) {
- return;
- }
- if (cache.find(n) != cache.end()) {
- return;
- }
- if (isAssignable(n)) {
- tm->d_equalityEngine->addTerm(n);
- }
- for(TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it) {
- checkTerms(*child_it, tm, cache);
- }
- cache.insert(n);
-}
-
-void TheoryEngineModelBuilder::assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep ) {
- d_constantReps[eqc] = const_rep;
- Trace("model-builder") << " Assign: Setting constant rep of " << eqc << " to " << const_rep << endl;
- tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
-}
-
-bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) {
- Trace("model-builder-debug") << "Is " << val << " and excluded codatatype value for " << eqc << "? " << std::endl;
- for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i ) {
- Assert(assertedReps.find(*i) != assertedReps.end());
- Node rep = assertedReps[*i];
- Trace("model-builder-debug") << " Rep : " << rep << std::endl;
- //check matching val to rep with eqc as a free variable
- Node eqc_m;
- if( isCdtValueMatch( val, rep, eqc, eqc_m ) ){
- Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl;
- if( eqc_m.getKind()==kind::UNINTERPRETED_CONSTANT ){
- Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc << std::endl;
- return true;
- }
- }
- }
- return false;
-}
-
-bool TheoryEngineModelBuilder::isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m ) {
- if( r==v ){
- return true;
- }else if( r==eqc ){
- if( eqc_m.isNull() ){
- //only if an uninterpreted constant?
- eqc_m = v;
- return true;
- }else{
- return v==eqc_m;
- }
- }else if( v.getKind()==kind::APPLY_CONSTRUCTOR && r.getKind()==kind::APPLY_CONSTRUCTOR ){
- if( v.getOperator()==r.getOperator() ){
- for( unsigned i=0; i<v.getNumChildren(); i++ ){
- if( !isCdtValueMatch( v[i], r[i], eqc, eqc_m ) ){
- return false;
- }
- }
- return true;
- }
- }
- return false;
-}
-
-bool TheoryEngineModelBuilder::involvesUSort( TypeNode tn ) {
- if( tn.isSort() ){
- return true;
- }else if( tn.isArray() ){
- return involvesUSort( tn.getArrayIndexType() ) || involvesUSort( tn.getArrayConstituentType() );
- }else if( tn.isSet() ){
- return involvesUSort( tn.getSetElementType() );
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- return dt.involvesUninterpretedType();
- }else{
- return false;
- }
-}
-
-bool TheoryEngineModelBuilder::isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited ) {
- Assert( v.isConst() );
- if( visited.find( v )==visited.end() ){
- visited[v] = true;
- TypeNode tn = v.getType();
- if( tn.isSort() ){
- Trace("model-builder-debug") << "Is excluded usort value : " << v << " " << tn << std::endl;
- unsigned card = eqc_usort_count[tn];
- Trace("model-builder-debug") << " Cardinality is " << card << std::endl;
- unsigned index = v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
- Trace("model-builder-debug") << " Index is " << index << std::endl;
- return index>0 && index>=card;
- }
- for( unsigned i=0; i<v.getNumChildren(); i++ ){
- if( isExcludedUSortValue( eqc_usort_count, v[i], visited ) ){
- return true;
- }
- }
- }
- return false;
-}
-
-
-void TheoryEngineModelBuilder::addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list,
- std::map< TypeNode, bool >& visiting ){
- if( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() ){
- if( visiting.find( tn )==visiting.end() ){
- visiting[tn] = true;
- /* This must make a recursive call on all types that are subterms of
- * values of the current type.
- * Note that recursive traversal here is over enumerated expressions
- * (very low expression depth). */
- if( tn.isArray() ){
- addToTypeList( tn.getArrayIndexType(), type_list, visiting );
- addToTypeList( tn.getArrayConstituentType(), type_list, visiting );
- }else if( tn.isSet() ){
- addToTypeList( tn.getSetElementType(), type_list, visiting );
- }else if( tn.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
- for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
- for( unsigned j=0; j<dt[i].getNumArgs(); j++ ){
- TypeNode ctn = TypeNode::fromType( dt[i][j].getRangeType() );
- addToTypeList( ctn, type_list, visiting );
- }
- }
- }
- Assert( std::find( type_list.begin(), type_list.end(), tn )==type_list.end() );
- type_list.push_back( tn );
- }
- }
-}
-
-bool TheoryEngineModelBuilder::buildModel(Model* m)
-{
- Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
- TheoryModel* tm = (TheoryModel*)m;
-
- // buildModel should only be called once per check
- Assert(!tm->isBuilt());
- tm->d_modelBuilt = true;
-
- // Reset model
- tm->reset();
-
- // Collect model info from the theories
- Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..." << std::endl;
- d_te->collectModelInfo(tm);
-
- // model-builder specific initialization
- if( !preProcessBuildModel(tm) ){
- return false;
- }
-
- // Loop through all terms and make sure that assignable sub-terms are in the 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 );
- {
- NodeSet cache;
- for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
- eq::EqClassIterator eqc_i = eq::EqClassIterator((*eqcs_i),tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- checkTerms(*eqc_i, tm, cache);
- }
- TypeNode tn = (*eqcs_i).getType();
- if( tn.isSort() ){
- if( eqc_usort_count.find( tn )==eqc_usort_count.end() ){
- eqc_usort_count[tn] = 1;
- }else{
- eqc_usort_count[tn]++;
- }
- }
- }
- }
-
- Trace("model-builder") << "Collect representatives..." << std::endl;
-
- // Process all terms in the equality engine, store representatives for each EC
- d_constantReps.clear();
- std::map< Node, Node > assertedReps;
- TypeSet typeConstSet, typeRepSet, typeNoRepSet;
- TypeEnumeratorProperties tep;
- if( options::finiteModelFind() ){
- tep.d_fixed_usort_card = true;
- for( std::map< TypeNode, unsigned >::iterator it = eqc_usort_count.begin(); it != eqc_usort_count.end(); ++it ){
- Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : " << it->second << std::endl;
- tep.d_fixed_card[it->first] = Integer(it->second);
- }
- 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 + parametric types
- // instantiated with uninterpreted sorts, but is probably a good idea to do in general
- // since it leads to models with smaller term sizes.
- std::vector< TypeNode > type_list;
- eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
- for ( ; !eqcs_i.isFinished(); ++eqcs_i) {
-
- // eqc is the equivalence class representative
- Node eqc = (*eqcs_i);
- Trace("model-builder") << "Processing EC: " << eqc << endl;
- Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
- TypeNode eqct = eqc.getType();
- Assert(assertedReps.find(eqc) == assertedReps.end());
- Assert(d_constantReps.find(eqc) == d_constantReps.end());
-
- // Loop through terms in this EC
- Node rep, const_rep;
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- Trace("model-builder") << " Processing Term: " << n << endl;
- // Record as rep if this node was specified as a representative
- if (tm->d_reps.find(n) != tm->d_reps.end()){
- //AJR: I believe this assertion is too strict,
- // e.g. datatypes may assert representative for two constructor terms that are not in the care graph and are merged during collectModelInfo.
- //Assert(rep.isNull());
- rep = tm->d_reps[n];
- Assert(!rep.isNull() );
- Trace("model-builder") << " Rep( " << eqc << " ) = " << rep << std::endl;
- }
- // Record as const_rep if this node is constant
- if (n.isConst()) {
- Assert(const_rep.isNull());
- const_rep = n;
- Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep << std::endl;
- }
- //model-specific processing of the term
- tm->addTerm(n);
- }
-
- // Assign representative for this EC
- if (!const_rep.isNull()) {
- // Theories should not specify a rep if there is already a constant in the EC
- //AJR: I believe this assertion is too strict, eqc with asserted reps may merge with constant eqc
- //Assert(rep.isNull() || rep == const_rep);
- assignConstantRep( tm, eqc, const_rep );
- typeConstSet.add(eqct.getBaseType(), const_rep);
- }
- else if (!rep.isNull()) {
- assertedReps[eqc] = rep;
- typeRepSet.add(eqct.getBaseType(), eqc);
- std::map< TypeNode, bool > visiting;
- addToTypeList(eqct.getBaseType(), type_list, visiting);
- }
- else {
- typeNoRepSet.add(eqct, eqc);
- std::map< TypeNode, bool > visiting;
- addToTypeList(eqct, type_list, visiting);
- }
- }
-
- // Need to ensure that each EC has a constant representative.
-
- Trace("model-builder") << "Processing EC's..." << std::endl;
-
- TypeSet::iterator it;
- vector<TypeNode>::iterator type_it;
- set<Node>::iterator i, i2;
- bool changed, unassignedAssignable, assignOne = false;
- set<TypeNode> evaluableSet;
-
- // Double-fixed-point loop
- // Outer loop handles a special corner case (see code at end of loop for details)
- for (;;) {
-
- // Inner fixed-point loop: we are trying to learn constant values for every EC. Each time through this loop, we process all of the
- // types by type and may learn some new EC values. EC's in one type may depend on EC's in another type, so we need a fixed-point loop
- // to ensure that we learn as many EC values as possible
- do {
- changed = false;
- unassignedAssignable = false;
- evaluableSet.clear();
-
- // Iterate over all types we've seen
- for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) {
- TypeNode t = *type_it;
- TypeNode tb = t.getBaseType();
- set<Node>* noRepSet = typeNoRepSet.getSet(t);
-
- // 1. Try to evaluate the EC's in this type
- if (noRepSet != NULL && !noRepSet->empty()) {
- Trace("model-builder") << " Eval phase, working on type: " << t << endl;
- bool assignable, evaluable, evaluated;
- 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 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;
- }
- }
- }
- if (!evaluated) {
- if (evaluable) {
- evaluableSet.insert(tb);
- }
- if (assignable) {
- unassignedAssignable = true;
- }
- }
- }
- }
-
- // 2. Normalize any non-const representative terms for this type
- set<Node>* repSet = typeRepSet.getSet(t);
- if (repSet != NULL && !repSet->empty()) {
- Trace("model-builder") << " Normalization phase, working on type: " << t << endl;
- d_normalizedCache.clear();
- for (i = repSet->begin(); i != repSet->end(); ) {
- Assert(assertedReps.find(*i) != assertedReps.end());
- Node rep = assertedReps[*i];
- Node normalized = normalize(tm, rep, false);
- Trace("model-builder") << " Normalizing rep (" << rep << "), normalized to (" << normalized << ")" << endl;
- if (normalized.isConst()) {
- changed = true;
- typeConstSet.add(tb, normalized);
- assignConstantRep( tm, *i, normalized);
- assertedReps.erase(*i);
- i2 = i;
- ++i;
- repSet->erase(i2);
- }
- else {
- if (normalized != rep) {
- assertedReps[*i] = normalized;
- changed = true;
- }
- ++i;
- }
- }
- }
- }
- } while (changed);
-
- if (!unassignedAssignable) {
- break;
- }
-
- // 3. Assign unassigned assignable EC's using type enumeration - assign a value *different* from all other EC's if the type is infinite
- // Assign first value from type enumerator otherwise - for finite types, we rely on polite framework to ensure that EC's that have to be
- // different are different.
-
- // Only make assignments on a type if:
- // 1. there are no terms that share the same base type with un-normalized representatives
- // 2. there are no terms that share teh same base type that are unevaluated evaluable terms
- // Alternatively, if 2 or 3 don't hold but we are in a special deadlock-breaking mode where assignOne is true, go ahead and make one assignment
- changed = false;
- //must iterate over the ordered type list to ensure that we do not enumerate values with subterms
- // having types that we are currently enumerating (when possible)
- // for example, this ensures we enumerate uninterpreted sort U before (List of U) and (Array U U)
- // however, it does not break cyclic type dependencies for mutually recursive datatypes, but this is handled
- // by recording all subterms of enumerated values in TypeSet::addSubTerms.
- for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it) {
- TypeNode t = *type_it;
- // continue if there are no more equivalence classes of this type to assign
- std::set<Node>* noRepSetPtr = typeNoRepSet.getSet( t );
- if( noRepSetPtr==NULL ){
- continue;
- }
- set<Node>& noRepSet = *noRepSetPtr;
- if (noRepSet.empty()) {
- continue;
- }
-
- //get properties of this type
- bool isCorecursive = false;
- if( t.isDatatype() ){
- const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
- isCorecursive = dt.isCodatatype() && ( !dt.isFinite( t.toType() ) || dt.isRecursiveSingleton( t.toType() ) );
- }
-#ifdef CVC4_ASSERTIONS
- bool isUSortFiniteRestricted = false;
- if( options::finiteModelFind() ){
- isUSortFiniteRestricted = !t.isSort() && involvesUSort( t );
- }
-#endif
-
- set<Node>* repSet = typeRepSet.getSet(t);
- TypeNode tb = t.getBaseType();
- if (!assignOne) {
- set<Node>* repSet = typeRepSet.getSet(tb);
- if (repSet != NULL && !repSet->empty()) {
- continue;
- }
- if (evaluableSet.find(tb) != evaluableSet.end()) {
- continue;
- }
- }
- Trace("model-builder") << " Assign phase, working on type: " << t << endl;
- bool assignable, evaluable CVC4_UNUSED;
- 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) {
- Node n = *eqc_i;
- if (isAssignable(n)) {
- assignable = true;
- }
- else {
- evaluable = true;
- }
- }
- Trace("model-builder-debug") << " eqc " << *i2 << " is assignable=" << assignable << ", evaluable=" << evaluable << std::endl;
- if (assignable) {
- Assert(!evaluable || assignOne);
- Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
- Node n;
- if (t.getCardinality().isInfinite()) {
- // if (!t.isInterpretedFinite()) {
- bool success;
- do{
- Trace("model-builder-debug") << "Enumerate term of type " << t << std::endl;
- n = typeConstSet.nextTypeEnum(t, true);
- //--- AJR: this code checks whether n is a legal value
- Assert( !n.isNull() );
- success = true;
- Trace("model-builder-debug") << "Check if excluded : " << n << std::endl;
-#ifdef CVC4_ASSERTIONS
- if( isUSortFiniteRestricted ){
- //must not involve uninterpreted constants beyond cardinality bound (which assumed to coincide with #eqc)
- //this is just an assertion now, since TypeEnumeratorProperties should ensure that only legal values are enumerated wrt this constraint.
- std::map< Node, bool > visited;
- success = !isExcludedUSortValue( eqc_usort_count, n, visited );
- if( !success ){
- Trace("model-builder") << "Excluded value for " << t << " : " << n << " due to out of range uninterpreted constant." << std::endl;
- }
- Assert( success );
- }
-#endif
- if( success && isCorecursive ){
- if (repSet != NULL && !repSet->empty()) {
- // in the case of codatatypes, check if it is in the set of values that we cannot assign
- // this will check whether n \not\in V^x_I from page 9 of Reynolds/Blanchette CADE 2015
- success = !isExcludedCdtValue( n, repSet, assertedReps, *i2 );
- if( !success ){
- Trace("model-builder") << "Excluded value : " << n << " due to alpha-equivalent codatatype expression." << std::endl;
- }
- }
- }
- //---
- }while( !success );
- }
- else {
- TypeEnumerator te(t);
- n = *te;
- }
- Assert(!n.isNull());
- assignConstantRep( tm, *i2, n);
- changed = true;
- noRepSet.erase(i2);
- if (assignOne) {
- assignOne = false;
- break;
- }
- }
- }
- }
-
- // Corner case - I'm not sure this can even happen - but it's theoretically possible to have a cyclical dependency
- // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In this case, neither one will get assigned because we are waiting
- // to be able to evaluate. But we will never be able to evaluate because the variables that need to be assigned are in
- // these same EC's. In this case, repeat the whole fixed-point computation with the difference that the first EC
- // that has both assignable and evaluable expressions will get assigned.
- if (!changed) {
- Assert(!assignOne); // check for infinite loop!
- assignOne = true;
- }
- }
-
-#ifdef CVC4_ASSERTIONS
- // Assert that all representatives have been converted to constants
- for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it) {
- set<Node>& repSet = TypeSet::getSet(it);
- if (!repSet.empty()) {
- Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size() << ", first = " << *(repSet.begin()) << endl;
- Assert(false);
- }
- }
-#endif /* CVC4_ASSERTIONS */
-
- Trace("model-builder") << "Copy representatives to model..." << std::endl;
- tm->d_reps.clear();
- std::map< Node, Node >::iterator itMap;
- for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap) {
- tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second.getType(), itMap->second);
- }
-
- Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
- // Make sure every EC has a rep
- for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap ) {
- tm->d_reps[itMap->first] = itMap->second;
- tm->d_rep_set.add(itMap->second.getType(), itMap->second);
- }
- for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it) {
- set<Node>& noRepSet = TypeSet::getSet(it);
- set<Node>::iterator i;
- for (i = noRepSet.begin(); i != noRepSet.end(); ++i) {
- tm->d_reps[*i] = *i;
- tm->d_rep_set.add((*i).getType(), *i);
- }
- }
-
- //modelBuilder-specific initialization
- if( !processBuildModel( tm ) ){
- return false;
- }else{
- return true;
- }
-}
-
-void TheoryEngineModelBuilder::debugCheckModel(Model* m){
- TheoryModel* tm = (TheoryModel*)m;
-#ifdef CVC4_ASSERTIONS
- Assert(tm->isBuilt());
- eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( tm->d_equalityEngine );
- std::map< Node, Node >::iterator itMap;
- // Check that every term evaluates to its representative in the model
- for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine); !eqcs_i.isFinished(); ++eqcs_i) {
- // eqc is the equivalence class representative
- Node eqc = (*eqcs_i);
- // get the representative
- Node rep = tm->getRepresentative( eqc );
- if( !rep.isConst() && eqc.getType().isBoolean() ){
- // if Boolean, it does not necessarily have a constant representative, use get value instead
- rep = tm->getValue(eqc);
- Assert(rep.isConst());
- }
- eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
- for ( ; !eqc_i.isFinished(); ++eqc_i) {
- Node n = *eqc_i;
- static int repCheckInstance = 0;
- ++repCheckInstance;
-
- // non-linear mult is not necessarily accurate wrt getValue
- if( n.getKind()!=kind::NONLINEAR_MULT ){
- Debug("check-model::rep-checking")
- << "( " << repCheckInstance <<") "
- << "n: " << n << endl
- << "getValue(n): " << tm->getValue(n) << endl
- << "rep: " << rep << endl;
- Assert(tm->getValue(*eqc_i) == rep, "run with -d check-model::rep-checking for details");
- }
- }
- }
-#endif /* CVC4_ASSERTIONS */
-
- // builder-specific debugging
- debugModel( tm );
-}
-
-Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
-{
- std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
- if (itMap != d_constantReps.end()) {
- return (*itMap).second;
- }
- NodeMap::iterator it = d_normalizedCache.find(r);
- if (it != d_normalizedCache.end()) {
- return (*it).second;
- }
- Trace("model-builder-debug") << "do normalize on " << r << std::endl;
- Node retNode = r;
- if (r.getNumChildren() > 0) {
- std::vector<Node> children;
- if (r.getMetaKind() == kind::metakind::PARAMETERIZED) {
- children.push_back(r.getOperator());
- }
- bool childrenConst = true;
- for (size_t i=0; i < r.getNumChildren(); ++i) {
- Node ri = r[i];
- bool recurse = true;
- if (!ri.isConst()) {
- if (m->d_equalityEngine->hasTerm(ri)) {
- itMap = d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
- if (itMap != d_constantReps.end()) {
- ri = (*itMap).second;
- recurse = false;
- }
- else if (!evalOnly) {
- recurse = false;
- }
- }
- if (recurse) {
- ri = normalize(m, ri, evalOnly);
- }
- if (!ri.isConst()) {
- childrenConst = false;
- }
- }
- children.push_back(ri);
- }
- retNode = NodeManager::currentNM()->mkNode( r.getKind(), children );
- if (childrenConst) {
- retNode = Rewriter::rewrite(retNode);
- Assert(retNode.getKind() == kind::APPLY_UF
- || !retNode.getType().isFirstClass()
- || retNode.isConst());
- }
- }
- d_normalizedCache[r] = retNode;
- return retNode;
-}
-
-bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m) {
- return true;
-}
-
-bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m){
- assignFunctions(m);
- return true;
-}
-
-void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f) {
- Assert( !options::ufHo() );
- uf::UfModelTree ufmt( f );
- Node default_v;
- for( size_t i=0; i<m->d_uf_terms[f].size(); i++ ){
- Node un = m->d_uf_terms[f][i];
- vector<TNode> children;
- children.push_back(f);
- Trace("model-builder-debug") << " process term : " << un << std::endl;
- for (size_t j = 0; j < un.getNumChildren(); ++j) {
- Node rc = m->getRepresentative(un[j]);
- Trace("model-builder-debug2") << " get rep : " << un[j] << " returned " << rc << std::endl;
- Assert( rc.isConst() );
- children.push_back(rc);
- }
- Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
- Node v = m->getRepresentative(un);
- Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")" << endl;
- ufmt.setValue(m, simp, v);
- default_v = v;
- }
- if( default_v.isNull() ){
- //choose default value from model if none exists
- TypeEnumerator te(f.getType().getRangeType());
- default_v = (*te);
- }
- ufmt.setDefaultValue( m, default_v );
- bool condenseFuncValues = options::condenseFunctionValues();
- if(condenseFuncValues) {
- ufmt.simplify();
- }
- std::stringstream ss;
- ss << "_arg_" << f << "_";
- Node val = ufmt.getFunctionValue( ss.str().c_str(), condenseFuncValues );
- m->assignFunctionDefinition( f, val );
- //ufmt.debugPrint( std::cout, m );
-}
-
-void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f) {
- Assert( options::ufHo() );
- TypeNode type = f.getType();
- std::vector< TypeNode > argTypes = type.getArgTypes();
- std::vector< Node > args;
- std::vector< TNode > apply_args;
- for( unsigned i=0; i<argTypes.size(); i++ ){
- Node v = NodeManager::currentNM()->mkBoundVar( argTypes[i] );
- args.push_back( v );
- if( i>0 ){
- apply_args.push_back( v );
- }
- }
- //start with the base return value (currently we use the same default value for all functions)
- TypeEnumerator te(type.getRangeType());
- Node curr = (*te);
- std::map< Node, std::vector< Node > >::iterator itht = m->d_ho_uf_terms.find( f );
- if( itht!=m->d_ho_uf_terms.end() ){
- for( size_t i=0; i<itht->second.size(); i++ ){
- Node hn = itht->second[i];
- Trace("model-builder-debug") << " process : " << hn << std::endl;
- Assert( hn.getKind()==kind::HO_APPLY );
- Assert( m->areEqual( hn[0], f ) );
- Node hni = m->getRepresentative(hn[1]);
- Trace("model-builder-debug2") << " get rep : " << hn[0] << " returned " << hni << std::endl;
- Assert( hni.isConst() );
- Assert( hni.getType().isSubtypeOf( args[0].getType() ) );
- hni = Rewriter::rewrite( args[0].eqNode( hni ) );
- Node hnv = m->getRepresentative(hn);
- Trace("model-builder-debug2") << " get rep val : " << hn << " returned " << hnv << std::endl;
- Assert( hnv.isConst() );
- if( !apply_args.empty() ){
- Assert( hnv.getKind()==kind::LAMBDA && hnv[0].getNumChildren()+1==args.size() );
- std::vector< TNode > largs;
- for( unsigned j=0; j<hnv[0].getNumChildren(); j++ ){
- largs.push_back( hnv[0][j] );
- }
- Assert( largs.size()==apply_args.size() );
- hnv = hnv[1].substitute( largs.begin(), largs.end(), apply_args.begin(), apply_args.end() );
- hnv = Rewriter::rewrite( hnv );
- }
- Assert( !TypeNode::leastCommonTypeNode( hnv.getType(), curr.getType() ).isNull() );
- curr = NodeManager::currentNM()->mkNode( kind::ITE, hni, hnv, curr );
- }
- }
- Node val = NodeManager::currentNM()->mkNode( kind::LAMBDA,
- NodeManager::currentNM()->mkNode( kind::BOUND_VAR_LIST, args ), curr );
- m->assignFunctionDefinition( f, val );
-}
-
-// This struct is used to sort terms by the "size" of their type
-// The size of the type is the number of nodes in the type, for example
-// size of Int is 1
-// size of Function( Int, Int ) is 3
-// size of Function( Function( Bool, Int ), Int ) is 5
-struct sortTypeSize {
- // stores the size of the type
- std::map< TypeNode, unsigned > d_type_size;
- // get the size of type tn
- unsigned getTypeSize( TypeNode tn ) {
- std::map< TypeNode, unsigned >::iterator it = d_type_size.find( tn );
- if( it!=d_type_size.end() ){
- return it->second;
- }else{
- unsigned sum = 1;
- for( unsigned i=0; i<tn.getNumChildren(); i++ ){
- sum += getTypeSize( tn[i] );
- }
- d_type_size[tn] = sum;
- return sum;
- }
- }
-public:
- // compares the type size of i and j
- // returns true iff the size of i is less than that of j
- // tiebreaks are determined by node value
- bool operator() (Node i, Node j) {
- int si = getTypeSize( i.getType() );
- int sj = getTypeSize( j.getType() );
- if( si<sj ){
- return true;
- }else if( si==sj ){
- return i<j;
- }else{
- return false;
- }
- }
-};
-
-void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m) {
- Trace("model-builder") << "Assigning function values..." << std::endl;
- std::vector< Node > funcs_to_assign = m->getFunctionsToAssign();
-
- if( options::ufHo() ){
- // sort based on type size if higher-order
- Trace("model-builder") << "Sort functions by type..." << std::endl;
- sortTypeSize sts;
- std::sort( funcs_to_assign.begin(), funcs_to_assign.end(), sts );
- }
-
- if( Trace.isOn("model-builder") ){
- Trace("model-builder") << "...have " << funcs_to_assign.size() << " functions to assign:" << std::endl;
- for( unsigned k=0; k<funcs_to_assign.size(); k++ ){
- Node f = funcs_to_assign[k];
- Trace("model-builder") << " [" << k << "] : " << f << " : " << f.getType() << std::endl;
- }
- }
-
- // construct function values
- for( unsigned k=0; k<funcs_to_assign.size(); k++ ){
- Node f = funcs_to_assign[k];
- Trace("model-builder") << " Function #" << k << " is " << f << std::endl;
- //std::map< Node, std::vector< Node > >::iterator itht = m->d_ho_uf_terms.find( f );
- if( !options::ufHo() ){
- Trace("model-builder") << " Assign function value for " << f << " based on APPLY_UF" << std::endl;
- assignFunction( m, f );
- }else{
- Trace("model-builder") << " Assign function value for " << f << " based on curried HO_APPLY" << std::endl;
- assignHoFunction( m, f );
- }
- }
- Trace("model-builder") << "Finished assigning function values." << std::endl;
-}
-
} /* namespace CVC4::theory */
} /* namespace CVC4 */
#include <unordered_set>
#include "smt/model.h"
-#include "theory/uf/equality_engine.h"
#include "theory/rep_set.h"
#include "theory/substitutions.h"
#include "theory/type_enumerator.h"
+#include "theory/type_set.h"
+#include "theory/uf/equality_engine.h"
namespace CVC4 {
namespace theory {
-/**
- * Theory Model class.
- * For Model m, should call m.initialize() before using.
+/** Theory Model class.
+ *
+ * This class represents a model produced by the TheoryEngine.
+ * The data structures used to represent a model are:
+ * (1) d_equalityEngine : an equality engine object, which stores
+ * an equivalence relation over all terms that exist in
+ * the current set of assertions.
+ * (2) d_substitutions : a substitution map storing cases of
+ * explicitly solved terms, for instance during preprocessing.
+ * (3) d_reps : a map from equivalence class representatives of
+ * the equality engine to the (constant) representatives
+ * assigned to that equivalence class.
+ * (4) d_uf_models : a map from uninterpreted functions to their
+ * lambda representation.
+ * (5) d_rep_set : a data structure that allows interpretations
+ * for types to be represented as terms. This is useful for
+ * finite model finding.
+ *
+ * These data structures are built after a full effort check with
+ * no lemmas sent, within a call to:
+ * TheoryEngineModelBuilder::buildModel(...)
+ * which includes subcalls to TheoryX::collectModelInfo(...) calls.
+ *
+ * These calls may modify the model object using the interface
+ * functions below, including:
+ * - assertEquality, assertPredicate, assertRepresentative,
+ * assertEqualityEngine.
+ * - assignFunctionDefinition
+ *
+ * During and after this building process, these calls may use
+ * interface functions below to guide the model construction:
+ * - hasTerm, getRepresentative, areEqual, areDisequal
+ * - getEqualityEngine
+ * - getRepSet
+ * - hasAssignedFunctionDefinition, getFunctionsToAssign
+ *
+ * After this building process, the function getValue can be
+ * used to query the value of nodes.
*/
class TheoryModel : public Model
{
friend class TheoryEngineModelBuilder;
-
public:
TheoryModel(context::Context* c, std::string name, bool enableFuncModels);
virtual ~TheoryModel() throw();
- /** get comments */
- void getComments(std::ostream& out) const;
- /** is built */
- bool isBuilt() { return d_modelBuilt; }
- /** set need build */
- void setNeedsBuild() { d_modelBuilt = false; }
- /**
- * Get value function. This should be called only after a ModelBuilder has called buildModel(...)
- * on this model.
+ /** reset the model */
+ virtual void reset();
+ /** is built
+ *
+ * Have we (attempted to) build this model since the last
+ * call to reset? Notice for model building techniques
+ * that are not guaranteed to succeed (such as
+ * when quantified formulas are enabled), a true return
+ * value does not imply that this is a model of the
+ * current assertions.
*/
- Node getValue( TNode n, bool useDontCares = false ) const;
-
- //---------------------------- separation logic
- /** set the heap and value sep.nil is equal to */
- void setHeapModel(Node h, Node neq);
- /** get the heap and value sep.nil is equal to */
- bool getHeapModel(Expr& h, Expr& neq) const;
- //---------------------------- end separation logic
-
+ bool isBuilt() { return d_modelBuilt; }
+ //---------------------------- for building the model
/** Adds a substitution from x to t. */
void addSubstitution(TNode x, TNode t, bool invalidateCache = true);
- /** add term function
- * addTerm( n ) will do any model-specific processing necessary for n,
- * such as constraining the interpretation of uninterpreted functions,
- * and adding n to the equality engine of this model
+ /** add term
+ * This will do any model-specific processing necessary for n,
+ * such as constraining the interpretation of uninterpreted functions,
+ * and adding n to the equality engine of this model.
*/
virtual void addTerm(TNode n);
/** assert equality holds in the model */
* functions.
*/
void assertRepresentative(TNode n);
+ //---------------------------- end building the model
// ------------------- general equality queries
/** does the equality engine of this model have term a? */
eq::EqualityEngine* getEqualityEngine() { return d_equalityEngine; }
// ------------------- end general equality queries
+ /** Get value function.
+ * This should be called only after a ModelBuilder
+ * has called buildModel(...) on this model.
+ * useDontCares is whether to return Node::null() if
+ * n does not occur in the equality engine.
+ */
+ Node getValue(TNode n, bool useDontCares = false) const;
+ /** get comments */
+ void getComments(std::ostream& out) const;
+
+ //---------------------------- separation logic
+ /** set the heap and value sep.nil is equal to */
+ void setHeapModel(Node h, Node neq);
+ /** get the heap and value sep.nil is equal to */
+ bool getHeapModel(Expr& h, Expr& neq) const;
+ //---------------------------- end separation logic
+
/** get the representative set object */
const RepSet* getRepSet() const { return &d_rep_set; }
/** get the representative set object (FIXME: remove this, see #1199) */
/** true/false nodes */
Node d_true;
Node d_false;
- mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
/** comment stream to include in printing */
std::stringstream d_comment_str;
- /** reset the model */
- virtual void reset();
- /**
- * Get model value function. This function is called by getValue
+ /** Get model value function.
+ *
+ * This function is a helper function for getValue.
+ * hasBoundVars is whether n may contain bound variables
+ * useDontCares is whether to return Node::null() if
+ * n does not occur in the equality engine.
*/
Node getModelValue(TNode n,
bool hasBoundVars = false,
bool useDontCares = false) const;
private:
+ /** cache for getModelValue */
+ mutable std::unordered_map<Node, Node, NodeHashFunction> d_modelCache;
+
//---------------------------- separation logic
/** the value of the heap */
Node d_sep_heap;
bool d_enableFuncModels;
/** map from function terms to the (lambda) definitions
* After the model is built, the domain of this map is all terms of function
- * type
- * that appear as terms in d_equalityEngine.
+ * type that appear as terms in d_equalityEngine.
*/
std::map<Node, Node> d_uf_models;
//---------------------------- end function values
};/* class TheoryModel */
-/*
- * Class that encapsulates a map from types to sets of nodes
- */
-class TypeSet {
-public:
- typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction> TypeSetMap;
- typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction> TypeToTypeEnumMap;
- typedef TypeSetMap::iterator iterator;
- typedef TypeSetMap::const_iterator const_iterator;
-private:
- TypeSetMap d_typeSet;
- TypeToTypeEnumMap d_teMap;
- TypeEnumeratorProperties * d_tep;
-
- /* Note that recursive traversal here is over enumerated expressions
- * (very low expression depth). */
- void addSubTerms(TNode n, std::map< TNode, bool >& visited, bool topLevel=true){
- if( visited.find( n )==visited.end() ){
- visited[n] = true;
- if( !topLevel ){
- add(n.getType(), n);
- }
- for( unsigned i=0; i<n.getNumChildren(); i++ ){
- addSubTerms( n[i], visited, false );
- }
- }
- }
-public:
- TypeSet() : d_tep(NULL) {}
- ~TypeSet() {
- iterator it;
- for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it) {
- if ((*it).second != NULL) {
- delete (*it).second;
- }
- }
- TypeToTypeEnumMap::iterator it2;
- for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2) {
- if ((*it2).second != NULL) {
- delete (*it2).second;
- }
- }
- }
- void setTypeEnumeratorProperties( TypeEnumeratorProperties * tep ) { d_tep = tep; }
- void add(TypeNode t, TNode n)
- {
- iterator it = d_typeSet.find(t);
- std::set<Node>* s;
- if (it == d_typeSet.end()) {
- s = new std::set<Node>;
- d_typeSet[t] = s;
- }
- else {
- s = (*it).second;
- }
- s->insert(n);
- }
-
- std::set<Node>* getSet(TypeNode t) const
- {
- const_iterator it = d_typeSet.find(t);
- if (it == d_typeSet.end()) {
- return NULL;
- }
- return (*it).second;
- }
-
- Node nextTypeEnum(TypeNode t, bool useBaseType = false)
- {
- TypeEnumerator* te;
- TypeToTypeEnumMap::iterator it = d_teMap.find(t);
- if (it == d_teMap.end()) {
- te = new TypeEnumerator(t, d_tep);
- d_teMap[t] = te;
- }
- else {
- te = (*it).second;
- }
- if (te->isFinished()) {
- return Node();
- }
-
- if (useBaseType) {
- t = t.getBaseType();
- }
- iterator itSet = d_typeSet.find(t);
- std::set<Node>* s;
- if (itSet == d_typeSet.end()) {
- s = new std::set<Node>;
- d_typeSet[t] = s;
- }
- else {
- s = (*itSet).second;
- }
- Node n = **te;
- while (s->find(n) != s->end()) {
- ++(*te);
- if (te->isFinished()) {
- return Node();
- }
- n = **te;
- }
- s->insert(n);
- // add all subterms of n to this set as well
- // this is necessary for parametric types whose values are constructed from other types
- // to ensure that we do not enumerate subterms of other previous enumerated values
- std::map< TNode, bool > visited;
- addSubTerms(n, visited);
- ++(*te);
- return n;
- }
-
- bool empty()
- {
- return d_typeSet.empty();
- }
-
- iterator begin()
- {
- return d_typeSet.begin();
- }
-
- iterator end()
- {
- return d_typeSet.end();
- }
-
- static TypeNode getType(iterator it)
- {
- return (*it).first;
- }
-
- static std::set<Node>& getSet(iterator it)
- {
- return *(*it).second;
- }
-
-};/* class TypeSet */
-
-/** TheoryEngineModelBuilder class
- * This model builder will consult all theories in a theory engine for
- * collectModelInfo( ... ) when building a model.
- */
-class TheoryEngineModelBuilder : public ModelBuilder
-{
-protected:
- /** pointer to theory engine */
- TheoryEngine* d_te;
- typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
- NodeMap d_normalizedCache;
- typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
- std::map< Node, Node > d_constantReps;
-
- /** process build model */
- virtual bool preProcessBuildModel(TheoryModel* m);
- virtual bool processBuildModel(TheoryModel* m);
- virtual void debugModel( TheoryModel* m ) {}
- /** normalize representative */
- Node normalize(TheoryModel* m, TNode r, bool evalOnly);
- bool isAssignable(TNode n);
- void checkTerms(TNode n, TheoryModel* tm, NodeSet& cache);
- void assignConstantRep( TheoryModel* tm, Node eqc, Node const_rep );
- void addToTypeList( TypeNode tn, std::vector< TypeNode >& type_list, std::map< TypeNode, bool >& visiting );
- /** is v an excluded codatatype value */
- bool isExcludedCdtValue( Node v, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc );
- bool isCdtValueMatch( Node v, Node r, Node eqc, Node& eqc_m );
- /** involves usort */
- bool involvesUSort( TypeNode tn );
- bool isExcludedUSortValue( std::map< TypeNode, unsigned >& eqc_usort_count, Node v, std::map< Node, bool >& visited );
-protected:
- /** assign function f based on the model m.
- * This construction is based on "table form". For example:
- * (f 0 1) = 1
- * (f 0 2) = 2
- * (f 1 1) = 3
- * ...
- * becomes:
- * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
- * (ite (and (= x 0) (= y 2)) 2
- * (ite (and (= x 1) (= y 1)) 3 ...)))
- */
- void assignFunction(TheoryModel* m, Node f);
- /** assign function f based on the model m.
- * This construction is based on "dag form". For example:
- * (f 0 1) = 1
- * (f 0 2) = 2
- * (f 1 1) = 3
- * ...
- * becomes:
- * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
- * (ite (= y 2) 2 ...))
- * (ite (= x 1) (ite (= y 1) 3 ...)
- * ...))
- *
- * where the above is represented as a directed acyclic graph (dag).
- * This construction is accomplished by assigning values to (f c)
- * terms before f, e.g.
- * (f 0) = (lambda y. (ite (= y 1) 1
- * (ite (= y 2) 2 ...))
- * (f 1) = (lambda y. (ite (= y 1) 3 ...))
- * where
- * f = (lambda xy. (ite (= x 0) ((f 0) y)
- * (ite (= x 1) ((f 1) y) ...))
- */
- void assignHoFunction(TheoryModel* m, Node f);
- /** Assign all unassigned functions in the model m (those returned by TheoryModel::getFunctionsToAssign),
- * using the two functions above. Currently:
- * If ufHo is disabled, we call assignFunction for all functions.
- * If ufHo is enabled, we call assignHoFunction.
- */
- void assignFunctions(TheoryModel* m);
-public:
- TheoryEngineModelBuilder(TheoryEngine* te);
- virtual ~TheoryEngineModelBuilder(){}
- /** Build model function.
- * Should be called only on TheoryModels m
- */
- bool buildModel(Model* m);
- void debugCheckModel(Model* m);
-};/* class TheoryEngineModelBuilder */
-
}/* CVC4::theory namespace */
}/* CVC4 namespace */
--- /dev/null
+/********************* */
+/*! \file theory_model_builder.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Clark Barrett, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of theory model buidler class
+ **/
+#include "theory/theory_model_builder.h"
+
+#include "options/quantifiers_options.h"
+#include "options/smt_options.h"
+#include "options/uf_options.h"
+#include "theory/theory_engine.h"
+#include "theory/uf/theory_uf_model.h"
+
+using namespace std;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+
+namespace CVC4 {
+namespace theory {
+
+TheoryEngineModelBuilder::TheoryEngineModelBuilder(TheoryEngine* te) : d_te(te)
+{
+}
+
+bool TheoryEngineModelBuilder::isAssignable(TNode n)
+{
+ if (n.getKind() == kind::SELECT || n.getKind() == kind::APPLY_SELECTOR_TOTAL)
+ {
+ // selectors are always assignable (where we guarantee that they are not
+ // evaluatable here)
+ if (!options::ufHo())
+ {
+ Assert(!n.getType().isFunction());
+ return true;
+ }
+ else
+ {
+ // might be a function field
+ return !n.getType().isFunction();
+ }
+ }
+ else
+ {
+ // non-function variables, and fully applied functions
+ if (!options::ufHo())
+ {
+ // no functions exist, all functions are fully applied
+ Assert(n.getKind() != kind::HO_APPLY);
+ Assert(!n.getType().isFunction());
+ return n.isVar() || n.getKind() == kind::APPLY_UF;
+ }
+ else
+ {
+ // Assert( n.getKind() != kind::APPLY_UF );
+ return (n.isVar() && !n.getType().isFunction())
+ || n.getKind() == kind::APPLY_UF
+ || (n.getKind() == kind::HO_APPLY
+ && n[0].getType().getNumChildren() == 2);
+ }
+ }
+}
+
+void TheoryEngineModelBuilder::addAssignableSubterms(TNode n,
+ TheoryModel* tm,
+ NodeSet& cache)
+{
+ if (n.getKind() == FORALL || n.getKind() == EXISTS)
+ {
+ return;
+ }
+ if (cache.find(n) != cache.end())
+ {
+ return;
+ }
+ if (isAssignable(n))
+ {
+ tm->d_equalityEngine->addTerm(n);
+ }
+ for (TNode::iterator child_it = n.begin(); child_it != n.end(); ++child_it)
+ {
+ addAssignableSubterms(*child_it, tm, cache);
+ }
+ cache.insert(n);
+}
+
+void TheoryEngineModelBuilder::assignConstantRep(TheoryModel* tm,
+ Node eqc,
+ Node const_rep)
+{
+ d_constantReps[eqc] = const_rep;
+ Trace("model-builder") << " Assign: Setting constant rep of " << eqc
+ << " to " << const_rep << endl;
+ tm->d_rep_set.setTermForRepresentative(const_rep, eqc);
+}
+
+bool TheoryEngineModelBuilder::isExcludedCdtValue(
+ Node val,
+ std::set<Node>* repSet,
+ std::map<Node, Node>& assertedReps,
+ Node eqc)
+{
+ Trace("model-builder-debug")
+ << "Is " << val << " and excluded codatatype value for " << eqc << "? "
+ << std::endl;
+ for (set<Node>::iterator i = repSet->begin(); i != repSet->end(); ++i)
+ {
+ Assert(assertedReps.find(*i) != assertedReps.end());
+ Node rep = assertedReps[*i];
+ Trace("model-builder-debug") << " Rep : " << rep << std::endl;
+ // check matching val to rep with eqc as a free variable
+ Node eqc_m;
+ if (isCdtValueMatch(val, rep, eqc, eqc_m))
+ {
+ Trace("model-builder-debug") << " ...matches with " << eqc << " -> "
+ << eqc_m << std::endl;
+ if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT)
+ {
+ Trace("model-builder-debug") << "*** " << val
+ << " is excluded datatype for " << eqc
+ << std::endl;
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+bool TheoryEngineModelBuilder::isCdtValueMatch(Node v,
+ Node r,
+ Node eqc,
+ Node& eqc_m)
+{
+ if (r == v)
+ {
+ return true;
+ }
+ else if (r == eqc)
+ {
+ if (eqc_m.isNull())
+ {
+ // only if an uninterpreted constant?
+ eqc_m = v;
+ return true;
+ }
+ else
+ {
+ return v == eqc_m;
+ }
+ }
+ else if (v.getKind() == kind::APPLY_CONSTRUCTOR
+ && r.getKind() == kind::APPLY_CONSTRUCTOR)
+ {
+ if (v.getOperator() == r.getOperator())
+ {
+ for (unsigned i = 0; i < v.getNumChildren(); i++)
+ {
+ if (!isCdtValueMatch(v[i], r[i], eqc, eqc_m))
+ {
+ return false;
+ }
+ }
+ return true;
+ }
+ }
+ return false;
+}
+
+bool TheoryEngineModelBuilder::involvesUSort(TypeNode tn)
+{
+ if (tn.isSort())
+ {
+ return true;
+ }
+ else if (tn.isArray())
+ {
+ return involvesUSort(tn.getArrayIndexType())
+ || involvesUSort(tn.getArrayConstituentType());
+ }
+ else if (tn.isSet())
+ {
+ return involvesUSort(tn.getSetElementType());
+ }
+ else if (tn.isDatatype())
+ {
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ return dt.involvesUninterpretedType();
+ }
+ else
+ {
+ return false;
+ }
+}
+
+bool TheoryEngineModelBuilder::isExcludedUSortValue(
+ std::map<TypeNode, unsigned>& eqc_usort_count,
+ Node v,
+ std::map<Node, bool>& visited)
+{
+ Assert(v.isConst());
+ if (visited.find(v) == visited.end())
+ {
+ visited[v] = true;
+ TypeNode tn = v.getType();
+ if (tn.isSort())
+ {
+ Trace("model-builder-debug") << "Is excluded usort value : " << v << " "
+ << tn << std::endl;
+ unsigned card = eqc_usort_count[tn];
+ Trace("model-builder-debug") << " Cardinality is " << card << std::endl;
+ unsigned index =
+ v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt();
+ Trace("model-builder-debug") << " Index is " << index << std::endl;
+ return index > 0 && index >= card;
+ }
+ for (unsigned i = 0; i < v.getNumChildren(); i++)
+ {
+ if (isExcludedUSortValue(eqc_usort_count, v[i], visited))
+ {
+ return true;
+ }
+ }
+ }
+ return false;
+}
+
+void TheoryEngineModelBuilder::addToTypeList(
+ TypeNode tn,
+ std::vector<TypeNode>& type_list,
+ std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting)
+{
+ if (std::find(type_list.begin(), type_list.end(), tn) == type_list.end())
+ {
+ if (visiting.find(tn) == visiting.end())
+ {
+ visiting.insert(tn);
+ /* This must make a recursive call on all types that are subterms of
+ * values of the current type.
+ * Note that recursive traversal here is over enumerated expressions
+ * (very low expression depth). */
+ if (tn.isArray())
+ {
+ addToTypeList(tn.getArrayIndexType(), type_list, visiting);
+ addToTypeList(tn.getArrayConstituentType(), type_list, visiting);
+ }
+ else if (tn.isSet())
+ {
+ addToTypeList(tn.getSetElementType(), type_list, visiting);
+ }
+ else if (tn.isDatatype())
+ {
+ const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype();
+ for (unsigned i = 0; i < dt.getNumConstructors(); i++)
+ {
+ for (unsigned j = 0; j < dt[i].getNumArgs(); j++)
+ {
+ TypeNode ctn = TypeNode::fromType(dt[i][j].getRangeType());
+ addToTypeList(ctn, type_list, visiting);
+ }
+ }
+ }
+ Assert(std::find(type_list.begin(), type_list.end(), tn)
+ == type_list.end());
+ type_list.push_back(tn);
+ }
+ }
+}
+
+bool TheoryEngineModelBuilder::buildModel(Model* m)
+{
+ Trace("model-builder") << "TheoryEngineModelBuilder: buildModel" << std::endl;
+ TheoryModel* tm = (TheoryModel*)m;
+
+ // buildModel should only be called once per check
+ Assert(!tm->isBuilt());
+
+ // Reset model
+ tm->reset();
+
+ // mark as built
+ tm->d_modelBuilt = true;
+
+ // Collect model info from the theories
+ Trace("model-builder") << "TheoryEngineModelBuilder: Collect model info..."
+ << std::endl;
+ d_te->collectModelInfo(tm);
+
+ // model-builder specific initialization
+ if (!preProcessBuildModel(tm))
+ {
+ return false;
+ }
+
+ // Loop through all terms and make sure that assignable sub-terms are in the
+ // 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);
+ {
+ NodeSet cache;
+ for (; !eqcs_i.isFinished(); ++eqcs_i)
+ {
+ eq::EqClassIterator eqc_i =
+ eq::EqClassIterator((*eqcs_i), tm->d_equalityEngine);
+ for (; !eqc_i.isFinished(); ++eqc_i)
+ {
+ addAssignableSubterms(*eqc_i, tm, cache);
+ }
+ TypeNode tn = (*eqcs_i).getType();
+ if (tn.isSort())
+ {
+ if (eqc_usort_count.find(tn) == eqc_usort_count.end())
+ {
+ eqc_usort_count[tn] = 1;
+ }
+ else
+ {
+ eqc_usort_count[tn]++;
+ }
+ }
+ }
+ }
+
+ Trace("model-builder") << "Collect representatives..." << std::endl;
+
+ // Process all terms in the equality engine, store representatives for each EC
+ d_constantReps.clear();
+ std::map<Node, Node> assertedReps;
+ TypeSet typeConstSet, typeRepSet, typeNoRepSet;
+ TypeEnumeratorProperties tep;
+ if (options::finiteModelFind())
+ {
+ tep.d_fixed_usort_card = true;
+ for (std::map<TypeNode, unsigned>::iterator it = eqc_usort_count.begin();
+ it != eqc_usort_count.end();
+ ++it)
+ {
+ Trace("model-builder") << "Fixed bound (#eqc) for " << it->first << " : "
+ << it->second << std::endl;
+ tep.d_fixed_card[it->first] = Integer(it->second);
+ }
+ 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 +
+ // parametric types
+ // instantiated with uninterpreted sorts, but is probably a good idea to do
+ // in general
+ // since it leads to models with smaller term sizes.
+ std::vector<TypeNode> type_list;
+ eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+ for (; !eqcs_i.isFinished(); ++eqcs_i)
+ {
+ // eqc is the equivalence class representative
+ Node eqc = (*eqcs_i);
+ Trace("model-builder") << "Processing EC: " << eqc << endl;
+ Assert(tm->d_equalityEngine->getRepresentative(eqc) == eqc);
+ TypeNode eqct = eqc.getType();
+ Assert(assertedReps.find(eqc) == assertedReps.end());
+ Assert(d_constantReps.find(eqc) == d_constantReps.end());
+
+ // Loop through terms in this EC
+ Node rep, const_rep;
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+ for (; !eqc_i.isFinished(); ++eqc_i)
+ {
+ Node n = *eqc_i;
+ Trace("model-builder") << " Processing Term: " << n << endl;
+ // Record as rep if this node was specified as a representative
+ if (tm->d_reps.find(n) != tm->d_reps.end())
+ {
+ // AJR: I believe this assertion is too strict,
+ // e.g. datatypes may assert representative for two constructor terms
+ // that are not in the care graph and are merged during
+ // collectModelInfo.
+ // Assert(rep.isNull());
+ rep = tm->d_reps[n];
+ Assert(!rep.isNull());
+ Trace("model-builder") << " Rep( " << eqc << " ) = " << rep
+ << std::endl;
+ }
+ // Record as const_rep if this node is constant
+ if (n.isConst())
+ {
+ Assert(const_rep.isNull());
+ const_rep = n;
+ Trace("model-builder") << " ConstRep( " << eqc << " ) = " << const_rep
+ << std::endl;
+ }
+ // model-specific processing of the term
+ tm->addTerm(n);
+ }
+
+ // Assign representative for this EC
+ if (!const_rep.isNull())
+ {
+ // Theories should not specify a rep if there is already a constant in the
+ // EC
+ // AJR: I believe this assertion is too strict, eqc with asserted reps may
+ // merge with constant eqc
+ // Assert(rep.isNull() || rep == const_rep);
+ assignConstantRep(tm, eqc, const_rep);
+ typeConstSet.add(eqct.getBaseType(), const_rep);
+ }
+ else if (!rep.isNull())
+ {
+ assertedReps[eqc] = rep;
+ typeRepSet.add(eqct.getBaseType(), eqc);
+ std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
+ addToTypeList(eqct.getBaseType(), type_list, visiting);
+ }
+ else
+ {
+ typeNoRepSet.add(eqct, eqc);
+ std::unordered_set<TypeNode, TypeNodeHashFunction> visiting;
+ addToTypeList(eqct, type_list, visiting);
+ }
+ }
+
+ // Need to ensure that each EC has a constant representative.
+
+ Trace("model-builder") << "Processing EC's..." << std::endl;
+
+ TypeSet::iterator it;
+ vector<TypeNode>::iterator type_it;
+ set<Node>::iterator i, i2;
+ bool changed, unassignedAssignable, assignOne = false;
+ set<TypeNode> evaluableSet;
+
+ // Double-fixed-point loop
+ // Outer loop handles a special corner case (see code at end of loop for
+ // details)
+ for (;;)
+ {
+ // Inner fixed-point loop: we are trying to learn constant values for every
+ // EC. Each time through this loop, we process all of the
+ // types by type and may learn some new EC values. EC's in one type may
+ // depend on EC's in another type, so we need a fixed-point loop
+ // to ensure that we learn as many EC values as possible
+ do
+ {
+ changed = false;
+ unassignedAssignable = false;
+ evaluableSet.clear();
+
+ // Iterate over all types we've seen
+ for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
+ {
+ TypeNode t = *type_it;
+ TypeNode tb = t.getBaseType();
+ set<Node>* noRepSet = typeNoRepSet.getSet(t);
+
+ // 1. Try to evaluate the EC's in this type
+ if (noRepSet != NULL && !noRepSet->empty())
+ {
+ Trace("model-builder") << " Eval phase, working on type: " << t
+ << endl;
+ bool assignable, evaluable, evaluated;
+ 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 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;
+ }
+ }
+ }
+ if (!evaluated)
+ {
+ if (evaluable)
+ {
+ evaluableSet.insert(tb);
+ }
+ if (assignable)
+ {
+ unassignedAssignable = true;
+ }
+ }
+ }
+ }
+
+ // 2. Normalize any non-const representative terms for this type
+ set<Node>* repSet = typeRepSet.getSet(t);
+ if (repSet != NULL && !repSet->empty())
+ {
+ Trace("model-builder")
+ << " Normalization phase, working on type: " << t << endl;
+ d_normalizedCache.clear();
+ for (i = repSet->begin(); i != repSet->end();)
+ {
+ Assert(assertedReps.find(*i) != assertedReps.end());
+ Node rep = assertedReps[*i];
+ Node normalized = normalize(tm, rep, false);
+ Trace("model-builder") << " Normalizing rep (" << rep
+ << "), normalized to (" << normalized << ")"
+ << endl;
+ if (normalized.isConst())
+ {
+ changed = true;
+ typeConstSet.add(tb, normalized);
+ assignConstantRep(tm, *i, normalized);
+ assertedReps.erase(*i);
+ i2 = i;
+ ++i;
+ repSet->erase(i2);
+ }
+ else
+ {
+ if (normalized != rep)
+ {
+ assertedReps[*i] = normalized;
+ changed = true;
+ }
+ ++i;
+ }
+ }
+ }
+ }
+ } while (changed);
+
+ if (!unassignedAssignable)
+ {
+ break;
+ }
+
+ // 3. Assign unassigned assignable EC's using type enumeration - assign a
+ // value *different* from all other EC's if the type is infinite
+ // Assign first value from type enumerator otherwise - for finite types, we
+ // rely on polite framework to ensure that EC's that have to be
+ // different are different.
+
+ // Only make assignments on a type if:
+ // 1. there are no terms that share the same base type with un-normalized
+ // representatives
+ // 2. there are no terms that share teh same base type that are unevaluated
+ // evaluable terms
+ // Alternatively, if 2 or 3 don't hold but we are in a special
+ // deadlock-breaking mode where assignOne is true, go ahead and make one
+ // assignment
+ changed = false;
+ // must iterate over the ordered type list to ensure that we do not
+ // enumerate values with subterms
+ // having types that we are currently enumerating (when possible)
+ // for example, this ensures we enumerate uninterpreted sort U before (List
+ // of U) and (Array U U)
+ // however, it does not break cyclic type dependencies for mutually
+ // recursive datatypes, but this is handled
+ // by recording all subterms of enumerated values in TypeSet::addSubTerms.
+ for (type_it = type_list.begin(); type_it != type_list.end(); ++type_it)
+ {
+ TypeNode t = *type_it;
+ // continue if there are no more equivalence classes of this type to
+ // assign
+ std::set<Node>* noRepSetPtr = typeNoRepSet.getSet(t);
+ if (noRepSetPtr == NULL)
+ {
+ continue;
+ }
+ set<Node>& noRepSet = *noRepSetPtr;
+ if (noRepSet.empty())
+ {
+ continue;
+ }
+
+ // get properties of this type
+ bool isCorecursive = false;
+ if (t.isDatatype())
+ {
+ const Datatype& dt = ((DatatypeType)(t).toType()).getDatatype();
+ isCorecursive =
+ dt.isCodatatype() && (!dt.isFinite(t.toType())
+ || dt.isRecursiveSingleton(t.toType()));
+ }
+#ifdef CVC4_ASSERTIONS
+ bool isUSortFiniteRestricted = false;
+ if (options::finiteModelFind())
+ {
+ isUSortFiniteRestricted = !t.isSort() && involvesUSort(t);
+ }
+#endif
+
+ set<Node>* repSet = typeRepSet.getSet(t);
+ TypeNode tb = t.getBaseType();
+ if (!assignOne)
+ {
+ set<Node>* repSet = typeRepSet.getSet(tb);
+ if (repSet != NULL && !repSet->empty())
+ {
+ continue;
+ }
+ if (evaluableSet.find(tb) != evaluableSet.end())
+ {
+ continue;
+ }
+ }
+ Trace("model-builder") << " Assign phase, working on type: " << t
+ << endl;
+ bool assignable, evaluable CVC4_UNUSED;
+ 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)
+ {
+ Node n = *eqc_i;
+ if (isAssignable(n))
+ {
+ assignable = true;
+ }
+ else
+ {
+ evaluable = true;
+ }
+ }
+ Trace("model-builder-debug")
+ << " eqc " << *i2 << " is assignable=" << assignable
+ << ", evaluable=" << evaluable << std::endl;
+ if (assignable)
+ {
+ Assert(!evaluable || assignOne);
+ Assert(!t.isBoolean() || (*i2).getKind() == kind::APPLY_UF);
+ Node n;
+ if (t.getCardinality().isInfinite())
+ {
+ // if (!t.isInterpretedFinite()) {
+ bool success;
+ do
+ {
+ Trace("model-builder-debug") << "Enumerate term of type " << t
+ << std::endl;
+ n = typeConstSet.nextTypeEnum(t, true);
+ //--- AJR: this code checks whether n is a legal value
+ Assert(!n.isNull());
+ success = true;
+ Trace("model-builder-debug") << "Check if excluded : " << n
+ << std::endl;
+#ifdef CVC4_ASSERTIONS
+ if (isUSortFiniteRestricted)
+ {
+ // must not involve uninterpreted constants beyond cardinality
+ // bound (which assumed to coincide with #eqc)
+ // this is just an assertion now, since TypeEnumeratorProperties
+ // should ensure that only legal values are enumerated wrt this
+ // constraint.
+ std::map<Node, bool> visited;
+ success = !isExcludedUSortValue(eqc_usort_count, n, visited);
+ if (!success)
+ {
+ Trace("model-builder")
+ << "Excluded value for " << t << " : " << n
+ << " due to out of range uninterpreted constant."
+ << std::endl;
+ }
+ Assert(success);
+ }
+#endif
+ if (success && isCorecursive)
+ {
+ if (repSet != NULL && !repSet->empty())
+ {
+ // in the case of codatatypes, check if it is in the set of
+ // values that we cannot assign
+ success = !isExcludedCdtValue(n, repSet, assertedReps, *i2);
+ if (!success)
+ {
+ Trace("model-builder")
+ << "Excluded value : " << n
+ << " due to alpha-equivalent codatatype expression."
+ << std::endl;
+ }
+ }
+ }
+ //---
+ } while (!success);
+ }
+ else
+ {
+ TypeEnumerator te(t);
+ n = *te;
+ }
+ Assert(!n.isNull());
+ assignConstantRep(tm, *i2, n);
+ changed = true;
+ noRepSet.erase(i2);
+ if (assignOne)
+ {
+ assignOne = false;
+ break;
+ }
+ }
+ }
+ }
+
+ // Corner case - I'm not sure this can even happen - but it's theoretically
+ // possible to have a cyclical dependency
+ // in EC assignment/evaluation, e.g. EC1 = {a, b + 1}; EC2 = {b, a - 1}. In
+ // this case, neither one will get assigned because we are waiting
+ // to be able to evaluate. But we will never be able to evaluate because
+ // the variables that need to be assigned are in
+ // these same EC's. In this case, repeat the whole fixed-point computation
+ // with the difference that the first EC
+ // that has both assignable and evaluable expressions will get assigned.
+ if (!changed)
+ {
+ Assert(!assignOne); // check for infinite loop!
+ assignOne = true;
+ }
+ }
+
+#ifdef CVC4_ASSERTIONS
+ // Assert that all representatives have been converted to constants
+ for (it = typeRepSet.begin(); it != typeRepSet.end(); ++it)
+ {
+ set<Node>& repSet = TypeSet::getSet(it);
+ if (!repSet.empty())
+ {
+ Trace("model-builder") << "***Non-empty repSet, size = " << repSet.size()
+ << ", first = " << *(repSet.begin()) << endl;
+ Assert(false);
+ }
+ }
+#endif /* CVC4_ASSERTIONS */
+
+ Trace("model-builder") << "Copy representatives to model..." << std::endl;
+ tm->d_reps.clear();
+ std::map<Node, Node>::iterator itMap;
+ for (itMap = d_constantReps.begin(); itMap != d_constantReps.end(); ++itMap)
+ {
+ tm->d_reps[itMap->first] = itMap->second;
+ tm->d_rep_set.add(itMap->second.getType(), itMap->second);
+ }
+
+ Trace("model-builder") << "Make sure ECs have reps..." << std::endl;
+ // Make sure every EC has a rep
+ for (itMap = assertedReps.begin(); itMap != assertedReps.end(); ++itMap)
+ {
+ tm->d_reps[itMap->first] = itMap->second;
+ tm->d_rep_set.add(itMap->second.getType(), itMap->second);
+ }
+ for (it = typeNoRepSet.begin(); it != typeNoRepSet.end(); ++it)
+ {
+ set<Node>& noRepSet = TypeSet::getSet(it);
+ set<Node>::iterator i;
+ for (i = noRepSet.begin(); i != noRepSet.end(); ++i)
+ {
+ tm->d_reps[*i] = *i;
+ tm->d_rep_set.add((*i).getType(), *i);
+ }
+ }
+
+ // modelBuilder-specific initialization
+ if (!processBuildModel(tm))
+ {
+ return false;
+ }
+ else
+ {
+ return true;
+ }
+}
+
+void TheoryEngineModelBuilder::debugCheckModel(Model* m)
+{
+ TheoryModel* tm = (TheoryModel*)m;
+#ifdef CVC4_ASSERTIONS
+ Assert(tm->isBuilt());
+ eq::EqClassesIterator eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+ std::map<Node, Node>::iterator itMap;
+ // Check that every term evaluates to its representative in the model
+ for (eqcs_i = eq::EqClassesIterator(tm->d_equalityEngine);
+ !eqcs_i.isFinished();
+ ++eqcs_i)
+ {
+ // eqc is the equivalence class representative
+ Node eqc = (*eqcs_i);
+ // get the representative
+ Node rep = tm->getRepresentative(eqc);
+ if (!rep.isConst() && eqc.getType().isBoolean())
+ {
+ // if Boolean, it does not necessarily have a constant representative, use
+ // get value instead
+ rep = tm->getValue(eqc);
+ Assert(rep.isConst());
+ }
+ eq::EqClassIterator eqc_i = eq::EqClassIterator(eqc, tm->d_equalityEngine);
+ for (; !eqc_i.isFinished(); ++eqc_i)
+ {
+ Node n = *eqc_i;
+ static int repCheckInstance = 0;
+ ++repCheckInstance;
+
+ // non-linear mult is not necessarily accurate wrt getValue
+ if (n.getKind() != kind::NONLINEAR_MULT)
+ {
+ Debug("check-model::rep-checking") << "( " << repCheckInstance << ") "
+ << "n: " << n << endl
+ << "getValue(n): " << tm->getValue(n)
+ << endl
+ << "rep: " << rep << endl;
+ Assert(tm->getValue(*eqc_i) == rep,
+ "run with -d check-model::rep-checking for details");
+ }
+ }
+ }
+#endif /* CVC4_ASSERTIONS */
+
+ // builder-specific debugging
+ debugModel(tm);
+}
+
+Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly)
+{
+ std::map<Node, Node>::iterator itMap = d_constantReps.find(r);
+ if (itMap != d_constantReps.end())
+ {
+ return (*itMap).second;
+ }
+ NodeMap::iterator it = d_normalizedCache.find(r);
+ if (it != d_normalizedCache.end())
+ {
+ return (*it).second;
+ }
+ Trace("model-builder-debug") << "do normalize on " << r << std::endl;
+ Node retNode = r;
+ if (r.getNumChildren() > 0)
+ {
+ std::vector<Node> children;
+ if (r.getMetaKind() == kind::metakind::PARAMETERIZED)
+ {
+ children.push_back(r.getOperator());
+ }
+ bool childrenConst = true;
+ for (size_t i = 0; i < r.getNumChildren(); ++i)
+ {
+ Node ri = r[i];
+ bool recurse = true;
+ if (!ri.isConst())
+ {
+ if (m->d_equalityEngine->hasTerm(ri))
+ {
+ itMap =
+ d_constantReps.find(m->d_equalityEngine->getRepresentative(ri));
+ if (itMap != d_constantReps.end())
+ {
+ ri = (*itMap).second;
+ recurse = false;
+ }
+ else if (!evalOnly)
+ {
+ recurse = false;
+ }
+ }
+ if (recurse)
+ {
+ ri = normalize(m, ri, evalOnly);
+ }
+ if (!ri.isConst())
+ {
+ childrenConst = false;
+ }
+ }
+ children.push_back(ri);
+ }
+ retNode = NodeManager::currentNM()->mkNode(r.getKind(), children);
+ if (childrenConst)
+ {
+ retNode = Rewriter::rewrite(retNode);
+ Assert(retNode.getKind() == kind::APPLY_UF
+ || !retNode.getType().isFirstClass()
+ || retNode.isConst());
+ }
+ }
+ d_normalizedCache[r] = retNode;
+ return retNode;
+}
+
+bool TheoryEngineModelBuilder::preProcessBuildModel(TheoryModel* m)
+{
+ return true;
+}
+
+bool TheoryEngineModelBuilder::processBuildModel(TheoryModel* m)
+{
+ assignFunctions(m);
+ return true;
+}
+
+void TheoryEngineModelBuilder::assignFunction(TheoryModel* m, Node f)
+{
+ Assert(!options::ufHo());
+ uf::UfModelTree ufmt(f);
+ Node default_v;
+ for (size_t i = 0; i < m->d_uf_terms[f].size(); i++)
+ {
+ Node un = m->d_uf_terms[f][i];
+ vector<TNode> children;
+ children.push_back(f);
+ Trace("model-builder-debug") << " process term : " << un << std::endl;
+ for (size_t j = 0; j < un.getNumChildren(); ++j)
+ {
+ Node rc = m->getRepresentative(un[j]);
+ Trace("model-builder-debug2") << " get rep : " << un[j] << " returned "
+ << rc << std::endl;
+ Assert(rc.isConst());
+ children.push_back(rc);
+ }
+ Node simp = NodeManager::currentNM()->mkNode(un.getKind(), children);
+ Node v = m->getRepresentative(un);
+ Trace("model-builder") << " Setting (" << simp << ") to (" << v << ")"
+ << endl;
+ ufmt.setValue(m, simp, v);
+ default_v = v;
+ }
+ if (default_v.isNull())
+ {
+ // choose default value from model if none exists
+ TypeEnumerator te(f.getType().getRangeType());
+ default_v = (*te);
+ }
+ ufmt.setDefaultValue(m, default_v);
+ bool condenseFuncValues = options::condenseFunctionValues();
+ if (condenseFuncValues)
+ {
+ ufmt.simplify();
+ }
+ std::stringstream ss;
+ ss << "_arg_" << f << "_";
+ Node val = ufmt.getFunctionValue(ss.str().c_str(), condenseFuncValues);
+ m->assignFunctionDefinition(f, val);
+ // ufmt.debugPrint( std::cout, m );
+}
+
+void TheoryEngineModelBuilder::assignHoFunction(TheoryModel* m, Node f)
+{
+ Assert(options::ufHo());
+ TypeNode type = f.getType();
+ std::vector<TypeNode> argTypes = type.getArgTypes();
+ std::vector<Node> args;
+ std::vector<TNode> apply_args;
+ for (unsigned i = 0; i < argTypes.size(); i++)
+ {
+ Node v = NodeManager::currentNM()->mkBoundVar(argTypes[i]);
+ args.push_back(v);
+ if (i > 0)
+ {
+ apply_args.push_back(v);
+ }
+ }
+ // start with the base return value (currently we use the same default value
+ // for all functions)
+ TypeEnumerator te(type.getRangeType());
+ Node curr = (*te);
+ std::map<Node, std::vector<Node> >::iterator itht = m->d_ho_uf_terms.find(f);
+ if (itht != m->d_ho_uf_terms.end())
+ {
+ for (size_t i = 0; i < itht->second.size(); i++)
+ {
+ Node hn = itht->second[i];
+ Trace("model-builder-debug") << " process : " << hn << std::endl;
+ Assert(hn.getKind() == kind::HO_APPLY);
+ Assert(m->areEqual(hn[0], f));
+ Node hni = m->getRepresentative(hn[1]);
+ Trace("model-builder-debug2") << " get rep : " << hn[0]
+ << " returned " << hni << std::endl;
+ Assert(hni.isConst());
+ Assert(hni.getType().isSubtypeOf(args[0].getType()));
+ hni = Rewriter::rewrite(args[0].eqNode(hni));
+ Node hnv = m->getRepresentative(hn);
+ Trace("model-builder-debug2") << " get rep val : " << hn
+ << " returned " << hnv << std::endl;
+ Assert(hnv.isConst());
+ if (!apply_args.empty())
+ {
+ Assert(hnv.getKind() == kind::LAMBDA
+ && hnv[0].getNumChildren() + 1 == args.size());
+ std::vector<TNode> largs;
+ for (unsigned j = 0; j < hnv[0].getNumChildren(); j++)
+ {
+ largs.push_back(hnv[0][j]);
+ }
+ Assert(largs.size() == apply_args.size());
+ hnv = hnv[1].substitute(
+ largs.begin(), largs.end(), apply_args.begin(), apply_args.end());
+ hnv = Rewriter::rewrite(hnv);
+ }
+ Assert(!TypeNode::leastCommonTypeNode(hnv.getType(), curr.getType())
+ .isNull());
+ curr = NodeManager::currentNM()->mkNode(kind::ITE, hni, hnv, curr);
+ }
+ }
+ Node val = NodeManager::currentNM()->mkNode(
+ kind::LAMBDA,
+ NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args),
+ curr);
+ m->assignFunctionDefinition(f, val);
+}
+
+// This struct is used to sort terms by the "size" of their type
+// The size of the type is the number of nodes in the type, for example
+// size of Int is 1
+// size of Function( Int, Int ) is 3
+// size of Function( Function( Bool, Int ), Int ) is 5
+struct sortTypeSize
+{
+ // stores the size of the type
+ std::map<TypeNode, unsigned> d_type_size;
+ // get the size of type tn
+ unsigned getTypeSize(TypeNode tn)
+ {
+ std::map<TypeNode, unsigned>::iterator it = d_type_size.find(tn);
+ if (it != d_type_size.end())
+ {
+ return it->second;
+ }
+ else
+ {
+ unsigned sum = 1;
+ for (unsigned i = 0; i < tn.getNumChildren(); i++)
+ {
+ sum += getTypeSize(tn[i]);
+ }
+ d_type_size[tn] = sum;
+ return sum;
+ }
+ }
+
+ public:
+ // compares the type size of i and j
+ // returns true iff the size of i is less than that of j
+ // tiebreaks are determined by node value
+ bool operator()(Node i, Node j)
+ {
+ int si = getTypeSize(i.getType());
+ int sj = getTypeSize(j.getType());
+ if (si < sj)
+ {
+ return true;
+ }
+ else if (si == sj)
+ {
+ return i < j;
+ }
+ else
+ {
+ return false;
+ }
+ }
+};
+
+void TheoryEngineModelBuilder::assignFunctions(TheoryModel* m)
+{
+ Trace("model-builder") << "Assigning function values..." << std::endl;
+ std::vector<Node> funcs_to_assign = m->getFunctionsToAssign();
+
+ if (options::ufHo())
+ {
+ // sort based on type size if higher-order
+ Trace("model-builder") << "Sort functions by type..." << std::endl;
+ sortTypeSize sts;
+ std::sort(funcs_to_assign.begin(), funcs_to_assign.end(), sts);
+ }
+
+ if (Trace.isOn("model-builder"))
+ {
+ Trace("model-builder") << "...have " << funcs_to_assign.size()
+ << " functions to assign:" << std::endl;
+ for (unsigned k = 0; k < funcs_to_assign.size(); k++)
+ {
+ Node f = funcs_to_assign[k];
+ Trace("model-builder") << " [" << k << "] : " << f << " : "
+ << f.getType() << std::endl;
+ }
+ }
+
+ // construct function values
+ for (unsigned k = 0; k < funcs_to_assign.size(); k++)
+ {
+ Node f = funcs_to_assign[k];
+ Trace("model-builder") << " Function #" << k << " is " << f << std::endl;
+ // std::map< Node, std::vector< Node > >::iterator itht =
+ // m->d_ho_uf_terms.find( f );
+ if (!options::ufHo())
+ {
+ Trace("model-builder") << " Assign function value for " << f
+ << " based on APPLY_UF" << std::endl;
+ assignFunction(m, f);
+ }
+ else
+ {
+ Trace("model-builder") << " Assign function value for " << f
+ << " based on curried HO_APPLY" << std::endl;
+ assignHoFunction(m, f);
+ }
+ }
+ Trace("model-builder") << "Finished assigning function values." << std::endl;
+}
+
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file theory_model.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Clark Barrett, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Model class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__THEORY_MODEL_BUILDER_H
+#define __CVC4__THEORY__THEORY_MODEL_BUILDER_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "theory/theory_model.h"
+
+namespace CVC4 {
+namespace theory {
+
+/** TheoryEngineModelBuilder class
+ *
+ * This is the class used by TheoryEngine
+ * for constructing TheoryModel objects, which is the class
+ * that represents models for a set of assertions.
+ *
+ * A call to TheoryEngineModelBuilder::buildModel(...) is made
+ * after a full effort check passes with no theory solvers
+ * adding lemmas or conflicts, and theory combination passes
+ * with no splits on shared terms. If buildModel is successful,
+ * this will set up the data structures in TheoryModel to represent
+ * a model for the current set of assertions.
+ */
+class TheoryEngineModelBuilder : public ModelBuilder
+{
+ typedef std::unordered_map<Node, Node, NodeHashFunction> NodeMap;
+ typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+
+ public:
+ TheoryEngineModelBuilder(TheoryEngine* te);
+ virtual ~TheoryEngineModelBuilder() {}
+ /** Build model function.
+ *
+ * Should be called only on TheoryModels m.
+ *
+ * This constructs the model m, via the following steps:
+ * (1) call TheoryEngine::collectModelInfo,
+ * (2) builder-specified pre-processing,
+ * (3) find the equivalence classes of m's
+ * equality engine that initially contain constants,
+ * (4) assign constants to all equivalence classes
+ * of m's equality engine, through alternating
+ * iterations of evaluation and enumeration,
+ * (5) builder-specific post-processing.
+ *
+ * This function returns false if any of the above
+ * steps results in a lemma sent on an output channel.
+ * Lemmas may be sent on an output channel by this
+ * builder in steps (2) or (5), for instance, if the model we
+ * are building fails to satisfy a quantified formula.
+ */
+ virtual bool buildModel(Model* m) override;
+ /** Debug check model.
+ *
+ * This throws an assertion failure if the model
+ * contains an equivalence class with two terms t1 and t2
+ * such that t1^M != t2^M.
+ */
+ void debugCheckModel(Model* m);
+
+ protected:
+ /** pointer to theory engine */
+ TheoryEngine* d_te;
+
+ //-----------------------------------virtual functions
+ /** pre-process build model
+ * Do pre-processing specific to this model builder.
+ * Called in step (2) of the build construction,
+ * described above.
+ */
+ virtual bool preProcessBuildModel(TheoryModel* m);
+ /** process build model
+ * Do processing specific to this model builder.
+ * Called in step (5) of the build construction,
+ * described above.
+ * By default, this assigns values to each function
+ * that appears in m's equality engine.
+ */
+ virtual bool processBuildModel(TheoryModel* m);
+ /** debug the model
+ * Check assertions and printing debug information for the model.
+ * Calls after step (5) described above is complete.
+ */
+ virtual void debugModel(TheoryModel* m) {}
+ //-----------------------------------end virtual functions
+
+ /** is n assignable?
+ *
+ * A term n is assignable 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.
+ */
+ bool isAssignable(TNode n);
+ /** add assignable subterms
+ * Adds all assignable subterms of n to tm's equality engine.
+ */
+ void addAssignableSubterms(TNode n, TheoryModel* tm, NodeSet& cache);
+ /** normalize representative r
+ *
+ * This returns a term that is equivalent to r's
+ * interpretation in the model m. It may do so
+ * by rewriting the application of r's operator to the
+ * result of normalizing each of r's children, if
+ * each child is constant.
+ */
+ Node normalize(TheoryModel* m, TNode r, bool evalOnly);
+ /** assign constant representative
+ *
+ * Called when equivalence class eqc is assigned a constant
+ * representative const_rep.
+ *
+ * eqc should be a representative of tm's equality engine.
+ */
+ void assignConstantRep(TheoryModel* tm, Node eqc, Node const_rep);
+ /** add to type list
+ *
+ * This adds to type_list the list of types that tn is built from.
+ * For example, if tn is (Array Int Bool) and type_list is empty,
+ * then we append ( Int, Bool, (Array Int Bool) ) to type_list.
+ */
+ void addToTypeList(
+ TypeNode tn,
+ std::vector<TypeNode>& type_list,
+ std::unordered_set<TypeNode, TypeNodeHashFunction>& visiting);
+ /** assign function f based on the model m.
+ * This construction is based on "table form". For example:
+ * (f 0 1) = 1
+ * (f 0 2) = 2
+ * (f 1 1) = 3
+ * ...
+ * becomes:
+ * f = (lambda xy. (ite (and (= x 0) (= y 1)) 1
+ * (ite (and (= x 0) (= y 2)) 2
+ * (ite (and (= x 1) (= y 1)) 3 ...)))
+ */
+ void assignFunction(TheoryModel* m, Node f);
+ /** assign function f based on the model m.
+ * This construction is based on "dag form". For example:
+ * (f 0 1) = 1
+ * (f 0 2) = 2
+ * (f 1 1) = 3
+ * ...
+ * becomes:
+ * f = (lambda xy. (ite (= x 0) (ite (= y 1) 1
+ * (ite (= y 2) 2 ...))
+ * (ite (= x 1) (ite (= y 1) 3 ...)
+ * ...))
+ *
+ * where the above is represented as a directed acyclic graph (dag).
+ * This construction is accomplished by assigning values to (f c)
+ * terms before f, e.g.
+ * (f 0) = (lambda y. (ite (= y 1) 1
+ * (ite (= y 2) 2 ...))
+ * (f 1) = (lambda y. (ite (= y 1) 3 ...))
+ * where
+ * f = (lambda xy. (ite (= x 0) ((f 0) y)
+ * (ite (= x 1) ((f 1) y) ...))
+ */
+ void assignHoFunction(TheoryModel* m, Node f);
+ /** assign functions
+ *
+ * Assign all unassigned functions in the model m (those returned by
+ * TheoryModel::getFunctionsToAssign),
+ * using the two functions above. Currently:
+ * If ufHo is disabled, we call assignFunction for all functions.
+ * If ufHo is enabled, we call assignHoFunction.
+ */
+ void assignFunctions(TheoryModel* m);
+
+ private:
+ /** normalized cache
+ * A temporary cache mapping terms to their
+ * normalized form, used during buildModel.
+ */
+ NodeMap d_normalizedCache;
+ /** mapping from terms to the constant associated with their equivalence class
+ */
+ std::map<Node, Node> d_constantReps;
+
+ //------------------------------------for codatatypes
+ /** is v an excluded codatatype value?
+ *
+ * If this returns true, then v is a value
+ * that cannot be used during enumeration in step (4)
+ * of model construction.
+ *
+ * repSet is the set of representatives of the same type as v,
+ * assertedReps is a map from representatives t,
+ * eqc is the equivalence class that v reside.
+ *
+ * This function is used to avoid alpha-equivalent
+ * assignments for codatatype terms, described in
+ * Reynolds/Blanchette CADE 2015. In particular,
+ * this function returns true if v is in
+ * the set V^{x}_I from page 9, where x is eqc
+ * and I is the model we are building.
+ */
+ bool isExcludedCdtValue(Node v,
+ std::set<Node>* repSet,
+ std::map<Node, Node>& assertedReps,
+ Node eqc);
+ /** is codatatype value match
+ *
+ * This returns true if v is r{ eqc -> t } for some t.
+ * If this function returns true, then t above is
+ * stored in eqc_m.
+ */
+ bool isCdtValueMatch(Node v, Node r, Node eqc, Node& eqc_m);
+ //------------------------------------end for codatatypes
+
+ //---------------------------------for debugging finite model finding
+ /** does type tn involve an uninterpreted sort? */
+ bool involvesUSort(TypeNode tn);
+ /** is v an excluded value based on uninterpreted sorts?
+ * This gives an assertion failure in the case that v contains
+ * an uninterpreted constant whose index is out of the bounds
+ * specified by eqc_usort_count.
+ */
+ bool isExcludedUSortValue(std::map<TypeNode, unsigned>& eqc_usort_count,
+ Node v,
+ std::map<Node, bool>& visited);
+ //---------------------------------end for debugging finite model finding
+
+}; /* class TheoryEngineModelBuilder */
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__THEORY_MODEL_BUILDER_H */
--- /dev/null
+/********************* */
+/*! \file type_set.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Clark Barrett, Andrew Reynolds, Morgan Deters
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Implementation of type set class
+ **/
+#include "theory/type_set.h"
+
+using namespace std;
+using namespace CVC4::kind;
+
+namespace CVC4 {
+namespace theory {
+
+TypeSet::~TypeSet()
+{
+ iterator it;
+ for (it = d_typeSet.begin(); it != d_typeSet.end(); ++it)
+ {
+ if ((*it).second != NULL)
+ {
+ delete (*it).second;
+ }
+ }
+ TypeToTypeEnumMap::iterator it2;
+ for (it2 = d_teMap.begin(); it2 != d_teMap.end(); ++it2)
+ {
+ if ((*it2).second != NULL)
+ {
+ delete (*it2).second;
+ }
+ }
+}
+
+void TypeSet::setTypeEnumeratorProperties(TypeEnumeratorProperties* tep)
+{
+ d_tep = tep;
+}
+
+void TypeSet::add(TypeNode t, TNode n)
+{
+ iterator it = d_typeSet.find(t);
+ std::set<Node>* s;
+ if (it == d_typeSet.end())
+ {
+ s = new std::set<Node>;
+ d_typeSet[t] = s;
+ }
+ else
+ {
+ s = (*it).second;
+ }
+ s->insert(n);
+}
+
+std::set<Node>* TypeSet::getSet(TypeNode t) const
+{
+ const_iterator it = d_typeSet.find(t);
+ if (it == d_typeSet.end())
+ {
+ return NULL;
+ }
+ return (*it).second;
+}
+
+Node TypeSet::nextTypeEnum(TypeNode t, bool useBaseType)
+{
+ TypeEnumerator* te;
+ TypeToTypeEnumMap::iterator it = d_teMap.find(t);
+ if (it == d_teMap.end())
+ {
+ te = new TypeEnumerator(t, d_tep);
+ d_teMap[t] = te;
+ }
+ else
+ {
+ te = (*it).second;
+ }
+ if (te->isFinished())
+ {
+ return Node();
+ }
+
+ if (useBaseType)
+ {
+ t = t.getBaseType();
+ }
+ iterator itSet = d_typeSet.find(t);
+ std::set<Node>* s;
+ if (itSet == d_typeSet.end())
+ {
+ s = new std::set<Node>;
+ d_typeSet[t] = s;
+ }
+ else
+ {
+ s = (*itSet).second;
+ }
+ Node n = **te;
+ while (s->find(n) != s->end())
+ {
+ ++(*te);
+ if (te->isFinished())
+ {
+ return Node();
+ }
+ n = **te;
+ }
+ s->insert(n);
+ // add all subterms of n to this set as well
+ // this is necessary for parametric types whose values are constructed from
+ // other types to ensure that we do not enumerate subterms of other
+ // previously enumerated values
+ std::unordered_set<TNode, TNodeHashFunction> visited;
+ addSubTerms(n, visited);
+ ++(*te);
+ return n;
+}
+
+void TypeSet::addSubTerms(TNode n,
+ std::unordered_set<TNode, TNodeHashFunction>& visited,
+ bool topLevel)
+{
+ if (visited.find(n) == visited.end())
+ {
+ visited.insert(n);
+ if (!topLevel)
+ {
+ add(n.getType(), n);
+ }
+ for (unsigned i = 0; i < n.getNumChildren(); i++)
+ {
+ addSubTerms(n[i], visited, false);
+ }
+ }
+}
+
+} /* namespace CVC4::theory */
+} /* namespace CVC4 */
--- /dev/null
+/********************* */
+/*! \file type_set.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ ** Clark Barrett, Morgan Deters, Andrew Reynolds
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved. See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief Type set class
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__TYPE_SET_H
+#define __CVC4__THEORY__TYPE_SET_H
+
+#include <unordered_map>
+#include <unordered_set>
+
+#include "theory/type_enumerator.h"
+
+namespace CVC4 {
+namespace theory {
+
+/* Type set
+ *
+ * This class encapsulates a map from types to sets of nodes.
+ */
+class TypeSet
+{
+ public:
+ typedef std::unordered_map<TypeNode, std::set<Node>*, TypeNodeHashFunction>
+ TypeSetMap;
+ typedef std::unordered_map<TypeNode, TypeEnumerator*, TypeNodeHashFunction>
+ TypeToTypeEnumMap;
+ typedef TypeSetMap::iterator iterator;
+ typedef TypeSetMap::const_iterator const_iterator;
+
+ public:
+ TypeSet() : d_tep(NULL) {}
+ ~TypeSet();
+ /** set the properties of the type set
+ *
+ * These indicate information such as finite bounds
+ * on the number of unique uninterpreted constants that can be
+ * enumerated by this class.
+ */
+ void setTypeEnumeratorProperties(TypeEnumeratorProperties* tep);
+ /** add node n to the set of values of t */
+ void add(TypeNode t, TNode n);
+ /** get the set of values of type t */
+ std::set<Node>* getSet(TypeNode t) const;
+ /** get the next enumerated term of type t
+ *
+ * useBaseType is whether
+ */
+ Node nextTypeEnum(TypeNode t, bool useBaseType = false);
+
+ bool empty() { return d_typeSet.empty(); }
+ iterator begin() { return d_typeSet.begin(); }
+ iterator end() { return d_typeSet.end(); }
+ static TypeNode getType(iterator it) { return (*it).first; }
+ static std::set<Node>& getSet(iterator it) { return *(*it).second; }
+ private:
+ /** sets of values for each type */
+ TypeSetMap d_typeSet;
+ /** type enumerators for each type */
+ TypeToTypeEnumMap d_teMap;
+ /** pointer the type enumerator properties for this class. */
+ TypeEnumeratorProperties* d_tep;
+
+ /* add all sub-terms of n to the sets of this class
+ *
+ * If topLevel is true, then we add strict subterms only.
+ *
+ * Note that recursive traversal here is over enumerated expressions
+ * (very low expression depth).
+ */
+ void addSubTerms(TNode n,
+ std::unordered_set<TNode, TNodeHashFunction>& visited,
+ bool topLevel = true);
+}; /* class TypeSet */
+
+} /* CVC4::theory namespace */
+} /* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__TYPE_SET_H */
projects / cvc5.git / commitdiff