diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
|---|---|---|
| committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2012-07-12 18:30:15 +0000 |
| commit | 65798541fa437278cde0c759ab70fd9fa4fe9638 (patch) | |
| tree | 27341327b8159e58a5ce6371bede6129bf67beb3 /src/theory/uf/theory_uf.h | |
| parent | 78d8b3ce56a1fd243acb54d2aaaf6d716e3b9788 (diff) | |
merged fmf-devel branch, includes support for SMT2 command get-value and (extended) SMT command get-model. added collectModelInfo and removed getValue from theory interface. merge also includes major updates to finite model finding module (from CASC), added fmf options, some updates to strong solver and quantifiers engine interface. The test recursion_breaker_black currently fails for me on production builds, Morgan is planning to look into this.
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index db417b08c..604b1f44c 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -132,8 +132,8 @@ private: Node d_conflictNode; /** - * Should be called to propagate the literal. We use a node here - * since some of the propagated literals are not kept anywhere. + * Should be called to propagate the literal. We use a node here + * since some of the propagated literals are not kept anywhere. */ bool propagate(TNode literal); @@ -193,6 +193,8 @@ public: void preRegisterTerm(TNode term); Node explain(TNode n); + void collectModelInfo( TheoryModel* m ); + void ppStaticLearn(TNode in, NodeBuilder<>& learned); void presolve(); |