diff options
Diffstat (limited to 'src/theory/arith/theory_arith.h')
-rw-r--r-- | src/theory/arith/theory_arith.h | 40 |
1 files changed, 35 insertions, 5 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index d211cd37d..82bb47eb4 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -1,7 +1,7 @@ /********************* */ /** theory_arith.h ** Original author: mdeters - ** Major contributors: none + ** Major contributors: taking ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) @@ -20,22 +20,52 @@ #include "theory/theory.h" #include "context/context.h" +#include "context/cdlist.h" + +#include "theory/arith/delta_rational.h" +#include "theory/arith/tableau.h" +#include "theory/arith/arith_rewriter.h" namespace CVC4 { namespace theory { namespace arith { class TheoryArith : public Theory { +private: + ArithConstants d_constants; + + context::CDList<Node> d_diseq; + Tableau d_tableau; + ArithRewriter d_rewriter; + public: TheoryArith(context::Context* c, OutputChannel& out) : - Theory(c, out) { - } + Theory(c, out), + d_constants(NodeManager::currentNM()), d_diseq(c), d_rewriter(&d_constants) + {} + + Node rewrite(TNode n); void preRegisterTerm(TNode n) { Unimplemented(); } - void registerTerm(TNode n) { Unimplemented(); } - void check(Effort e) { Unimplemented(); } + void registerTerm(TNode n); + void check(Effort e); void propagate(Effort e) { Unimplemented(); } void explain(TNode n, Effort e) { Unimplemented(); } + +private: + void AssertLower(TNode n); + void AssertUpper(TNode n); + void update(TNode x_i, DeltaRational& v); + void pivotAndUpdate(TNode x_i, TNode x_j, DeltaRational& v); + TNode updateInconsistentVars(); + + TNode selectSlackBelow(TNode x_i); + TNode selectSlackAbove(TNode x_i); + TNode selectSmallestInconsistentVar(); + + Node generateConflictAbove(TNode conflictVar); + Node generateConflictBelow(TNode conflictVar); + }; }/* CVC4::theory::arith namespace */ |