diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-15 11:19:08 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-02-16 15:23:00 -0500 |
| commit | f06ae104dc3caf9b4ff01a0b2d49b09ace88faad (patch) | |
| tree | 488669992e6d375450e18a2c92659be3f93f7a88 /src/theory/quantifiers | |
| parent | 5e29fdffd2f72212d699316f9b27e1bf9d6c715c (diff) | |
Some cleanup and copyright updating
* update some copyrights for 2013
* cleaned up some comments/ifdefs, indentation
* some spelling corrections
* add some missing makefiles
Diffstat (limited to 'src/theory/quantifiers')
| -rw-r--r-- | src/theory/quantifiers/inst_gen.h | 10 | ||||
| -rw-r--r-- | src/theory/quantifiers/macros.cpp | 2 | ||||
| -rw-r--r-- | src/theory/quantifiers/term_database.h | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/src/theory/quantifiers/inst_gen.h b/src/theory/quantifiers/inst_gen.h index 94922df18..930133954 100644 --- a/src/theory/quantifiers/inst_gen.h +++ b/src/theory/quantifiers/inst_gen.h @@ -50,10 +50,10 @@ public: int getNumMatches() { return d_matches.size(); } bool getMatch( EqualityQuery* q, int i, InstMatch& m ); Node getMatchValue( int i ) { return d_match_values[i]; } -}; +};/* class InstGenProcess */ -} -} -} +}/* CVC4::theory::quantifiers namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ -#endif +#endif /* __CVC4__THEORY__QUANTIFIERS__INST_GEN_H */ diff --git a/src/theory/quantifiers/macros.cpp b/src/theory/quantifiers/macros.cpp index 9f08764a9..bf67bdd25 100644 --- a/src/theory/quantifiers/macros.cpp +++ b/src/theory/quantifiers/macros.cpp @@ -358,7 +358,7 @@ Node QuantifierMacros::simplify( Node n ){ if( n.getKind()==APPLY_UF ){ Node op = n.getOperator(); if( d_macro_defs.find( op )!=d_macro_defs.end() && !d_macro_defs[op].isNull() ){ - //do subsitutition + //do substitution Node ret = d_macro_defs[op]; ret = ret.substitute( d_macro_basis[op].begin(), d_macro_basis[op].end(), children.begin(), children.end() ); return ret; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 9ac431107..6bfea5c44 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -167,7 +167,7 @@ public: /** get counterexample literal (for cbqi) */ Node getCounterexampleLiteral( Node f ); /** returns node n with bound vars of f replaced by instantiation constants of f - node n : is the futur pattern + node n : is the future pattern node f : is the quantifier containing which bind the variable return a pattern where the variable are replaced by variable for instantiation. |