summaryrefslogtreecommitdiff
path: root/src/printer
AgeCommit message (Collapse)Author
2021-04-01Rename namespace CVC5 to cvc5. (#6258)Aina Niemetz
2021-03-31Rename namespace CVC4 to CVC5. (#6249)Aina Niemetz
2021-03-30Fix printing for double patterns (#6235)Andrew Reynolds
2021-03-30Make SEXPR simply typed (#6160)Andrew Reynolds
Currently, SEXPR applications are given a parametric type SEXPR_TYPE applied to the types of its arguments. This means that SEXPR that are type checked consume roughly double the memory. This issue arises in practice when printing proofs in the internal calculus. There is no need to have SEXPR_TYPE as a parametric type, this PR makes SEXPR simply typed. Also moves some implementation of TypeNode methods to type_node.cpp.
2021-03-25FP: Refactor FloatingPointLiteral in preparation for MPFR. (#6206)Aina Niemetz
This pushes all symfpu specific parts from FloatingPoint into FloatingPointLiteral. FloatingPoint is now generic. An additional FloatingPointLiteral implementation using MPFR will be made configurable similiarly to how we handle Integers with either GMP or CLN backend.
2021-03-18Eliminate more uses of SExpr. (#6149)Abdalrhman Mohamed
This PR eliminates all remaining uses of SExpr outside of statistics.
2021-03-15Letify quantifier bodies independently (#6112)Andrew Reynolds
This fixes a subtle bug with how quantifier bodies are letified. It makes our letification more conservative so that let symbols are never pushed inside quantifier bodies, instead quantifier bodies are letified independently of the context.
2021-03-11Delete Expr layer. (#6117)Aina Niemetz
2021-03-09Some more cleanup of includes (#6083)Gereon Kremer
This PR does some more cleanup of the includes.
2021-03-09Update copyright headers to 2021. (#6081)Aina Niemetz
2021-03-05Remove partial UDIV/UREM operators. (#6069)Mathias Preiner
This commit removes the partial UDIV/UREM operator handling. BITVECTOR_UDIV and BITVECTOR_UREM are now total.
2021-03-06Remove SMT-LIB 2.5 and 2.0 support. (#6068)Mathias Preiner
This commit removes parser and printer support for old SMT-LIB standards and also converts all regression tests to 2.6.
2021-03-03More cleanup of includes to reduce compilation times (#6037)Gereon Kremer
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
2021-03-03Remove uses of SExpr class. (#6035)Abdalrhman Mohamed
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
2021-03-03Add tuple projection operator (#5904)mudathirmahgoub
This PR adds tuple projection operator to the theory of data types. It Also adds helper functions for selecting elements from a tuple.
2021-03-02Clean up includes to reduce compile times (#6031)Gereon Kremer
This PR cleans up a ton of includes, based on the suggestions of iwyu. Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
2021-02-26Minor improvement and fix to smt2 printer (#6009)Andrew Reynolds
This permits access to the static method string smtKindString(Kind k, Variant v) which is required for LFSC proof conversion. It also makes a fix to how a string kind is printed.
2021-02-22(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949)Gereon Kremer
This PR introduces a new arithmetic kind for indexed root predicates. An indexed root predicate compares a real variable to the k'th root of a given polynomial as follows: Let IRP_k(x ~ 0, p) an indexed root predicate with k a non-negative number, x some real variable, ~ an arithmetic relation (e.g. =, <, ...), and p a polynomial over x (and possibly other variables). If p contains variables apart from x, we can only evaluate the expression over a suitable assignment for at least these variables. The evaluation of this expression is equivalent to computing the k'th real root of p in x (with all other variables evaluated over a given assignment) and comparing this real root to zero (according to the relation symbol ~). Note that we currently do not intend to use this structure for solving, but require it for representing and printing CAD proofs.
2021-02-08Use quantifiers inference manager for lemma management (#5867)Andrew Reynolds
Towards eliminating dependencies on quantifiers engine. This replaces the custom implementation of lemma management in quantifiers engine with the standard one. It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers. Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
2021-01-24(proof-new) Instantiation list utility (#5768)Andrew Reynolds
This is in preparation for refactoring the printing of instantiations. We will migrate the printing of instantiations (currently done in the Instantiate module within quantifiers engine) to somewhere more high level e.g. the SmtEngine or in the command layer. This will make the infrastructure for dumping instantiations much more flexible, as implemented on proof-new.
2021-01-11Further simplifications in preparation for removing Expr layer (#5756)Andrew Reynolds
This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager. These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly. This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.
2021-01-08Add bags inference generator (#5731)mudathirmahgoub
This PR adds inference generator for basic bag rules.
2021-01-05Remove a few miscellaneous references to the expr layer (#5661)Andrew Reynolds
Leftover from a development branch.
2020-12-16Simplify synth-fun printer (#5682)Andrew Reynolds
Simplifies synth-fun printing to assume that the function-to-synthesize should be printed with the proper name and return type.
2020-12-15Improvements related to quantifiers printing (#5678)Andrew Reynolds
Also fixes a bug where patterns would be printed with the wrong scope (that included the bound variable list).
2020-12-08Fix a bug with synth-fun printer (#5512)Abdalrhman Mohamed
This PR fixes #5448. SynthFunCommand::toStream used to call d_grammar->resolve even when d_grammar is a nullptr. This PR fixes the issue and modifies the signature of Printer::toStreamCmdSynthFun to make it clear that grammar is an optional argument.
2020-12-03Models as (#5581)yoni206
This PR relates to #4987 . Our plan is to: delete the model keyword (done in #5415 ) avoid printing extra declarations by default (done in #5432 ) wrap UF values with as expressions. This PR does step 3, fixes a regression accordingly, and adds the formula from #4987 and a variant of it to the regressions.
2020-12-02Update copyright headers.Aina Niemetz
2020-12-02Remove dagification visitor (#5574)Andrew Reynolds
This has fully been replaced by the new let binding.
2020-12-02Use new let binding for cvc printer (#5561)Andrew Reynolds
Also changes names slightly to avoid accidental uses of toStream, which can lead to infinite loops if the wrong version is used.
2020-11-30Use new let binding in AST printer (#5529)Andrew Reynolds
Required for removing the old DagificationVisitor
2020-11-25Use symbol manager for printing responses get-model (#5516)Andrew Reynolds
This makes symbol manager be in charge of determining which sorts and terms to print in response to get-model. This eliminates the need for the parser to call ExprManager::mkVar (and similar methods) with custom flags. This requires significant simplifications to the printers for models, where instead of a NodeCommand, we take a Sort or Term to print in the model. This is one of the last remaining steps for migrating the parser to the new API. The next step will be to remove a lot of the internal infrastructure for managing expression names, commands to print in models, node commands, node listeners, etc.
2020-11-24Allow printing of null node in let binder (#5523)Andrew Reynolds
2020-11-20RoundingMode: Rename enum values to conform to code style guidelines. (#5494)Aina Niemetz
2020-11-19Use new let binding utility in smt2 printer (#5472)Andrew Reynolds
Also fixes some whitespace issues in printing quantified formulas.
2020-11-19Use symbol manager for unsat cores (#5468)Andrew Reynolds
This PR uses the symbol manager for handling names for unsat cores. This replaces interfaces in SmtEngine for managing expression names. It removes the SetExpressionName command.
2020-11-18Add let binding utility (#5444)Andrew Reynolds
This utility will replace the dagification visitor for printing lets for Node in the smt2 printer, and will be used further in e.g. LFSC proof printing.
2020-11-18Use symbol manager for get assignment (#5451)Andrew Reynolds
This replaces the previous methods for get-assignment which involving making a DefinedNamedFunctIonCommand and storing the expression names map in the SmtEngine. Note: we now limit :named terms to those not beneath quantifiers and let-bindings.
2020-11-17FloatingPoint: Clean up and document header, format. (#5453)Aina Niemetz
This cleans up the src/util/floatingpoint.h.in header to conform to the code style guidelines of CVC4. This further attempts to fully document the header. The main changes (except for added documentation) are renames of member variables, getting rid of the redundant functions FloatingPointSize::exponent() and FloatingPointSize::significand(), and a more explicit naming of CVC4 wrapper types vs symFPU trait types. Else, it's mainly reordering and formatting.
2020-11-13Model declarations printing options (#5432)yoni206
This PR relates to #4987 . Our plan is to: delete the model keyword avoid printing extra declarations by default wrap UF values with as expressions. This PR is step 2. It allows the user to choose the model printing style in case of uninterpreted elements: either using datatypes, or using declare-sorts and declare-funs or just using declare-funs. The default option, which is closest to the standard, is just using declare-funs. In step 3, these will be replaced by abstract values using as.
2020-11-12Models standard (#5415)yoni206
This PR relates to #4987 . Our plan is to: delete the model keyword avoid printing extra declarations by default wrap UF values with as expressions. This PR does step 1, and fixes regressions accordingly.
2020-11-10Add proper support for the declare-heap command for separation logic (#5405)Andrew Reynolds
This adds proper support for the (declare-heap (T U)) command, which declares the type of the heap in separation logic. This command is part of the standard for separation logic. This previous was handled in an ad-hoc way where the type of the heap would be inferred on demand. This was a poor solution and has led to a number of issues related to when the heap is inferred. Fixes #5343, fixes #4926. Work towards CVC4/cvc4-wishues#22.
2020-11-09Simplify handling of subtypes in smt2 printer (#5401)Andrew Reynolds
This makes major simplifications to how subtypes are enforced in the smt2 printer. It is now the principle that the smt2 prints things faithfully to the AST, regardless of whether it conforms to the smt2 standard. It also fixes the current smt2 printing of to_real. Conversely, this removes a hack from GetValueCommand which forced casting via x -> (/ x 1). This is now properly handled in Solver::getValue. Some regressions change expected output as a result. Notice that internally generated Node may not conform to the smt2 standard, but user-level terms will.
2020-11-05Simplify printing with respect to expression types (#5394)Andrew Reynolds
This removes infrastructure for stream property related to printing type annotations on all variables. This is towards refactoring the printers.
2020-11-03Add support for printing `re.loop` and `re.^` (#5392)Andres Noetzli
In the new SMT-LIB string standard, re.loop and re.^ are indexed operators but the printer was not updated to print them correctly. This commit adds support for printing re.loop and re.^.
2020-10-29Update api::Sort to use TypeNode instead of Type (#5363)Andrew Reynolds
This is work towards removing the old API. This makes TypeNode the backend for Sort instead of Type. It also updates a unit test for methods isUninterpretedSortParameterized and getUninterpretedSortParamSorts whose implementation was previously buggy due to the implementation of Type-level SortType.
2020-10-29Add mkInteger to the API (#5274)mudathirmahgoub
This PR adds mkInteger to the API and update mkReal to ensure that the returned term has real sort. The parsers are modified to parse numbers like "0" "5" as integers and "0.0" and "15.0" as reals. This means subtyping is effectively eliminated from all theories except arithmetic. Other changes: Term::isValue is removed which was introduced to support parsing for constant arrays. It is no longer needed after this PR. Benchmarks are updated to match the changes in the parsers Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu
2020-10-28Remove more uses of Expr (#5357)Andrew Reynolds
This PR removes more uses of Expr, mostly related to UnsatCore. It makes UnsatCore a cvc4_private object storing Node instead of Expr.
2020-10-20Remove some Commands from the API. (#5268)Abdalrhman Mohamed
This PR removes Solver::getAssignment command from the API as there is no way to assign names to terms in the API. It also removes ExpandDefinitionsCommand, an internal functionality in CVC4.
2020-10-16Refactor SMT-level model object (#5277)Andrew Reynolds
This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary. Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only. This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback