summaryrefslogtreecommitdiff
path: root/src/parser/smt2
AgeCommit message (Collapse)Author
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-25New C++ API: Clean up API: mkVar vs mkConst vs mkBoundVar. (#2977)Aina Niemetz
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).
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-04-16Make bv{add,mul,and,or,xor,xnor} left-associative (#2955)Andres Noetzli
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)
2019-03-26Update copyright headers.Aina Niemetz
2019-03-19Make declare-datatype(s) a standard, non-extended command in the Smt2 ↵Andrew Reynolds
parser. (#2874)
2019-03-18New C++: Remove redundant mkVar function.Aina Niemetz
s
2019-01-10New C++ API: Get rid of mkConst functions (simplify API). (#2783)Aina Niemetz
2019-01-03API/Smt2 parser: refactor termAtomic (#2674)Andres Noetzli
2018-11-27Reduce lookahead when parsing string literals (#2721)Andres Noetzli
2018-11-21Support string replace all (#2704)Andrew Reynolds
2018-10-20Remove antlr_undefines.h. (#2664)Mathias Preiner
Is not required anymore since we don't use autotools anymore.
2018-10-19Remove autotools build system. (#2639)Mathias Preiner
2018-10-18Introducing internal commands for SyGuS commands (#2627)Haniel Barbosa
2018-10-02Allow (_ to_fp ...) in strict parsing mode (#2566)Andres Noetzli
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.
2018-09-26Makes SyGuS parsing more robust in invariant problems (#2509)Haniel Barbosa
2018-09-22cmake: Only build libcvc4 and libcvc4parser as libraries.Mathias Preiner
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.
2018-09-22cmake: Move find_package to where it is actually needed.Mathias Preiner
2018-09-22cmake: Cleanup CMakeLists.txt files, remove SHARED.Mathias Preiner
2018-09-22cmake: Working build infrastructure.Mathias Preiner
TODO: cvc4autoconfig.h
2018-09-22cmake: Antlr parser generation done.Mathias Preiner
2018-09-22cmake: Added initial build infrastructure.Aina Niemetz
2018-08-27Make division chainable in the smt2 parser (#2367)Andrew Reynolds
2018-08-21 Fix processing of nested Variable construct in sygus let bodies (#2351)Andrew Reynolds
2018-08-21Warn and enable quantifiers when using sygus + logics with QF (#2352)Andrew Reynolds
2018-08-20 Remove support for prototype (non-sygus) synthesis (#2338)Andrew Reynolds
2018-08-17Split sygus grammar to its own ANTLR grammar (#2307)Andrew Reynolds
2018-08-08Plug solver API object into parser. (#2240)Aina Niemetz
2018-08-07Simplify and improve the sygus parser (#2266)Andrew Reynolds
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.
2018-08-06Add RegLan to smt2/sygus parsers. (#2276)Andrew Reynolds
2018-08-06Remove support for Enum sygus syntax. (#2264)Andrew Reynolds
2018-08-02Parse standard separation logic inputs (#2257)Andrew Reynolds
2018-08-01Fix issues with printing parametric datatypes in smt2 (#2213)Andrew Reynolds
2018-07-14sygusComp2018: update semantics for declare-fun in sygus. (#2102)Andrew Reynolds
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-04Only enable transcendentals if logic is N[I]RAT (#2052)Andres Noetzli
2018-05-29 Make user's SMT2 version override file version (#2004)Andres Noetzli
2018-05-29Track input language in a single place (#2003)Andres Noetzli
2018-05-22Parse error for sygus grammar term with multiple let bodies (#1961)Andrew Reynolds
2018-05-21Improvements in parsing and printing related to mixed int/real (#1879)Andrew Reynolds
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).
2018-05-08Support for str.<= and str.< (#1882)Andrew Reynolds
2018-05-07Add support for str.code (#1821)Andrew Reynolds
2018-05-03Fix redundant internalPush calls. (#1865)Mathias Preiner
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.
2018-05-02Initial support for string standard in smt lib 2.6 (#1848)Andrew Reynolds
2018-04-08Check free variables in assertions (#1737)Andrew Reynolds
2018-03-09Add support for SMT-LIB v2.5 command get-unsat-assumptions (#1653)Aina Niemetz
2018-03-06Make statistics output consistent. (#1647)Mathias Preiner
* 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").
2018-03-05Enable -Wsuggest-override by default. (#1643)Mathias Preiner
Adds missing override keywords.
2018-03-05Add support for check-sat-assuming. (#1637)Aina Niemetz
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)).
2018-02-27Remove unused code in pushDefineFunRecScop in smt2.cpp. (#1627)Aina Niemetz
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback