diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-22 23:09:03 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-22 23:09:03 +0000 |
| commit | 1a99b24c49f9b865a70fa626efcb96571499917e (patch) | |
| tree | cb3c85e9c439925b74cb4f2e5782a5c19d32fe94 /src/theory/arith/theory_arith.h | |
| parent | c0324db3ac7e5984c632f46690f58c333b9a42b2 (diff) | |
* improving arithmetic getEqualityStatus
* some sharing improvements based on model
Diffstat (limited to 'src/theory/arith/theory_arith.h')
| -rw-r--r-- | src/theory/arith/theory_arith.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 929ef1173..ec2df3e17 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -249,6 +249,13 @@ private: /** This implements the Simplex decision procedure. */ SimplexDecisionProcedure d_simplex; + + /** Internal model value for the atom */ + bool getDeltaAtomValue(TNode n); + + /** Internal model value for the node */ + DeltaRational getDeltaValue(TNode n); + public: TheoryArith(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); virtual ~TheoryArith(); |