diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-09-29 05:15:30 +0000 |
commit | c94347913fa464b1ec6a3da2ab21e319c0c42e02 (patch) | |
tree | 6c8252385365e5dacc86ce8c364c3d06332d39a7 /src/theory/example | |
parent | 7adcbaf2eac82be6ca8cf1569bab80c961710950 (diff) |
Some base infrastructure for user push/pop; a few bugfixes to user push/pop and model gen also.
I also expect this commit to fix bug #273.
No performance change is expected on regressions with this commit, see
http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2871&reference_id=2863
Diffstat (limited to 'src/theory/example')
-rw-r--r-- | src/theory/example/theory_uf_tim.cpp | 4 | ||||
-rw-r--r-- | src/theory/example/theory_uf_tim.h | 4 |
2 files changed, 4 insertions, 4 deletions
diff --git a/src/theory/example/theory_uf_tim.cpp b/src/theory/example/theory_uf_tim.cpp index ae37dfe99..03787703a 100644 --- a/src/theory/example/theory_uf_tim.cpp +++ b/src/theory/example/theory_uf_tim.cpp @@ -27,8 +27,8 @@ using namespace CVC4::theory; using namespace CVC4::theory::uf; using namespace CVC4::theory::uf::tim; -TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out, Valuation valuation) : - TheoryUF(c, out, valuation), +TheoryUFTim::TheoryUFTim(Context* c, UserContext* u, OutputChannel& out, Valuation valuation) : + Theory(THEORY_UF, c, u, out, valuation), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), diff --git a/src/theory/example/theory_uf_tim.h b/src/theory/example/theory_uf_tim.h index 70c60728f..b47536f07 100644 --- a/src/theory/example/theory_uf_tim.h +++ b/src/theory/example/theory_uf_tim.h @@ -43,7 +43,7 @@ namespace theory { namespace uf { namespace tim { -class TheoryUFTim : public TheoryUF { +class TheoryUFTim : public Theory { private: @@ -85,7 +85,7 @@ private: public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUFTim(context::Context* c, OutputChannel& out, Valuation valuation); + TheoryUFTim(context::Context* c, context::UserContext* u, OutputChannel& out, Valuation valuation); /** Destructor for the TheoryUF object. */ ~TheoryUFTim(); |