Age | Commit message (Collapse) | Author |
|
(#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.
|
|
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.
|
|
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
|
|
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>
|
|
This PR removes the old dumping infrastructure. All dumping has already been migrated to -o.
|
|
Header of the Alethe printer
Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>
|
|
This fixes a few minor coverity issues.
|
|
|
|
|
|
Signed-off-by: Sujit Muduli <smuduli@cse.iitk.ac.in>
|
|
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.
|
|
Regression tests either timeout or return unknown if cvc5 is configured with --no-poly.
|
|
This refactors mkTerm to allow creation of terms of kinds with arity = 0
via Op and/or empty children vector.
|
|
The C++ datatypes example was extended in #7689. This updates the Python
API datatypes example accordingly.
|
|
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
|
|
Allows to disable linking against static system libraries explicitly.
|
|
This fixes the i386 and aarch64 nightly builds.
|
|
The C++ datatypes example was extended in #7689. This updates the Java
API datatypes example accordingly.
|
|
This is further work towards breaking cyclic dependencies in the `expr`
folder.
|
|
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.
|
|
application. (#7689)
|
|
|
|
Fixes cvc5/cvc5-projects#367.
|
|
Fixes cvc5/cvc5-projects#350
|
|
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.
|
|
This PR adds the kinds to the documentation for the regular python docs.
|
|
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).
|
|
Add rewrite rule for bag.card operator using bag.map and lambda
|
|
This PR adds documentation for the Terms class in the python API.
Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de
|
|
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.
|
|
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.
|
|
This solves 4 more challenge Amazon benchmarks.
|
|
|
|
|
|
Makes it so that we report *all* unsatisfied assertions, not just the first one.
|
|
Fixes #7677.
|
|
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
|
|
|
|
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`.
|
|
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, ...)).
|
|
|
|
|
|
This PR implements another strategy for using the linear model in the CAD-based nonlinear solver. It stays disabled by default.
|
|
|
|
In the Alethe specification the DUPLICATED_LITERALS rule was renamed to CONTRACTION. This PR renames the rule to be consistent with the standard.
|
|
|
|
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.
|
|
|
|
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.
|
|
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.
|