summaryrefslogtreecommitdiff
path: root/src/parser/cvc/Cvc.g
AgeCommit message (Collapse)Author
2020-05-21Update string kind names in new API (#4509)Andrew Reynolds
To match the smt2 Unicode standard. The internal ones are left unchanged for now.
2020-05-19Renamed operator CHOICE to WITNESS (#4207)mudathirmahgoub
Renamed operator CHOICE to WITNESS, and removed it from the front end
2020-04-08Added CHOOSE operator for sets (#4211)mudathirmahgoub
This PR enables THEORY_UF by default for sets and adds the operator CHOOSE for sets which returns an element from a given set. The semantics is as follows: If a set A = {x}, then the term (choose A) is equivalent to the term x. If the set is empty, then (choose A) is an arbitrary value. If the set has cardinality > 1, then (choose A) will deterministically return an element in A.
2020-03-31Remove replay and use-theory options and idl (#4186)Andrew Reynolds
Towards disentangling Options / NodeManager / SmtEngine. This PR removes options --use-theory=NAME and --replay/--replay-log. Both of these options are highly complex, unused, and lead to complications when implementing the way options and our build system work. The first is motivated by making TheoryEngine use an "alternate" theory, which appears to e.g. make it so that TheoryIdl could entirely replace TheoryArith. I believe this is too heavy handed of a solution: there should a consistent TheoryArith class, and options should be used to enable/disable alternate modules within it. The second attempts to replay low level decisions from the SAT solver. It is documented as not working (in 1.0). I do not believe this is worth salvaging. It also removes the solver in src/theory/idl, which cannot be enabled after this commit.
2020-03-30Support indexed operators re.loop and re.^ (#4167)Andrew Reynolds
Towards support for the strings standard. This modifies our interface so that we accept the SMT-LIB standard versions of re.loop and re.^. This means re.loop no longer accepts 3 arguments but 1 (with 2 indices). This means we no longer accept re.loop with only a lower bound and no upper bound on the number of repetitions. Also fixes #4161.
2020-03-30Frontend support for the choice operator (#4175)mudathirmahgoub
Added the operator choice to Smt2.g and Cvc.g. Removed the unused parameter hasBoundVars from TheoryModel::getModelValue
2020-03-27Support unicode internal representation and escape sequences (#3852)Andrew Reynolds
Work towards support for the strings standard. This updates the string solver and parser such that: The internal representation of strings is vectors of code points, Generation of the previous internal representation of strings has been relegated to the type enumerator. This is the code that ensures that "A" is the first character chosen for values of strings in models, The previous ad-hoc escape sequence handling is moved from the String class to the parser. It will live there for at least one version of CVC4, until we no longer support non-smt-lib complaint escape sequences or non-printable characters in strings, Handle unicode escape sequences according to the SMT-LIB standard in String, Simplify a number of calls to String utility functions, since the conversion between the previous internal format and code points is now unnecessary, Fixed a bug in the handling of TO_CODE: it should be based on the alphabet cardinality, not the number of internal code points.
2020-03-12Convert most instances of dataypes in parsers to the new API (#4054)Andrew Reynolds
I am still accessing Expr-level Datatypes for the sygus v1/v2 parsers (within smt2). This will be addressed in two ways in the future: (1) The sygus v1 parser will be deleted, (2) The sygus v2 parser will be updated to use a "Grammar" object as an extension of the new API, which will hide all calls to the underlying datatype. (See https://github.com/abdoo8080/CVC4/tree/sygus-api). FYI @abdoo8080 . Note I've renamed "mkMutualDatatypeTypes" to "bindMutualDatatypeTypes" to be more accurate and follow the updated name conventions in the parser. The next step will be to handle parametric datatypes, which are not specifically addressed by this PR.
2020-03-09Clean up more uses of ExprManager in parsers (#3932)Andrew Reynolds
Towards parser migration. Beyond Datatypes, there are still a handful of calls to the ExprManager in the parsers. This eliminates a few missing cases from TPTP and also inlines the access of ExprManager in the places its used.
2020-03-06Simplify DatatypeDeclarationCommand command (#3928)Andrew Reynolds
The new API does not use inheritence for Sorts. The current DatatypeDeclarationCommand uses DatatypeType, which inherits from Type. This commit simplifies the class DatatypeType -> Type and updates the necessary code (e.g. in the printers). Notice we are not yet converting commands Type -> Sort here. It also makes the main call for constructing datatypes in the parser from DatatypeType -> api::Sort. This is in preparation for converting Expr-level Datatype to Term-level DatatypeDecl in the parsers.
2020-03-06Remove tester name from APIs (#3929)Andrew Reynolds
This removes the field "tester name" from the Expr-level and Term-level APIs. This field is an artifact of parsing and thus should be handled in the parsers. This refactor uncovered an issue in our regressions, namely our smt version >= 2.6 was not strictly complaint, since the symbol is-cons was being automatically defined for testers of constructors cons. This disables this behavior when strict mode is enabled. It updates the regressions with this issue. This is work towards parser migration.
2020-03-05Migrate a majority of the functionality in parsers to the new API (#3838)Andrew Reynolds
This PR migrates a majority of the functionality of the parsers (cvc, tptp, smt2/sygus) to the new API. The main omitted functionality not addressed in this PR is the datatypes. Largely, the Expr-level Datatype is still used throughout. Remaining tasks: Migrate the Datatypes to the new API in cvc/smt2. Eliminate the use of ExprManager::mkVar (with flags for DEFINED/GLOBAL). For the latter, I have made a utility function in Parser::mkVar that captures all calls to this function. Notice that the existing mkVar/mkBoundVar/mkDefinedFun have been renamed to the more fitting names bindVar/bindBoundVar/bindDefinedFun etc. Note: this PR contains no major code changes, each line of code should roughly correspond one-to-one with the changed version. This fixes CVC4/cvc4-projects#77, fixes CVC4/cvc4-projects#78, fixes CVC4/cvc4-projects#80, fixes CVC4/cvc4-projects#85.
2020-03-05Enable -Wshadow and fix warnings. (#3909)Mathias Preiner
Fixes all -Wshadow warnings and enables the -Wshadow compile flag globally. Co-authored-by: Clark Barrett <barrett@cs.stanford.edu> Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com> Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com> Co-authored-by: Alex Ozdemir <aozdemir@hmc.edu> Co-authored-by: makaimann <makaim@stanford.edu> Co-authored-by: yoni206 <yoni206@users.noreply.github.com> Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com> Co-authored-by: AleksandarZeljic <zeljic@stanford.edu> Co-authored-by: Caleb Donovick <cdonovick@users.noreply.github.com> Co-authored-by: Amalee <amaleewilson@gmail.com> Co-authored-by: Scott Kovach <dskovach@gmail.com> Co-authored-by: ntsis <nekuna@gmail.com>
2020-02-27Refactor operator applications in the parser (#3831)Andrew Reynolds
This PR refactors how a term is constructed based on information regarding an operator (ParseOp) and its arguments. It also makes a few miscellaneous fixes. This includes: Indexed ops are carried in ParseOp via api::Op not Expr, getKindForFunction is limited to "APPLY" kinds from the new API, The TPTP/SMT2 parsers rely on mkTermInternal for handling associativity. TPTP should use DIVISION not DIVISION_TOTAL. This is in preparation for parser migration. These are the essential behavioral changes required for using the new API for the majority of the parser.
2020-02-26Basic support for regular expression complement (#3437)Andrew Reynolds
Fixes #3408 . Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h
2020-02-26Refactor type ascriptions in the parser (#3825)Andrew Reynolds
Towards parser migration. This consolidates two blocks of code (cvc/smt2) that do type ascriptions to a utility function in the parser. It updates this function to use the new API. This code will be further refactored when the interface for parametric datatype constructors is further developed in the new API.
2020-02-26Minor cleaning of smt2 parser (#3823)Andrew Reynolds
Towards parser migration, will make the diff of the eventual conversion a bit smaller.
2019-12-23Initial support for string reverse (#3581)Andrew Reynolds
Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`). Also improves support in a few places for tolower/toupper.
2019-12-06Add ExprManager as argument to Datatype (#3535)Andrew Reynolds
2019-10-08[CVC Parser] Add support for regular expressions (#3346)Andres Noetzli
2019-09-06Remove SMT1 parser. (#3228)Mathias Preiner
This commit removes the SMT1 parser infrastructure and adds the SMT2 translations of the SMT1 regression tests. For now this commit removes regression test regress3/pp-regfile.smt since the SMT2 translation has a file size of 887M (vs. 172K for the SMT1 version). Fixes #2948 and fixes #1313.
2019-08-26Remove unnecessary code from Cvc.g (#3213)Andrew Reynolds
2019-08-10Simplify how defined functions are tracked during parsing (#3177)Andrew Reynolds
2019-03-28Fix issues in cvc parser (#2901)Andrew Reynolds
2019-03-26Update copyright headers.Aina Niemetz
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-06-25Updated copyright headers.Aina Niemetz
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-04-06Add define rec fun to cvc parser (#1738)Arjun Viswanathan
2018-04-02Remove references to nyu (#1721)Clark Barrett
2017-10-18Strings API escape sequences (#1245)Andrew Reynolds
* 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.
2017-10-03Op overload parser (#1162)Andrew Reynolds
* Update parser for operator overloading. * Improvements * Updates * Add assert
2017-09-14Remove unhandled subtypes (#1098)Andrew Reynolds
* Remove unhandled subtypes, which consequently makes typing rules uniformly stricter based on weakening the subtype relation. Ensure coercions in the smt2 and cvc parser for Real decimal constants whose type is Integer. Ensure type annotations are computed during preRewrite to ensure rewriting (which does not preserve types) does not impact term construction for parametric datatypes. This fixes issue #1048 (we now give an type exception). * Update unit test for parametric datatypes to reflect new subtyping relation. * Remove deprecated test. * Make array construction for lambdas work with new subtype relations to handle lambdas like (lambda ((x Int) (y Int)) (ite (= x 0) 0.5 0.0)).
2017-09-05Remove support for conversions between uint32/uint16 and string. (#1069)Andrew Reynolds
* Remove support for conversions between uint32/uint16 and string. * Temporarily disable regression.
2017-08-17Remove unused SubrangeBound(s) classes (#221)Andres Noetzli
As discussed in pull request #220, commit 360d6ee8d3cdd5ddb47c328043eaed3a107b8db1 mostly got rid of SubrangeBound(s). There were still a few mentions of it left in the code, most of them commented out. The occurrences in expr.i and expr_manager.i, however, created issues with the Python wrapper. This commit removes the SubrangeBound(s) implementation and other leftovers.
2017-07-29Add support for charat in native language, minor cleanup.ajreynol
2017-07-17Remove PtrCloser (#198)Andres Noetzli
With C++11, we don't need PtrCloser anymore because we can just use std::unique_ptr.
2017-07-12Make type rules more strict for operators whose type rules involve subtypes. ↵ajreynol
Disable support for subrange and predicate subtypes (which were only partially supported previously).
2017-07-10Merge datatype shared selectors/sygus comp 2017 branch. Modify the datatypes ↵ajreynol
decision procedure to share selectors of the same type across multiple constructors. Major rewrite of the SyGuS solver. Adds several new strategies for I/O example problems (PBE) and invariant synthesis. Major simplifications to sygus parsing and synthesis conjecture representation. Do not support check-synth in portfolio. Add sygus regressions.
2017-07-07Update copyright headers.Mathias Preiner
2017-07-07Use new copyright header format.Mathias Preiner
2017-04-20Support for relational operators identity and join imagePaul Meng
2017-04-12Add nullary operator metakind.ajreynol
2017-03-20fixed cvc4 parser for set complementPaul Meng
2017-03-16Parsing support for SMT LIB 2.6. Minor fixes for printing datatypes. Fix for ↵ajreynol
mkGroundTerm for parametric datatypes. Minor change to run_regression to allow regressions to override input language. Minor refactoring to Cvc.g.
2017-03-07More fixes for printing/parsing sets, fix kind name.ajreynol
2017-03-07Fix cvc parser for set compliment.ajreynol
2017-03-06Support for set compliment and universe set. Simplify approach for sep.nil ↵ajreynol
nodes.
2017-03-02Eliminate Boolean term conversion. Generalizes removeITE pass to remove ↵ajreynol
Boolean terms, treats distinguished BOOLEAN_TERM_VARIABLE kind as theory literal. Fixes bugs 597, 604, 651, 652, 691, 694. Add regressions.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback