Alethe: Add function that adds final steps to proof (#7710)

There are some cases when the result has to be transformed, e.g. when it was printed as (cl false) which is correct everywhere except in the last step. This function then transforms the result into (cl).

Should be merged after PR #7675.

Co-authored-by: Haniel Barbosa hanielbbarbosa@gmail.com

Translating API tests to Python — part 2 (#7651)

This PR translates the remaining cpp API tests to python.

Use new token for docs-release (#7709)

This PR uses the new CVC5_DOCS_RELEASE_TOKEN to make uploads to docs-release actually work.

Remove spurious assertion in parser (#7713)

When global declarations are true, we do not push/pop the context of the symbol manager. This removes a spurious assertion that checked whether a pop in this case was greater than the actual context level of the symbol manager.

Fixes cvc5/cvc5-projects#370.

Define sort undeclared (#7714)

Fixes cvc5/cvc5-projects#369.

Now gives:

(error "Parse Error: proj-369.smt2:3.22: Symbol 'Bool' previously declared as a type

  (define-sort _s0 (Bool Bool Bool Bool Bool Bool Bool Bool Bool) Bool)
                    ^
")

Translating more cpp API unit tests to python (#7669)

This translates the majority of the tests from https://github.com/cvc5/cvc5/blob/master/test/unit/api/cpp/solver_black.cpp that were not translated yet, to python.
Additionally, some minor renames and `yapf` formatting is done the the existing tests.

Always run update-pr (#7719)

This removes the event condition on the `update-pr` ci job. Right now, it is not run although it should.

Extend docs example extension (#7717)

This PR extends the custom sphinx extension for examples. It now allows for simple patterns in the file names and matches the file types using arbitrary regular expressions instead of just looking at the file extensions. This is necessary to integrate examples from the z3pycompat API: the examples live at a nontrivial place (in the build folder), which we inject via the file name patterns; we will have two separate examples which both end in .py but can be distinguished via the pattern used in the beginning.

Change CVC4 urls to cvc5. (#7706)

This commit will change the URLs to the new cvc5 nightly builds and coverage
information.

Add rewrite for is_int pi (#7711)

Fixes cvc5/cvc5-projects#365.
Fixes cvc5/cvc5-projects#356.

Scaffold the idiomatic API's documentation (#7715)

Scaffolding the documentation, and fleshing it out for the Boolean functions and terms.

Generalize eager length bound conflicts for regular expression memberships (#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.

Proper check for first-class types in datatype subfields (#7712)

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.

Alethe: Further Printer Implementation (#7675)

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

[proofs] Alethe: Implementation of Printer (#7674)

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>

Remove now unused dumping infrastructure (#7703)

This PR removes the old dumping infrastructure. All dumping has already been migrated to -o.

[proofs] Alethe: Printer Specification (#7673)

Header of the Alethe printer

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Fix minor issues (#7704)

This fixes a few minor coverity issues.

Start post-release for 0.0.4

Bump version to 0.0.4

Bug in printing parameter list in define_fun_to_string (#7700)

Signed-off-by: Sujit Muduli <smuduli@cse.iitk.ac.in>

Consolidate CI jobs (#7697)

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.

Guard regression tests that require libpoly to pass. (#7698)

Regression tests either timeout or return unknown if cvc5 is configured with --no-poly.

api: Refactor mkTerm for kinds with arity = 0. (#7699)

This refactors mkTerm to allow creation of terms of kinds with arity = 0
via Op and/or empty children vector.

examples: Update python api datatypes example. (#7692)

The C++ datatypes example was extended in #7689. This updates the Python
API datatypes example accordingly.

Always enable API black box unit tests (#7696)

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

cmake: Add option --[no]-static-binary. (#7695)

Allows to disable linking against static system libraries explicitly.

Fix ANTLR3 config for i386 and aarch64 builds. (#7694)

This fixes the i386 and aarch64 nightly builds.

examples: Update Java datatypes example with recent extensions. (#7693)

The C++ datatypes example was extended in #7689. This updates the Java
API datatypes example accordingly.

Remove dependency of `TypeNode` on `Node` (#7690)

This is further work towards breaking cyclic dependencies in the `expr`
folder.

Fix potential for cycles in trust substitutions (#7687)

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.

examples: Extend DT api example with APPLY_TESTER and APPLY_UPDATER application. (#7689)

Minor fixes (#7691)

api: Fix creation of nary term kinds via Op. (#7688)

Fixes cvc5/cvc5-projects#367.

Make difficulty manager only consider lemmas at full effort (#7685)

Fixes cvc5/cvc5-projects#350

Enable model-based reduction technique for strings (#7680)

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.

Add kinds to python docs (#7672)

This PR adds the kinds to the documentation for the regular python docs.

Push output language inside the printing code (#7683)

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 (#7643)

Add rewrite rule for bag.card operator using bag.map and lambda

Python API documentation: terms (#7659)

This PR adds documentation for the Terms class in the python API.
Co-authored-by: Gereon Kremer gereon.kremer@cs.rwth-aachen.de

Make `node_value.h` not depend on `node_manager.h` (#7676)

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.

Refactor IO stream manipulators (#7555)

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.

Add rewrite for repeated re.allchar (#7681)

This solves 4 more challenge Amazon benchmarks.

Set proper system processor for arm64 toolchain (#7665)

[prop] Remove unused #define in theory proxy (#7670)

Improve error for check theory assertions with model (#7679)

Makes it so that we report *all* unsatisfied assertions, not just the first one.

Fix const RE test for internal regexp rv kind (#7678)

Fixes #7677.

bv2int module: translation of more cases (#7653)

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

[API] Avoid copying values (#7666)

Clean up relationship of metakind and node_manager (#7649)

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`.

Remove n-ary builder (#7671)

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, ...)).

Allow negative denominator for CLN Rationals constructed from string. (#7667)

api: Fix categorization of DT kinds in kind maps. (#7668)

Refactor CAD option for linear model seed (#7657)

This PR implements another strategy for using the linear model in the CAD-based nonlinear solver. It stays disabled by default.

[proofs] Fix trace in SatProofManager  (#7664)

[proofs] Alethe: Rename DUPLICATED_LITERALS (#7661)

In the Alethe specification the DUPLICATED_LITERALS rule was renamed to CONTRACTION. This PR renames the rule to be consistent with the standard.

api: Fix kind documentation for BAG_MAKE. (#7663)

Improve naming in term canonization when handling HO variables (#7660)

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.

[sat] Fix indentation in "reason" (#7662)

Add documentation for z3py compatibility API (#7652)

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.

Preparations for eliminating arithmetic subtyping (#7637)

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.

Revert change and clean datatypes cons candidate generator (#7645)

PR #7600 refactored and optimized candidate generator. This PR actually corrected an issue where the datatypes constructor expansion candidate generator did not generate instances for triggers whose top symbol is a constructor. However, fixing it to generate instances led to a performance regression on Facebook benchmarks.

This PR reverts the behavior change from that PR, and moreover makes it explicit that we do not generate instances in this case.

Implement aggressive pruning in CAD solver (#7650)

This PR implements a more aggressive pruning of redundant intervals, namely intervals that are covered by two other intervals, but not a single one. As already discussed in the respective paper, it is not entirely clear whether this is beneficial as removing such an interval may make the "overlap" smaller and thus the generated interval in the lower dimension may become smaller as well. It is thus only enabled via a (new) option.
Experiments show that such redundant intervals are relatively common (878 benchmarks on QF_NRA), the impact of this option is very limited and not strictly beneficial.

Update Python packaging infrastructure (#7654)

- Stop passing --lib-only (it no longer exists)
- Fix the regex search for the cvc5 version
- Take a version suffix as an (optional) environmental variable

make default and modes strings instead of enum values (#7656)

For mode options, getOptionInfo would hold the name of the enum values for the default value and the available modes. This PR changes this to hold the string values instead, which is what users can actually use via the API.

Fix binding of quoted symbols in `define-fun` (#7655)

Our `DefineFunctionCommand` was binding the string representation of the
function symbol including the `|` quotes instead of the symbol without
the quotes. This commit fixes the issue.

Remove documentation for --lib-only (#7648)

The feature was removed in #7258.

Update SimpleVC.java (#7647)

Update SimpleVC.java with try with resource missed in previous PR

Translating API tests to Python — part 1 (#7597)

This PR translates some of the API tests from here to Python. The other tests are translated in a private branch and will be added in a separate PR.

Fix compile errors with java examples (#7646)

Fix compile errors with java examples

[proofs] Make sure --proof-check=... is no-op when not checking proofs (#7638)

Fixes cvc5/cvc5-projects#342

Refactor `metakind` (#7639)

This is a first attempt of refactoring our `metakind` definitions and
declarations. The commit removes unnecessary code that was being
generated, moves code from header to source files (primarily code that
was only relevant to the source file), and gets rid of some hacks
related to circular dependencies.

api: Rename BOUND_VAR_LIST to VARIABLE_LIST. (#7632)

[Strings] Minor refactor of eager solver (#7628)

This moves code that is not strictly related to the eager solver out of
the eager solver and into TheoryStrings. This is cleaner and makes it
easier to enable/disable the eager solver.

Add documentation for theory_bags_type_rules.h (#7642)

This PR adds documentation for theory_bags_type_rules.h, and updates the type rule for rel.join_image to ensure tuple elements in the binary relation have the same sort.

Skip `str.code` inferences for sequence eqcs (#7644)

Fixes cvc5/cvc5-projects#340. Type checking
failed because cvc5 was trying to construct a term (str.to_code (seq.unit false)). We do not allow the construction of terms
(str.to_code t) where t is not of type string. This commit fixes the
issue by skipping sequence equivalence classes when doing inferences
related to str.to_code.

Note that the regression test is slightly different from the original
unit test. It asserts that the index passed to seq.nth is
non-negative, which ensures that we can check the resulting model. I
have checked that the modified regression test triggers the issue before
the change in this commit.

Fix type error for rewriting bag.map bag.union_disjoint (#7640)

Fix type error for rewriting bag.map bag.union_disjoint

Add operator set.map to theory of sets (#7641)

Towards supporting set.map operator in the sets solver.

bags: Rename kinds with a more consistent naming scheme (#7611)

[proofs] Cancel SYMM in CDProof, throw an error for cyclic proofs during double SYMM elimination (#7630)

This fixes the potential for cyclic proofs in CDProof when P and (SYMM P) are added as proofs to a CDProof with automatic managing of symmetry.

This manifested as non-termination on the seqArray branch with proofs enabled, instead, if this were to occur, we should throw an error, which is easy to catch.

Fix redundant definitions of `NodeValue::getConst` (#7636)

If multiple kinds have the same payload, cvc5 is currently generating
multiple copies of NodeValue::getConst() with the same template
argument, which results in a redefinition of the same function. This
commit modifies the mkmetakind script to avoid emitting redundant
definitions of NodeValue::getConst().

Add some basic rewrites for regular expression intersection (#7629)

Adds some basic rewrites for re.inter and re.union involving children of the form (str.to_re c) for constants c.

This is towards addressing bottlenecks for Zelkova benchmarks.

Remove `ConstantMap<Rational>` (#7635)

This is in preparation of having two different kinds (CONST_RATIONAL
and CONST_INT) share the same payload. To do so, we cannot rely on
ConstantMap<Rational> anymore to map the payload type to a kind. This
commit extends support in the mkmetakind script to deal with such
payloads by adding a + suffix to the type. The commit also does some
minor refactoring of NodeManager::mkConst() and
NodeManager::mkConstInternal() to support setting the kind explicitly.
Finally, the commit addresses all instances where mkConst<Rational>()
is used, including the API.

Various minor docs improvements (#7626)

This PR does a number of minor improvements to the docs.

Add an API method to get the raw name of a term. (#7618)

Generalize front-end checks to check for shadowed variables (#7634)

When using the API, we currently check for free variables in assertions and in terms passed to get-value.

We also require checking for variable shadowing.

This generalizes the utility method so that both free variables and shadowed variables are checked and reported to the user.

Add lazy approach for handling lambdas in the HO extension (#7625)

This adds a new option --uf-lazy-ll for not applying lambda lifting eagerly. This is motivated by HO operators in theory of bags, e.g. bag.map, which cannot answer "sat" for simple problems where lambdas are mapped to bags, due to the introduction of quantified formulas for eliminating lambdas.

It moves lambda lifting from term formula removal to a utility module within TheoryUF. If lazy lambda lifting is enabled, this module does not introduce quantified formulas for lambdas eagerly.

It adds 2 lemma schemas for reasoning about quantifier-free constraints with lambdas natively in TheoryUF. It extends the model construction in the HoExtension to assign lambdas in the case that an equivalence class contains a variable that is defined by a lambda.

Fixes for update/nth over constant sequences (#7631)

This includes fixes related to how we process seq.update / seq.nth applied to sequence constants.

api: Add Solver::mkRegexpAll(). (#7614)

[proofs] Alethe: Translate of Arithmetic rules (#7613)

Implementation of the translation of MACRO_ARITH_SCALE_SUM_UB, INT_TIGHT_UB and INT_TIGHT_LB into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Translate INSTANTIATE rule  (#7607)

Implementation of the translation of INSTANTIATE rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

docs: Also create javadoc for generated Kind.java (#7624)

Fix soundness issue of missing premises for count bag lemmas (#7615)

This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems.
The error is related to a previous fix which did not include the required antecedent in the two lemmas:

(=>  (= e x)
        (=
              (bag.count e (bag x c))
             (ite (>= c 1) c 0)))

and

(=>  (distinct x e))  (= (bag.count e (bag x c)) 0))

java: Fix building cvc5.jar for cmake 3.16. (#7623)

Fixes #7579.

Fix parsing array constants (#7617)

This generalizes a fix for parsing array constants.

Fixes #7596.

sets: Rename set.intersection to set.inter. (#7622)

This further renames kind SET_INTERSECTION to SET_INTER.

Reorganize test/unit/api directory. (#7612)

This moves .cpp files to directory test/unit/api/cpp and python files in
test/python/unit/api to test/unit/api/python.

[proofs] Alethe: Translate Further Equality rules (#7606)

Implementation of the translation of FALSE_INTRO, FALSE_ELIM, TRUE_INTRO and TRUE_ELIM rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

[proofs] Alethe: Translate Equality rules (#7605)

Implementation of the translation of SYMM, TRANS and CONG rules into the Alethe calculus.

Co-authored-by: Haniel Barbosa <hanielbbarbosa@gmail.com>

Only eliminate lambdas in higher-order elimination if ho-elim is enabled (#7603)

Required for lazy lambdas in HO.

Also properly guards the case when the preprocessing pass is a no-op.