summaryrefslogtreecommitdiff
path: root/src/theory/booleans
diff options
context:
space:
mode:
authorDejan Jovanović <dejan.jovanovic@gmail.com>2012-05-03 20:18:18 +0000
committerDejan Jovanović <dejan.jovanovic@gmail.com>2012-05-03 20:18:18 +0000
commit1433806056059339dd16ae8e431feaae23553150 (patch)
treecf678baa687b1a19e479c28a1c01470bb2f120c7 /src/theory/booleans
parent8ef2015de66fc409a2a2958b9452c0c9b1456ee3 (diff)
Some cleanup starting off from trying to understand the sharing code. Changes include
* fixed term visitor from the bvprop branch * removed all the warnings from builds -- warnings are there to be noted *NOT* to be used as scribbles * moved the LogicInfo into the theory constructor
Diffstat (limited to 'src/theory/booleans')
-rw-r--r--src/theory/booleans/theory_bool.h4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/theory/booleans/theory_bool.h b/src/theory/booleans/theory_bool.h
index fedc47aeb..99b5b6007 100644
--- a/src/theory/booleans/theory_bool.h
+++ b/src/theory/booleans/theory_bool.h
@@ -30,8 +30,8 @@ namespace booleans {
class TheoryBool : public Theory {
public:
- TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation) :
- Theory(THEORY_BOOL, c, u, out, valuation) {
+ TheoryBool(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation, const LogicInfo& logicInfo) :
+ Theory(THEORY_BOOL, c, u, out, valuation, logicInfo) {
}
Node getValue(TNode n);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback