Age | Commit message (Collapse) | Author |
|
|
|
This cleans up naming of API functions to create first-order constants and variables.
mkVar -> mkConst
mkBoundVar -> mkVar
declareConst is redundant (= mkConst) and thus, in an effort to avoid redundancy, removed.
Note that we want to avoid redundancy in order to reduce code duplication and maintenance
overhead (we do not allow nested API calls, since this is problematic when tracing API calls).
|
|
Fixes 2887.
|
|
The most recent version of SMT-LIB defines bv{add,mul,and,or,xor,xnor}
[0, 1] as left-associative. CVC4 treats all but bvxnor as having
variable arity anyway but the arity check was too strict when using
`--strict-parsing`. This commit changes the strict parsing check. For
bvxnor, it adds code to the parser that expands an application of bvxnor
into multiple applications of a binary bvxnor if needed.
References:
[0] http://smtlib.cs.uiowa.edu/theories-FixedSizeBitVectors.shtml (bvand,
bvor, bvadd, bvmul)
[1] http://smtlib.cs.uiowa.edu/logics-all.shtml#QF_BV (bvxor, bvxnor)
|
|
|
|
parser. (#2874)
|
|
s
|
|
|
|
|
|
|
|
|
|
Is not required anymore since we don't use autotools anymore.
|
|
|
|
|
|
When parsing with `--strict-parsing`, we are checking whether the
operators that we encounter have been explicitly added to the
`d_logicOperators` set in the `Parser` class. We did not do that for the
indexed operator `(_ to_fp ...)` (which is represented by the kind
`FLOATINGPOINT_TO_FP_GENERIC`). This commit adds the operator.
|
|
|
|
The sources of all previous libraries are now added to libcvc4 and built as
libcvc4. This removes circular dependencies between libcvc4 and libexpr.
Further, we now only have one parser library and don't build additional
libraries for each language.
|
|
|
|
|
|
TODO: cvc4autoconfig.h
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Currently, there is code duplication for parsing constants in sygus grammars, e.g.:
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L1048
https://github.com/CVC4/CVC4/blob/master/src/parser/smt2/Smt2.g#L2304
This PR removes this duplication by introducing a new ANTLR grammar "termAtomic" in Smt2.g.
As a result of this PR, we now parse sygus grammars with any constant we otherwise parse. This addresses known issues where CVC4 rejects grammars with floating point constants.
It also removes some unnecessary code for converting builtin kinds to their total versions.
This is work towards #2197. We still do not support sygus grammars with non-trivial *composite* terms, such as applications of indexed function symbols.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This eliminates some hacks for dealing with Int/Real.
- Eliminates the use of "to_real" to cast decimals like "2.0" that happen to be Int. We now replace these by (/ 2 1) instead of (to_real 2), which has the advantage of being smt-lib compliant for all theories, including QF_LRA.
- Eliminates the use of a hack to use "type ascriptions" when returning values from a get-value command. Instead, we use division with 1 when necessary. This affects the output of a few regressions, but we remain smt-lib compliant.
- Addresses a bug with printing arbitrary type ascriptions for smt2 terms. This partially addresses #1852.
- Updates our printing of negative rationals to be (/ (- n) m) instead of (- (/ n m)), which is consistent with the smt lib standard for real values (http://smtlib.cs.uiowa.edu/theories-Reals.shtml).
|
|
|
|
|
|
The SMT2 parser by default passes a true expression to the CheckSatCommand,
which results in checkSatisfiability (in SmtEngine) to always do an internal
push. As a consequence, the work of each check-sat was reset even though no
user level push/pop happened.
|
|
|
|
|
|
|
|
* Fixes --hide-zero-stats (and really skips the 0 values)
* Removes the additional newline after each statistic
* Introduces theory::getStatsPrefix(TheoryId) to generate consistent
prefixes for statistics based on the theory id
(e.g., THEORY_BV -> "theory::bv").
|
|
Adds missing override keywords.
|
|
This adds support for check-sat-assuming. It further adds support for SmtEngine::query() over a
vector of Expressions, e.g., smtEngine->query({a, b}); checks the validity (of the current input
formula) under assumption (not (or a b)).
|
|
|