summaryrefslogtreecommitdiff
path: root/src/printer/cvc
AgeCommit message (Collapse)Author
2020-03-18Move node visitor class from smt_util/ to expr/ (#4110)Alex Ozdemir
Done by: Running rg 'smt_util/node_visitor' -l | xargs sed -i 's/smt_util\/node_visitor/expr\/node_visitor/' in src to change the #includes Moving the file Changing src/expr/CMakeLists.txt and src/CMakeLists.txt clang-format, omitting node_visitor.h. In reference to discussion, here.
2020-03-07Explicit end marker for models printed in the CVC language (#3934)Ying Sheng
Fixes https://github.com/CVC4/cvc4-wishues/issues/9. When communicating with CVC4 using pipes and the CVC language, it was not possible to determine when all the lines of a model have been printed. This change adds begin and end markers as the example below: ``` MODEL BEGIN x : INT = -3; y : INT = 0; z : INT = 0; MODEL END; ```
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-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-27Fix -Wshadow warnings in common headers (#3826)Andres Noetzli
2020-02-20Remove front-end support for Chain (#3767)Andrew Reynolds
2019-12-16Move Datatype management to ExprManager (#3568)Andrew Reynolds
This is further work towards decoupling the Expr layer from the Node layer. This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType. As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.
2019-12-13Eliminate Expr-level calls in TypeNode (#3562)Andrew Reynolds
2019-10-30Unify CVC4_CHECK/CVC4_DCHECK/AlwaysAssert/Assert. (#3366)Mathias Preiner
2019-09-26CVC print support for recoverable failure (#3323)Andrew Reynolds
2019-04-29Eliminate APPLY kind (#2976)Andrew Reynolds
2019-04-24Do not use __ prefix for header guards. (#2974)Mathias Preiner
Fixes 2887.
2019-03-26Update copyright headers.Aina Niemetz
2019-01-22 Fix tuple and record CVC printing (#2818)Andrew Reynolds
2019-01-03[LRA proof] Recording & Printing LRA Proofs (#2758)Alex Ozdemir
* [LRA proof] Recording & Printing LRA Proofs Now we use the ArithProofRecorder to record and later print arithmetic proofs. If an LRA lemma can be proven by a single farkas proof, then that is done. Otherwise, we `trust` the lemma. I haven't **really** enabled LRA proofs yet, so `--check-proofs` still is a no-op for LRA. To test, do ``` lfsccvc4 <(./bin/cvc4 --dump-proofs ../test/regress/regress0/lemmas/mode_cntrl.induction.smt | tail -n +2) ``` where `lfsccvc4` is an alias invoking `lfscc` with all the necessary signatures. On my machine that is: ``` alias lfsccvc4="/home/aozdemir/repos/LFSC/build/src/lfscc \ /home/aozdemir/repos/CVC4/proofs/signatures/sat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/smt.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/lrat.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_base.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_bv_bitblast.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_arrays.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_int.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_quant.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf \ /home/aozdemir/repos/CVC4/proofs/signatures/th_real.plf" ``` * Added guards to proof recording Also reverted some small, unintentional changes. Also had to add printing for STRING_SUBSTR?? * Responding to Yoni's review * SimpleFarkasProof examples * Respond to Aina's comments * Reorder Constraint declarations * fix build * Moved friend declaration in Constraint * Trichotomy example * Lift getNumChildren invocation in PLUS case Credits to aina for spotting it. * Clang-format
2018-06-25Minor improvements in SMT2 and CVC printers (#2089)Andres Noetzli
This commit adds support for string concatenation, charat, and length operators in the CVC printer and support for re.nostr, re.allchar, and insert into a set in the SMT2 printer.
2018-06-25Updated copyright headers.Aina Niemetz
2018-06-25Remove parentheses for prefix ops without args (#2082)Andres Noetzli
In the CVC printer, function definitions without arguments are printed like constants but when actually using that function we were printing in the form of `x()`. For example: ``` (set-logic QF_BV) (define-fun x1480 () Bool true) (define-fun x2859 () Bool true) (define-fun x2387 () Bool x2859) (check-sat) ``` Was dumped as: ``` OPTION "incremental" false; OPTION "logic" "QF_BV"; x1480 : BOOLEAN = TRUE; x2859 : BOOLEAN = TRUE; x2387 : BOOLEAN = x2859(); ``` This commit removes these parentheses when prefix functions with zero arguments are printed, so the example above becomes: ``` OPTION "incremental" false; OPTION "logic" "QF_BV"; x1480 : BOOLEAN = TRUE; x2859 : BOOLEAN = TRUE; x2387 : BOOLEAN = x2859(); ```
2018-05-05Fix handling of TO_REAL in cvc printer (#1876)Andrew Reynolds
2018-05-04Remove special case for record selector printing. (#1875)Andrew Reynolds
2018-05-03Fix printing of multiple datatypes (#1872)Andres Noetzli
2018-05-02Fix cvc printer for nullary constructors (#1856)Andrew Reynolds
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-05Cleaning up the printing of theory model representative sets. (#1538)Tim King
2017-11-28Removing throw specifiers from internal Printer hierarchy. (#1393)Tim King
2017-10-27Refactor theory model (#1236)Andrew Reynolds
* Refactor theory model, working on making RepSet references const. * Encapsulation of members of rep set. * More documentation on rep set. * Swap names * Reference issues. * Minor * Minor * New clang format.
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-04-20Support for relational operators identity and join imagePaul Meng
2017-04-14Fix nullary operator printers, minor.ajreynol
2017-04-02Adding a model based axiom instantiation scheme for multiplication. Merge ↵Tim King
commit for nlAlgMaster.
2017-03-20fixed cvc4 parser for set complementPaul Meng
2017-03-07More fixes for printing/parsing sets, fix kind name.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.
2017-01-10Adding regression test scrubbing.Tim King
2016-12-07Added cardinality to cvc language, fixes bug 753. Throw logic exception when ↵ajreynol
using cardinality on sets with finite element type.
2016-11-22Fix smt2 and cvc printers for testers when output and input languages are ↵ajreynol
different.
2016-11-01Make tuple and record names unique. Do not print internal datatype ↵ajreynol
declaration in cvc printer.
2016-11-01Working memory leak free version, changes interface to pointers.ajreynol
2016-10-26New implementation of sets+cardinality. Merge Paul Meng's relation solver ↵ajreynol
as extension of sets solver, add regressions.
2016-10-13Revert "Merge branch 'origin' of https://github.com/CVC4/CVC4.git"Tim King
This reverts commit 3395c5c13cd61d98aec0d9806e3b9bc3d707968a, reversing changes made to 5f415d4585134612bc24e9a823289fee35541a01.
2016-08-24Merge remote-tracking branch 'origin/master'PaulMeng
2016-08-19Fixed two bugsClark Barrett
2016-04-20update from the masterPaulMeng
2016-04-15change transitive closure operator name to TCLOUSREPaulMeng
2016-04-09cardinality operation for finite sets (based on my thesis / ijcar16 paper)Kshitij Bansal
Some further cleanup/fixes pending This is squash of 39 commits (kbansal/card branch + cleanup): * add card operator * local reasoning * towards graph building * first implementation * close cardinality terms * model building * more * more * more * Add aggressive sets rewriting. * Recursively aggressive rewrite sets. * Fix * incomplete card2 implementation * ... * Avoid using auto in sets. * fix merge * more * ... * more * ... * Fixed for loops * Slight modification to computeRelevantTerms * more * .. * more * ... * mv empty set lemma generation to later point * more options/reordering * debug related * more trace * ... * fix merge_nodes, models * rm warnigns * fix compile errors * warning * bug fixes/cleanup * mroe fixes * cleanup * ...
2016-04-03Updating the copyright headers and scripts.Tim King
2016-02-15Merge remote-tracking branch 'origin/master'PaulMeng
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback