summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2021-11-30Generalize eager length bound conflicts for regular expression memberships ↵Andrew Reynolds
(#7633) This generalizes eager length bound conflicts to take into account regular expression memberships. For example: If `(str.in_re x (re.++ (re.* re.allchar) (str.to_re "abc") (re.* re.allchar))` is asserted, then we know `(str.len x) >= 3`. If e.g. equivalence class of `x` is merged with `(str.substr y 0 2)`, we get the conflict `(and (str.in_re x (re.++ (re.* re.allchar) (str.to_re "abc") (re.* re.allchar)) (= x (str.substr y 0 2))` since `(str.len (str.substr y 0 2)) <= 2`. This also does some minor refactoring to eager prefix conflicts to make it more analogous to our implementation of length conflicts.
2021-11-30Proper check for first-class types in datatype subfields (#7712)Andrew Reynolds
Fixes two issues with our check for datatype subfields (isFunctionLike -> isFirstClass): functions should be allowed, RegLan should not. Fixes cvc5/cvc5-projects#368. That issue now throws an error: (error "Parse Error: proj-368.smt2:3.39: cannot use fields in datatypes that are not first class types (declare-datatype x ((_x (x8 RegLan)))) ^ ") This adds a regression showing we allow functions as subfields.
2021-11-30Alethe: Further Printer Implementation (#7675)Lachnitt
Adds implementation of PrintInternal a function to print a proof node after the first step has been printed. Should be merged after PR #7674. Co-authored-by: Haniel Barbosa hanielbbarbosa@gmail.com
2021-11-30[proofs] Alethe: Implementation of Printer (#7674)Lachnitt
Adds an implementation file of the Alethe printer with function stubs to be filled in in further PRs. Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-11-30Remove now unused dumping infrastructure (#7703)Gereon Kremer
This PR removes the old dumping infrastructure. All dumping has already been migrated to -o.
2021-11-30[proofs] Alethe: Printer Specification (#7673)Lachnitt
Header of the Alethe printer Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
2021-11-29Fix minor issues (#7704)Gereon Kremer
This fixes a few minor coverity issues.
2021-11-29Start post-release for 0.0.4Mathias Preiner
2021-11-29Bump version to 0.0.4Mathias Preiner
2021-11-29Bug in printing parameter list in define_fun_to_string (#7700)Sujit Kumar Muduli
Signed-off-by: Sujit Muduli <smuduli@cse.iitk.ac.in>
2021-11-25Consolidate CI jobs (#7697)Gereon Kremer
This PR integrates the cancel and update-pr jobs into the main CI jobs. This not only looks nicer in the actions menu (less jobs) but also improves which jobs we cancel: this now also allows to cancel jobs in forks by getting rid of the magic workflow number.
2021-11-25Guard regression tests that require libpoly to pass. (#7698)Mathias Preiner
Regression tests either timeout or return unknown if cvc5 is configured with --no-poly.
2021-11-25api: Refactor mkTerm for kinds with arity = 0. (#7699)Aina Niemetz
This refactors mkTerm to allow creation of terms of kinds with arity = 0 via Op and/or empty children vector.
2021-11-24examples: Update python api datatypes example. (#7692)Aina Niemetz
The C++ datatypes example was extended in #7689. This updates the Python API datatypes example accordingly.
2021-11-24Always enable API black box unit tests (#7696)Andres Noetzli
Currently, when assertions are disabled, we do not enable any unit tests. However, we have decided that it would be beneficial to do black box unit testing of the API even when building cvc5 without assertions, because the API is user facing. This commit makes the following changes: - Always enables API black box unit tests - Adds a test to check whether a buggy version of Clang is being used, which prevents the use of `-fno-access-control` for white box tests - Fixes a spooky variable name in a Python unit test
2021-11-24cmake: Add option --[no]-static-binary. (#7695)Mathias Preiner
Allows to disable linking against static system libraries explicitly.
2021-11-24Fix ANTLR3 config for i386 and aarch64 builds. (#7694)Mathias Preiner
This fixes the i386 and aarch64 nightly builds.
2021-11-24examples: Update Java datatypes example with recent extensions. (#7693)Aina Niemetz
The C++ datatypes example was extended in #7689. This updates the Java API datatypes example accordingly.
2021-11-24Remove dependency of `TypeNode` on `Node` (#7690)Andres Noetzli
This is further work towards breaking cyclic dependencies in the `expr` folder.
2021-11-24Fix potential for cycles in trust substitutions (#7687)Andrew Reynolds
This ensures we use only the prefix of substitutions for the *first* time a formula is proven in a substitution map. This avoids the possibility for cycles in proof generators during non-clausal simplification, where we may reprove a formula F later at a point where later substitutions depend on F.
2021-11-24examples: Extend DT api example with APPLY_TESTER and APPLY_UPDATER ↵Aina Niemetz
application. (#7689)
2021-11-24Minor fixes (#7691)Andres Noetzli
2021-11-24api: Fix creation of nary term kinds via Op. (#7688)Aina Niemetz
Fixes cvc5/cvc5-projects#367.
2021-11-23Make difficulty manager only consider lemmas at full effort (#7685)Andrew Reynolds
Fixes cvc5/cvc5-projects#350
2021-11-23Enable model-based reduction technique for strings (#7680)Andrew Reynolds
This changes our default strategy for deferring (some) reductions until after the model is constructed. It introduces the option `--strings-mbr` (model-based reduction) which is enabled by default. When using model-based reductions, only *negatIve* contains and negative memberships are deferred for reduction/unfolding until LAST_CALL effort, where a candidate model is available. These steps are performed only if the constraints are not already satisfied in the model. The intuition is that negative contains/membership are the *most* expensive constraints to process and are moreover the *least* likely to be false in the model. It makes a few fixes to the extended/RE solvers: - 2 kinds of inferences in `checkExtfEval` should not be performed for substitutions based on models - The regular expression solver should not use inclusion tests to justify reduction of memberships when the basis for the reduction is an unfolded membership, due to the reasoning being potentially cyclic. This led to a bogus model on a regression when the new strategy was enabled. It also does minor refactoring of those solvers that was required for implementing the new policy. This branch is +446-1 on SMT-LIB, with all gains coming on "sat" benchmarks, mostly from pyex. It also solves 2 previously unsolved challenge Amazon benchmarks quickly.
2021-11-23Add kinds to python docs (#7672)Gereon Kremer
This PR adds the kinds to the documentation for the regular python docs.
2021-11-23Push output language inside the printing code (#7683)Gereon Kremer
This PR pushes the explicit specification of the output language further inside the printing methods. The general way to specify the output language is to attach it to the output stream. The changes simplify the interface, while we still allow printing in another output language via using a scope (as used in the lfsc and tptp printers).
2021-11-23Add rewrite rule for bag.card operator using bag.map and lambda (#7643)mudathirmahgoub
Add rewrite rule for bag.card operator using bag.map and lambda
2021-11-23Python API documentation: terms (#7659)yoni206
This PR adds documentation for the Terms class in the python API. Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de
2021-11-23Make `node_value.h` not depend on `node_manager.h` (#7676)Andres Noetzli
This commit breaks a circular dependency by making `node_value.h` not depend on `node_manager.h`. As a result, we can remove the hack-y include of `node_manager.h` in the middle of the `node_value.h` file.
2021-11-22Refactor IO stream manipulators (#7555)Gereon Kremer
This PR consolidates SetLanguage, ExprSetDepth and ExprDag into a single consistent utility. Also, it makes it play more nicely with users setting these options and removes some obsolete code.
2021-11-22Add rewrite for repeated re.allchar (#7681)Andrew Reynolds
This solves 4 more challenge Amazon benchmarks.
2021-11-22Set proper system processor for arm64 toolchain (#7665)Gereon Kremer
2021-11-22[prop] Remove unused #define in theory proxy (#7670)Haniel Barbosa
2021-11-22Improve error for check theory assertions with model (#7679)Andrew Reynolds
Makes it so that we report *all* unsatisfied assertions, not just the first one.
2021-11-21Fix const RE test for internal regexp rv kind (#7678)Andrew Reynolds
Fixes #7677.
2021-11-20bv2int module: translation of more cases (#7653)yoni206
This commit adds the implementation of the translation from BV to Int for the remaining operators. Some cases are left for the next PR. Corresponding unit tests are added. Notice that in the new module, the following issues do not occur. They will be added as tests in the following PRs: https://github.com/cvc5/cvc5-projects/issues/345 https://github.com/cvc5/cvc5-projects/issues/344 https://github.com/cvc5/cvc5-projects/issues/343
2021-11-19[API] Avoid copying values (#7666)Andres Noetzli
2021-11-19Clean up relationship of metakind and node_manager (#7649)Andres Noetzli
Before this commit, we were including `metakind.h` twice in `node_manager.h`, once without and once with defining `CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP`. Additionally, `mkmetakind` generated structs that mapped types to kinds. This commit makes all of this obsolete by directly generating instantiations of `mkConst`, which allows us to get rid of the double include and the `ConstantMap`.
2021-11-19Remove n-ary builder (#7671)Andrew Reynolds
Adds the only usage of this file into ite_simp.cpp, where it is specialized for AND. This is work towards eliminating arithmetic subtyping (that utility had an unused and ambiguous use of mkConst(CONST_RATIONAL, ...)).
2021-11-19Allow negative denominator for CLN Rationals constructed from string. (#7667)Mathias Preiner
2021-11-18api: Fix categorization of DT kinds in kind maps. (#7668)Aina Niemetz
2021-11-18Refactor CAD option for linear model seed (#7657)Gereon Kremer
This PR implements another strategy for using the linear model in the CAD-based nonlinear solver. It stays disabled by default.
2021-11-18[proofs] Fix trace in SatProofManager (#7664)Haniel Barbosa
2021-11-18[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)Lachnitt
In the Alethe specification the DUPLICATED_LITERALS rule was renamed to CONTRACTION. This PR renames the rule to be consistent with the standard.
2021-11-18api: Fix kind documentation for BAG_MAKE. (#7663)Aina Niemetz
2021-11-17Improve naming in term canonization when handling HO variables (#7660)Haniel Barbosa
Previously all higher-order variables would me named with "-" followed by the index, since the method did not account for functional types (which are printed as with (-> ...)). This commit changes it so that it takes the return type, which will always be atomic, thus giving more meaningful names to the canonical variables.
2021-11-17[sat] Fix indentation in "reason" (#7662)Haniel Barbosa
2021-11-17Add documentation for z3py compatibility API (#7652)Gereon Kremer
This PR includes documentation for the z3py compatibility API into our general API. It does so by adding the z3py compatibility API as an external project to download it and then have sphinx document it via the autodoc extension that we already use for our regular python API. Right now we simply show everything on one page, which should be refactored in the future.
2021-11-17Preparations for eliminating arithmetic subtyping (#7637)Andrew Reynolds
Adds TypeNode::isArithmetic, NodeManager::mkConstReal and NodeManager::mkConstInt. The first method (for now) is equivalent to TypeNode::isReal, and the latter 2 are equivalent to NodeManager::mkConst(CONST_RATIONAL, ...). This furthermore distinguishes all uses of isReal: all that intend to be isArithmetic are changed in this PR. Redundant uses of isReal() || isInteger() are merged to isArithmetic(). Due to the above, there are no behavior changes in this PR.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback