diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-10-27 11:20:50 -0500 |
---|---|---|
committer | GitHub <noreply@github.com> | 2017-10-27 11:20:50 -0500 |
commit | 079ed9540d498bcbb58f2f0fbe87bdae28101d1e (patch) | |
tree | 8c3ba1818dc515c1714b23555460a3a39192acc5 /src/theory/theory_model.cpp | |
parent | 03cc40cc070df0bc11c1556cef3016f784a95d23 (diff) |
Refactor theory model (#1236)
* Refactor theory model, working on making RepSet references const.
* Encapsulation of members of rep set.
* More documentation on rep set.
* Swap names
* Reference issues.
* Minor
* Minor
* New clang format.
Diffstat (limited to 'src/theory/theory_model.cpp')
-rw-r--r-- | src/theory/theory_model.cpp | 27 |
1 files changed, 11 insertions, 16 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index a4b36b87c..490ed45c9 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -252,7 +252,11 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c // TODO: if func models not enabled, throw an error? Unreachable(); } - }else if(t.isRegExp()) { + } + else if (!t.isFirstClass()) + { + // this is the class for regular expressions + // we simply invoke the rewriter on them ret = Rewriter::rewrite(ret); } else { if (options::omitDontCares() && useDontCares) { @@ -279,18 +283,6 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c return ret; } -Node TheoryModel::getDomainValue( TypeNode tn, std::vector< Node >& exclude ){ - if( d_rep_set.d_type_reps.find( tn )!=d_rep_set.d_type_reps.end() ){ - //try to find a pre-existing arbitrary element - for( size_t i=0; i<d_rep_set.d_type_reps[tn].size(); i++ ){ - if( std::find( exclude.begin(), exclude.end(), d_rep_set.d_type_reps[tn][i] )==exclude.end() ){ - return d_rep_set.d_type_reps[tn][i]; - } - } - } - return Node::null(); -} - /** add substitution */ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ if( !d_substitutions.hasSubstitution( x ) ){ @@ -415,7 +407,8 @@ void TheoryModel::assertEqualityEngine(const eq::EqualityEngine* ee, set<Node>* if (first) { rep = (*eqc_i); //add the term (this is specifically for the case of singleton equivalence classes) - if( !rep.getType().isRegExp() ){ + if (rep.getType().isFirstClass()) + { d_equalityEngine->addTerm( rep ); Trace("model-builder-debug") << "Add term to ee within assertEqualityEngine: " << rep << std::endl; } @@ -636,7 +629,7 @@ void TheoryEngineModelBuilder::checkTerms(TNode n, TheoryModel* tm, NodeSet& cac 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.d_values_to_terms[const_rep] = eqc; + tm->d_rep_set.setTermForRepresentative(const_rep, eqc); } bool TheoryEngineModelBuilder::isExcludedCdtValue( Node val, std::set<Node>* repSet, std::map< Node, Node >& assertedReps, Node eqc ) { @@ -1238,7 +1231,9 @@ Node TheoryEngineModelBuilder::normalize(TheoryModel* m, TNode r, bool evalOnly) retNode = NodeManager::currentNM()->mkNode( r.getKind(), children ); if (childrenConst) { retNode = Rewriter::rewrite(retNode); - Assert(retNode.getKind()==kind::APPLY_UF || retNode.getType().isRegExp() || retNode.isConst()); + Assert(retNode.getKind() == kind::APPLY_UF + || !retNode.getType().isFirstClass() + || retNode.isConst()); } } d_normalizedCache[r] = retNode; |