diff options
author | Clark Barrett <barrett@cs.nyu.edu> | 2012-12-03 04:35:27 +0000 |
---|---|---|
committer | François Bobot <francois@bobot.eu> | 2012-12-06 11:19:17 +0100 |
commit | 4f19239003837851bf4b196deeb067cda8a67543 (patch) | |
tree | 247ec91f5d91239b2169dd8cf186e4b35e973971 /src/theory/model.h | |
parent | b1556c088eb14807610b96800e208055514ba0d7 (diff) |
Fix for fuzzer-found model bug
(cherry picked from commit 25c6e1331d338c6ba8d60224711343986e11cf79)
Diffstat (limited to 'src/theory/model.h')
-rw-r--r-- | src/theory/model.h | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/src/theory/model.h b/src/theory/model.h index 7ccbe2fc3..e283ee183 100644 --- a/src/theory/model.h +++ b/src/theory/model.h @@ -90,11 +90,11 @@ public: * such as contraining the interpretation of uninterpretted functions, * and adding n to the equality engine of this model */ - virtual void addTerm( Node n ); + virtual void addTerm(TNode n); /** assert equality holds in the model */ - void assertEquality( Node a, Node b, bool polarity ); + void assertEquality(TNode a, TNode b, bool polarity); /** assert predicate holds in the model */ - void assertPredicate( Node a, bool polarity ); + void assertPredicate(TNode a, bool polarity); /** assert all equalities/predicates in equality engine hold in the model */ void assertEqualityEngine(const eq::EqualityEngine* ee, std::set<Node>* termSet = NULL); /** assert representative @@ -103,13 +103,13 @@ public: * case of TheoryEngineModelBuilder, it should be called during Theory's collectModelInfo( ... ) * functions where fullModel = true. */ - void assertRepresentative( Node n ); + void assertRepresentative(TNode n); public: /** general queries */ - bool hasTerm( Node a ); - Node getRepresentative( Node a ); - bool areEqual( Node a, Node b ); - bool areDisequal( Node a, Node b ); + bool hasTerm(TNode a); + Node getRepresentative(TNode a); + bool areEqual(TNode a, TNode b); + bool areDisequal(TNode a, TNode b); public: /** get value function for Exprs. */ Expr getValue( Expr expr ) const; |