Age | Commit message (Collapse) | Author |
|
|
|
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)).
|
|
|
|
Also adds parsing support for PI in smt2 with syntax "real.pi".
|
|
|
|
|
|
|
|
|
|
|
|
|
|
This commit fixes two issues with reset-assertions:
- pending pops were not done in SmtEngine, resulting in the following
assertion failure:
d_userLevels.size() == 0 && d_userContext->getLevel() == 1
- all definitions were erased on reset-assertion in an SMT2 file,
leading to errors about undefined types
|
|
|
|
|
|
|
|
|
|
* Make higher-order a flag in logic info.
* Format
* Minor
* Format
|
|
* Represent sygus synthesis conjectures using higher-order quantification, remove associated hacks.
* Minor fix
* Fix bug in Node::hasBoundVar for non-ground operators.
* Add regression.
* Address review.
* Apply clang format.
|
|
* Argument for strings class to specify whether to process escape sequences.
* Change default value on string constructor.
* Make CVC4::String::toString symmetric to the constructor for CVC4::String, document.
* Clang format.
|
|
* Allow any smt2 logic to be a sygus logic. Add non-linear SyGuS regressions.
* Minor
* Add case for reals, comment.
* Fix regress1.
|
|
* Move unsat core names to SmtEnginePrivate. Adds a SetExpressionNameCommand to do this. Removes the names field from GetUnsatCoreCommand.
* Comment
* Pass expression names by reference.
* Update throw specifiers.
* Minor
* Switch expression names to CDMap, simplify interface for printing unsat core names.
* Revert throw specifier change.
* Minor simplifcations
|
|
* Move equality query to own file, move equality inference to quantifiers engine.
* Move quantifiers attributes out of TermDb and into QuantAttribute.
* Move term database sygus to quantifiers engine, move some attributes to quantifiers attributes header.
* Split term database into term util.
* Partial fix for #1205 that eliminates need for dependency in node.cpp.
* Add more references to github issues.
|