summaryrefslogtreecommitdiff
path: root/src
AgeCommit message (Collapse)Author
2021-09-29Add Sort.java to the java API (#6382)mudathirmahgoub
This adds Sort.java SortTest.java and cvc5_Sort.cpp to the java api.
2021-09-28Remove linking against RT (#7257)Gereon Kremer
This PR removes long obsolete cmake code that is only required when using a pre-2013 glibc.
2021-09-24Eliminate calls to Rewriter::rewrite from strings entailment checks (#7203)Andrew Reynolds
There are a few further circular references that prevent us from not passing Rewriter to the strings TheoryRewriter constructor, this can be cleaned in future PRs.
2021-09-23Generalize string enumerator for fixed length sequences (#7234)Andrew Reynolds
This adds a utility to get enumerators for fixed length constants of a given sequence type. This will be used to construct fixed length gaps in array models.
2021-09-23Eliminate Output macro in favor of simple Env functions (#7223)Gereon Kremer
This PR eliminates the Output macro together with the associated output stream (stored in a static variable). It is replaces by a set of simple utility functions of the Env class, and we instead use the output stream from options.base.out. To achieve this, a couple of quantifier classes are now derived from EnvObj.
2021-09-23[proofs[ Alethe: Fix Order of Arguments of addAletheStepFromOr (#7237)Lachnitt
Changes the order of the arguments of addAletheStepFromOr to be consistent with addAletheStep.
2021-09-23[proofs] Alethe: Translate THEORY_REWRITE (#7236)Lachnitt
Implementation of the translation of THEORY_REWRITE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-23[proofs] Alethe: Add Alethe Files to be Compiled (#7241)Lachnitt
Adds Alethe proof rule and option. Adds alethe_post_processor and alethe_proof_rule files to list of files to be compiled. During incorporating these changes errors occurred in the SCOPE rule that are also fixed in this PR.
2021-09-23Refactor check interface of nonlinear extension (#7235)Gereon Kremer
This PR does a first step for refactoring the main check interface of the nonlinear extension. It does not change anything yet, but merely moves code around.
2021-09-23More uses of EnvObj (#7230)Andrew Reynolds
2021-09-23[proofs] Alethe: Translate SCOPE rule (#7224)Lachnitt
Implementation of the translation of SCOPE rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-23Use `|` to print quoted strings in `set-info` command. (#7240)Abdalrhman Mohamed
This PR is a step towards enabling raw-benchmark for cvc5 regressions. cvc5 fails to reparse 57 regressions (in regress0) printed be raw-benchmark because they contain multi-line strings in set-info that we don't print between vertical bars right now. This PR fixes that bug and removes 2 commands (derived from set-info commands) that are not used by the parsers anymore.
2021-09-23Implement alpha equivalence proofs (#7066)Andrew Reynolds
This is a modified version of #6137 which accounts for extended rewriting between quantified formulas that are considered alpha equivalent. It also generalizes the proof rule ALPHA_EQUIV. Notice that if we were to make this rule more pedantic, we would check for variable shadowing during substitution, although this is not currently done.
2021-09-22Make cegqi subsolvers EnvObj (#7205)Andrew Reynolds
Makes a few places do multiplication for Rational directly instead of invoking the rewriter.
2021-09-22Remove CVC language support (#7219)Mathias Preiner
This commit removes the support for the CVC language and converts all *.cvc regression tests to SMT-LIBv2.
2021-09-22Towards standard usage of evaluator (#7189)Andrew Reynolds
This makes the evaluator accessible via EnvObj through the Rewriter. It furthermore removes Rewriter::rewrite from inside the evaluator itself. Construction of Evaluator utilities is now discouraged. The include dependencies were cleaned slightly in this PR, leading to more precise includes throughout. This is work towards having a configurable cardinality for strings, as well as eliminating SmtEngineScope.
2021-09-22Add extensionality option for strings disequalities (#7229)Andrew Reynolds
Towards the strings array solver. Extensionality for disequalities is disabled by default, but will be used when the strings array solver is enabled.
2021-09-22arrays: Use EnvObj::rewrite and EnvObj::options. (#7217)Aina Niemetz
This does not yet clean up the usage of Rewriter::rewrite in the arrays type enumerator yet. Will be cleaned up in a follow-up PR.
2021-09-22arrays: Move type enumerator implementation to .cpp. (#7216)Aina Niemetz
This further cleans up the class declaration in the header to comply with code style guidelines.
2021-09-22Eliminate arithmetic proof macros (#7226)Gereon Kremer
This PR eliminates some macros for arithmetic proofs, that only slightly simplified access to the produce-proofs option. Now that static access is deprecated, these checks needed to be implemented differently anyway.
2021-09-22Minimal fixing version for tuple update parsing (#7228)Andrew Reynolds
This takes the essential changes from #7218 so that the current ANTLR issues are avoided.
2021-09-21[Proofs] Alethe: Translate ASSUME rule (#7213)Lachnitt
Implementation of the translation of ASSUME rules into the Alethe calculus. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-21[proofs] Alethe: Implementation of AletheProofPostprocessCallback (#7212)Lachnitt
Implementation of addAletheStep and addAletheStepFromOr. Added stub for AletheProofPostprocessCallback update function that will be populated by subsequent PRs. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-20Fix handling of conversions between FP and reals (#7149)Andres Noetzli
Fixes #7056. Currently, we introduce a UF for conversions between FP numbers and reals. This is done as part of `ppRewrite()`. The problem is that terms sent to `ppRewrite()` are not fully preprocessed yet and the FP theory solver was storing terms that were not fully preprocessed in a map for later lookup. For the issue at hand, the conversion term contained an `ite`, which was later removed. As a result, the theory solver did not consider the term to be relevant when refining abstractions. This commit changes the handling of conversion functions to instead adding purification lemmas for conversion terms when they are registered. The purification lemmas are needed, because otherwise, we can't retrieve the model values for the term without the rewriter interferring.
2021-09-20Start python API Solver documentation (#7064)Alex Ozdemir
2021-09-20[proofs] Alethe: adds a node converterHaniel Barbosa
Currently the only transformation it applies is removing attributes from quantifiers. Others may be added later.
2021-09-20Add the LFSC proof post-processor (#7134)Andrew Reynolds
Includes the necessary conversions to LFSC for the core rules of the internal calculus.
2021-09-20TheoryModel: Use EnvObj::rewrite instead of Rewriter::rewrite. (#7215)Aina Niemetz
2021-09-20Add anchors to cmdline options (#7210)Gereon Kremer
This PR adds anchors to the auto-generates command line option documentation. This allows to link to specific options from other parts of the documentation.
2021-09-18Fix printer for datatype udpater (#7208)Andrew Reynolds
2021-09-18Refactor tag suggestion mechanism (#7199)Gereon Kremer
This refactors the internal tag suggestion mechanism to no longer rely on C-style char arrays, but use a C++ vector of strings instead.
2021-09-17Use a single `NodeManager` per thread (#7204)Andres Noetzli
This changes cvc5 to use a single `NodeManager` per thread (using `thread_local`). We have decided that this is more convenient because nodes between solvers in the same thread could be exchanged and that there isn't really an advantage of having multiple `NodeManager`s per thread. One wrinkle of this change is that `NodeManager::init()` must be called explicitly before the `NodeManager` can be used. This code can currently not be moved to the constructor of `NodeManager` because the code indirectly calls `NodeManager::currentNM()`, which leads to a loop because the `NodeManager` is created in `NodeManager::currentNM()`. Further refactoring is required to get rid of this restriction.
2021-09-17[proofs] Alethe: Added Proof Postprocessor to alethe_proof_processor (#7202)Lachnitt
Added proof postprocessor class to alethe_proof_processor header file. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-17[proofs] Alethe: Added Final Callback Function to alethe_proof_processor (#7200)Lachnitt
Added final callback class to alethe_proof_processor header file. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-17Replace write access to options by a local variable (#7207)Gereon Kremer
This PR replaces a write to the options object by a local variable in the simplex procedure base class. The write was used to temporarily lower a limit for a single simplex call.
2021-09-17Minor cleanup related to EnvObj (#7206)Gereon Kremer
This PR does a bit of cleanup in the nonlinear arithmetic code related to the usage of EnvObj.
2021-09-16Fix relevant domain for parametric operators (#7198)Andrew Reynolds
Fixes #6531. This issue also occurs when using `--full-saturate-quant` on facebook benchmarks that combine multiple sequence types. It does some cleanup on relevant domain in the process.
2021-09-15[proofs] Alethe: Added Callback Function to alethe_proof_processor (#7186)Lachnitt
Added alethe_proof_processor header file and introduced callback class. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-15Minor changes to E-matching utilities (#7062)Andrew Reynolds
2021-09-15remove options that are no longer used (#7197)Gereon Kremer
This PR removes a handful of options that are no longer used anywhere.
2021-09-15[proof] Added printer for proof rule names (#7185)Lachnitt
Implementation file for Alethe proof rules.
2021-09-15[proof] Alethe proof rules (#7180)Lachnitt
Adds header for Alethe proof rules Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-09-15Eliminate global access to options:: from quantifiers rewriter (#7192)Andrew Reynolds
2021-09-14Add get-difficulty to the API (#7194)Andrew Reynolds
Adds smt2 parsing, printing and API support for get-difficulty. Adds unit tests.
2021-09-14Final cleanup (#7193)Gereon Kremer
This PR does some final cleanup on the options generation code.
2021-09-14Make `-o raw-benchmark` work with `--parse-only` (#7195)Andres Noetzli
Before, cvc5 was returning with --parse-only before the code could reach the code responsible for dumping the raw benchmark. This moves the check for --parse-only to the appropriate place and updates the run_regression.py script to use --parse-only.
2021-09-14Support sygus version 2.1 command assume (#7081)Andrew Reynolds
Adds support for global assumptions in sygus files. Also guards against cases of declare-const, which should be prohibited in sygus.
2021-09-14Utilities in preparation for print benchmark utility (#7190)Andrew Reynolds
This adds a few utilities in preparation for the print benchmark utility, which will replace our own dumping infrastructure.
2021-09-14Add proof manager method to translate difficulty map (#7159)Andrew Reynolds
This method will be called from SmtEngine in the implementation for (get-difficulty).
2021-09-14Refactor code generation for option modules (#7182)Gereon Kremer
This PR refactors the code generation for options/<module>_options.(h|cpp).
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback