diff options
author | Morgan Deters <mdeters@gmail.com> | 2010-10-09 04:24:15 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2010-10-09 04:24:15 +0000 |
commit | 97668b64994c5749a5a75822136de49841d2c15d (patch) | |
tree | 23dd1852741a847f6228cc063b0a5ad7ec3c2af3 /src/theory/theory.h | |
parent | e63abd23b45a078a42cafb277a4817abb4d044a1 (diff) |
Model generation for arith, boolean, and uf theories via
(get-value ...) SMT-LIBv2 command. As per SMT-LIBv2 spec,
you must pass --interactive --produce-models on the command
line (although they don't currently make us do any extra
work). Closes bug #213.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 66 |
1 files changed, 53 insertions, 13 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index 2711a0b95..df9dcafef 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -262,9 +262,11 @@ public: // TODO add compiler annotation "constant function" here static bool minEffortOnly(Effort e) { return e == MIN_EFFORT; } static bool quickCheckOrMore(Effort e) { return e >= QUICK_CHECK; } - static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && e < STANDARD; } + static bool quickCheckOnly(Effort e) { return e >= QUICK_CHECK && + e < STANDARD; } static bool standardEffortOrMore(Effort e) { return e >= STANDARD; } - static bool standardEffortOnly(Effort e) { return e >= STANDARD && e < FULL_EFFORT; } + static bool standardEffortOnly(Effort e) { return e >= STANDARD && + e < FULL_EFFORT; } static bool fullEffort(Effort e) { return e >= FULL_EFFORT; } /** @@ -328,7 +330,8 @@ public: * (ITE true x y). */ virtual RewriteResponse preRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl; + Debug("theory-rewrite") << "no pre-rewriting to perform for " + << n << std::endl; return RewriteComplete(n); } @@ -340,7 +343,8 @@ public: * memory leakage). */ virtual RewriteResponse postRewrite(TNode n, bool topLevel) { - Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl; + Debug("theory-rewrite") << "no post-rewriting to perform for " + << n << std::endl; return RewriteComplete(n); } @@ -366,18 +370,21 @@ public: } /** - * This method is called to notify a theory that the node n should be considered a "shared term" by this theory + * This method is called to notify a theory that the node n should + * be considered a "shared term" by this theory */ virtual void addSharedTerm(TNode n) { } /** - * This method is called by the shared term manager when a shared term lhs - * which this theory cares about (either because it received a previous - * addSharedTerm call with lhs or because it received a previous notifyEq call - * with lhs as the second argument) becomes equal to another shared term rhs. - * This call also serves as notice to the theory that the shared term manager - * now considers rhs the representative for this equivalence class of shared - * terms, so future notifications for this class will be based on rhs not lhs. + * This method is called by the shared term manager when a shared + * term lhs which this theory cares about (either because it + * received a previous addSharedTerm call with lhs or because it + * received a previous notifyEq call with lhs as the second + * argument) becomes equal to another shared term rhs. This call + * also serves as notice to the theory that the shared term manager + * now considers rhs the representative for this equivalence class + * of shared terms, so future notifications for this class will be + * based on rhs not lhs. */ virtual void notifyEq(TNode lhs, TNode rhs) { } @@ -405,6 +412,38 @@ public: virtual void explain(TNode n, Effort level = FULL_EFFORT) = 0; /** + * Return the value of a node (typically used after a ). If the + * theory supports model generation but has no value for this node, + * it should return Node::null(). If the theory doesn't support + * model generation at all, or usually would but doesn't in its + * current state, it should throw an exception saying so. + * + * The TheoryEngine is passed in so that you can recursively request + * values for the Node's children. This is important because the + * TheoryEngine takes care of simple cases (metakind CONSTANT, + * Boolean-valued VARIABLES, ...) and can dispatch to other theories + * if that's necessary. Only call your own getValue() recursively + * if you *know* that you are responsible handle the Node you're + * asking for; other theories can use your types, so be careful + * here! To be safe, it's best to delegate back to the + * TheoryEngine. + * + * Usually, you need to handle at least the two cases of EQUAL and + * VARIABLE---EQUAL in case a value of yours is on the LHS of an + * EQUAL, and VARIABLE for variables of your types. You also need + * to support any operators that can survive your rewriter. You + * don't need to handle constants, as they are handled by the + * TheoryEngine. + * + * There are some gotchas here. The user may be requesting the + * value of an expression that wasn't part of the satisfiable + * assertion, or has been declared since. If you don't have a value + * and suspect this situation is the case, return Node::null() + * rather than throwing an exception. + */ + virtual Node getValue(TNode n, TheoryEngine* engine) = 0; + + /** * Identify this theory (for debugging, dynamic configuration, * etc..) */ @@ -550,7 +589,8 @@ std::ostream& operator<<(std::ostream& os, Theory::Effort level); }/* CVC4::theory namespace */ -inline std::ostream& operator<<(std::ostream& out, const CVC4::theory::Theory& theory) { +inline std::ostream& operator<<(std::ostream& out, + const CVC4::theory::Theory& theory) { return out << theory.identify(); } |