diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 01:31:07 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-08-01 01:31:07 +0200 |
| commit | 91f40dee752910fca5d749656c0b6ee1bc1281aa (patch) | |
| tree | 4db131923ceabe2fff9f408fc39032bac973e399 /src/smt/smt_engine.h | |
| parent | bf7f7d6960f6e03e90880dd3da9ff1bf00943cf3 (diff) | |
Make --fmf-fun and --macros-quant work in incremental mode. Add regressions.
Diffstat (limited to 'src/smt/smt_engine.h')
| -rw-r--r-- | src/smt/smt_engine.h | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index db0809308..b4c293dff 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -128,6 +128,10 @@ class CVC4_PUBLIC SmtEngine { typedef context::CDList<Expr> AssertionList; /** The type of our internal assignment set */ typedef context::CDHashSet<Node, NodeHashFunction> AssignmentSet; + /** The types for the recursive function definitions */ + typedef context::CDHashMap< Node, TypeNode, NodeHashFunction > TypeNodeMap; + typedef context::CDList<Node> NodeList; + typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; /** Expr manager context */ context::Context* d_context; @@ -151,6 +155,9 @@ class CVC4_PUBLIC SmtEngine { ProofManager* d_proofManager; /** An index of our defined functions */ DefinedFunctionMap* d_definedFunctions; + /** recursive function definition abstractions for --fmf-fun */ + TypeNodeMap* d_fmfRecFunctionsAbs; + NodeListMap* d_fmfRecFunctionsConcrete; /** * The assertion list (before any conversion) for supporting |