diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2019-10-30 15:27:10 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-10-30 15:27:10 -0700 |
| commit | 43ab3f4cd1aa5549cb1aa3c20a2d589614bcb8fc (patch) | |
| tree | cf7b5d7f73a4d4ddc34492334a7d0eb90b57b77b /src/theory/theory_model.cpp | |
| parent | 8dda9531995953c3cec094339002f2ee7cadae08 (diff) | |
Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)
Diffstat (limited to 'src/theory/theory_model.cpp')
| -rw-r--r-- | src/theory/theory_model.cpp | 17 |
1 files changed, 8 insertions, 9 deletions
diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp index 0d82d3f02..da66a2ef2 100644 --- a/src/theory/theory_model.cpp +++ b/src/theory/theory_model.cpp @@ -369,12 +369,11 @@ void TheoryModel::addSubstitution( TNode x, TNode t, bool invalidateCache ){ Node oldX = d_substitutions.getSubstitution(x); // check that either the old substitution is the same, or it now maps to the new substitution if(oldX != t && d_substitutions.apply(oldX) != d_substitutions.apply(t)) { - stringstream ss; - ss << "Two incompatible substitutions added to TheoryModel:\n" - << "the term: " << x << "\n" - << "old mapping: " << d_substitutions.apply(oldX) << "\n" - << "new mapping: " << d_substitutions.apply(t); - InternalError(ss.str()); + InternalError() + << "Two incompatible substitutions added to TheoryModel:\n" + << "the term: " << x << "\n" + << "old mapping: " << d_substitutions.apply(oldX) << "\n" + << "new mapping: " << d_substitutions.apply(t); } #endif /* CVC4_ASSERTIONS */ } @@ -600,7 +599,7 @@ bool TheoryModel::areFunctionValuesEnabled() const } void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { - Assert( d_uf_models.find( f )==d_uf_models.end() ); + Assert(d_uf_models.find(f) == d_uf_models.end()); Trace("model-builder") << " Assigning function (" << f << ") to (" << f_def << ")" << endl; if( options::ufHo() ){ @@ -608,7 +607,7 @@ void TheoryModel::assignFunctionDefinition( Node f, Node f_def ) { f_def = Rewriter::rewrite( f_def ); Trace("model-builder-debug") << "Model value (post-rewrite) : " << f_def << std::endl; - Assert( f_def.isConst() ); + Assert(f_def.isConst()); } // d_uf_models only stores models for variables @@ -646,7 +645,7 @@ std::vector< Node > TheoryModel::getFunctionsToAssign() { // collect functions for( std::map< Node, std::vector< Node > >::iterator it = d_uf_terms.begin(); it != d_uf_terms.end(); ++it ){ Node n = it->first; - Assert( !n.isNull() ); + Assert(!n.isNull()); if( !hasAssignedFunctionDefinition( n ) ){ Trace("model-builder-fun-debug") << "Look at function : " << n << std::endl; if( options::ufHo() ){ |