diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-03 17:13:31 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-11-27 17:55:53 -0500 |
| commit | a97891f9cc892fdc261cd4e3d3229ec68f05b45e (patch) | |
| tree | a05c30ddbe81d9dd084a2e024875f829d6f1f3a7 /src/smt | |
| parent | b28a42c3a4fd8c9b079b157ad8ff36e581b60d29 (diff) | |
General pre-release cleanup commit
* Rename {model,util_model}.{h,cpp} files to match class names
* Fix alreadyVisited() issue in TheoryEngine
* Remove spurious Message that causes compliance issues
* Update copyrights, fix public/private markings in headers
* minor comment fixes
* remove EXTRACT_OP as a special-case in typechecker
* note about rewriters in theoryskel readme
* Clean up some compiler warnings
* Code typos and spacing
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/boolean_terms.cpp | 2 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 8 |
2 files changed, 5 insertions, 5 deletions
diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp index 1157c464e..108c88829 100644 --- a/src/smt/boolean_terms.cpp +++ b/src/smt/boolean_terms.cpp @@ -18,7 +18,7 @@ #include "smt/boolean_terms.h" #include "smt/smt_engine.h" #include "theory/theory_engine.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "theory/booleans/boolean_term_conversion_mode.h" #include "theory/booleans/options.h" #include "expr/kind.h" diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 2cc606fa9..2e1d5de3c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -70,7 +70,7 @@ #include "theory/booleans/boolean_term_conversion_mode.h" #include "theory/booleans/options.h" #include "util/ite_removal.h" -#include "theory/model.h" +#include "theory/theory_model.h" #include "printer/printer.h" #include "prop/options.h" #include "theory/arrays/options.h" @@ -1815,7 +1815,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { return false; } - // No, conflict, go through the literals and solve them + // No conflict, go through the literals and solve them SubstitutionMap constantPropagations(d_smt.d_context); SubstitutionMap newSubstitutions(d_smt.d_context); SubstitutionMap::iterator pos; @@ -1904,7 +1904,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Assert(d_topLevelSubstitutions.apply(t) == t); Assert(newSubstitutions.apply(t) == t); constantPropagations.addSubstitution(t, c); - // vector<pair<Node,Node> > equations;a + // vector<pair<Node,Node> > equations; // constantPropagations.simplifyLHS(t, c, equations, true); // if (!equations.empty()) { // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); @@ -1951,7 +1951,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // } Assert(constantPropagations.apply((*pos).second) == (*pos).second); } -#endif +#endif /* CVC4_ASSERTIONS */ } // Resize the learnt d_nonClausalLearnedLiterals.resize(j); |