From: Clark Barrett Date: Fri, 30 Nov 2012 22:44:26 +0000 (+0000) Subject: Fix assertion in smt_engine's getValue X-Git-Tag: cvc5-1.0.0~7509 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=2eff007e694baec68204021164238dcc274e695c;p=cvc5.git Fix assertion in smt_engine's getValue Minor changes to RELASE-NOTES --- diff --git a/RELEASE-NOTES b/RELEASE-NOTES index 5a6ad2cb9..38d1459ad 100644 --- a/RELEASE-NOTES +++ b/RELEASE-NOTES @@ -1,11 +1,11 @@ -Release Notes for CVC4 1.0, October 2012 +Release Notes for CVC4 1.0, December 2012 ** Getting started If you run CVC4 without arguments, you will find yourself in an interactive CVC4 session, which expects commands in CVC4's native language (the so-called "presentation" language). To use SMT-LIB, use the "--lang smt" option on the -command line. For stricter adherence to the standard, use "--smtlib" +command line. For stricter adherence to the standard, use "--smtlib-strict" (see below regarding SMT-LIB compliance). When a filename is given on the command line, the file's extension determines @@ -15,10 +15,16 @@ this, you can use the --lang option. ** Type correctness -Type Correctness Conditions (TCCs), and the checking of such, are not -supported by CVC4 1.0. Thus, a function defined only on integers can be -applied to REAL (as INT is a subtype of REAL), and CVC4 will not complain, -but may produce strange results. For example: +The CVC family of systems relies on Type Correctness Conditions (TCCs) when +mixing two types that have a compatible base type. TCCs, and the checking of +such, are not supported by CVC4 1.0. This is an issue when mixing integers and +reals. A function defined only on integers can be applied to REAL (as INT is a +subtype of REAL), and CVC4 will not complain. It is up to the user to ensure +that the REAL expression must be an integer. If the REAL expression is not +an integer and is used where an INT is expected, CVC4 may produce strange +results. + +For example: f : INT -> INT; ASSERT f(1/3) = 0; @@ -28,9 +34,10 @@ but may produce strange results. For example: COUNTEREXAMPLE; % f : (INT) -> INT = LAMBDA(x1:INT) : 0; -CVC3 can be used to produce TCCs for this input (with the +dump-tcc option). -The TCC can be checked by CVC3 or another solver. (CVC3 can also check -TCCs while solving with +tcc.) +This kind of problem can be identified by checking TCCs. Though CVC4 does not +(yet) support TCCs, CVC3 can be used to produce TCCs for this input (with the ++dump-tcc option). The TCC can be checked by CVC3 or another solver. (CVC3 can +also check TCCs while solving with +tcc.) ** Changes in CVC's Presentation Language @@ -71,7 +78,7 @@ Every effort has been made to make CVC4 compliant with the SMT-LIB 2.0 standard (http://smtlib.org/). However, when parsing SMT-LIB input, certain default settings don't match what is stated in the official standard. To make CVC4 adhere more strictly to the standard, use the -"--smtlib" command-line option. Even with this setting, CVC4 is +"--smtlib-strict" command-line option. Even with this setting, CVC4 is somewhat lenient; some non-conforming input may still be parsed and processed. @@ -79,10 +86,6 @@ For the latest news on SMT-LIB compliance, please check: http://church.cims.nyu.edu/wiki/SMT-LIB_Compliance -However, please note that that page may refer to a more recent version -(and possibly an unreleased, development version) than the one you are -looking at. - ** Getting statistics Statistics can be dumped on exit (both normal and abnormal exits) with @@ -100,7 +103,7 @@ case, you can use "-vv" (double verbosity) to see what CVC4 is doing. Time-limited runs are not deterministic; two consecutive runs with the same time limit might produce different results (i.e., one may time out -and responds with "unknown", while the other completes and provides an +and respond with "unknown", while the other completes and provides an answer). To ensure that results are reproducible, use --rlimit or --rlimit-per. These options take a "resource count" (presently, based on the number of SAT conflicts) that limits the search time. A word of @@ -153,6 +156,6 @@ CVC4 is under active development. Should you find a bug in CVC4's documentation, behavior, API, or SMT-LIB compliance, or if you have a feature request, please let us know on our bugtracker at - http://church.cims.nyu.edu/bugs/ + http://cvc4.cs.nyu.edu/bugs/ or send an email to cvc-bugs@cims.nyu.edu. diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 25a066e4a..b5ed59912 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2622,7 +2622,7 @@ Expr SmtEngine::getValue(const Expr& ex) throw(ModalException, LogicException) { Assert(resultNode.isNull() || resultNode.getType().isSubtypeOf(n.getType())); // ensure it's a constant - Assert(resultNode.isConst()); + Assert(resultNode.getKind() == kind::LAMBDA || resultNode.isConst()); if(options::abstractValues() && resultNode.getType().isArray()) { resultNode = d_private->mkAbstractValue(resultNode);