Improve handling of `(push)` and `(pop)` (#8641)

This extends PushCommand and PopCommand to take a number of levels
to push/pop. We have support for pushing an arbitrary number of levels
at the API level, so this simplifies the parser code and makes dumping
more precise (previously, we were dumping (push 2) as two (push 1)
commands).

Add declare-oracle-fun command (#8621)

In preparation for adding declare-oracle-fun to the API/parser.

Minor simplifications for datatype selector triggers (#8636)

This is leftover simplification from the fact that (s x) is no longer expanded to (ite (is-C x) (s_total x) (uf x)).

int-blaster: direct support for bvcomp (#8640)

This PR adds a translation of bvcomp using an ite.
Fixes cvc5/cvc5-projects#417
and contains the failed formula as a regression.

Remove redundant assertion in int-blaster (#8639)

When translating nodes with no children, the default case does not change the original node, and so we do not need to assume anything about the node. fixes cvc5/cvc5-projects#416 . The example from the issue is added as a unit test.

Updates to zero level learner (#8597)

Now tracks learned literals for all types.  Unifies the output of `-o learned-literals`.

Followup PRs will add the deep restart feature, which configures which kind of learned literals can be used when restarting.

Avoid trivial equalities in explanation of SETS_CARD_CYCLE (#8635)

This was the root cause of cvc5/cvc5-projects#178.

Simplify implementation of subtype methods in TypeNode (#8634)

Also deletes unused data that was used for an inference schema involving subtypes in sets.

Add table.project evaluator (#8632)

This PR

adds evaluator for table.project operator
updates the parser to interpret "Table" as a table with zero columns

Move linear arithmetic solver to theory::arith::linear (#8628)

This moves the current linear arithmetic solver to src/theory/arith/linear, and inside `cvc5::internal::theory::arith::linear`.

Some code uses internal utilities from `arith::linear`, although this should be minimized.

This is preparation for breaking dependencies with the old code.

Generalize concat conflict for sequences in LFSC (#8625)

This ensures LFSC proofs are correct when using CONCAT_CONFLICT for sequences.

In detail, to justify why (seq.++ (seq.unit c1) t1) = (seq.++ (seq.unit c2) t2) is a conflict, where c1 and c2 are constants, we require an explicit step to evalute (seq.unit c1) = (seq.unit c2) to false, since c1 and c2 are theory-specific constants.

Note this is different from (str.++ (char n1) t1) = (str.++ (char n2) t2) where a syntactic check of n1 and n2 suffices.

This fixes proof checking for regress0/seq/seq-types.smt2.

Remove instances of `check-proofs` in regressions. (#8630)

This PR removes usages of check-proofs option according to the following rules:

unsat and no-check-proofs --> DISABLE-TESTER: proof
unsat and check-proofs --> remove option
sat and no-check-proofs --> remove option
sat and check-proofs --> change to produce-proofs
no-produce-proofs --> DISABLE-TESTER: proof

Add some missing FP symbols to LFSC (#8629)

Distinguish name variants for types in LFSC node converter (#8624)

This PR ensures we distinguish names for cases where types and terms are given the same name.

In particular, this generalizes the getNameForUserNameOf to work with node identifiers instead of Node, so that TypeNode can also use this method for assigning unique names.

It also adds preliminary support for uninterpreted sort constructors in the LFSC node converter.

This fixes 4 more LFSC failures on our regressions.

Make more utilities distinguish Int and Real (#8626)

Towards eliminating arithmetic subtyping.

Simplify management of separation logic heap (#8580)

The separation logic heap is conceptually an extension of the logic, which lives in Env. This PR moves the separation logic heap types from TheoryEngine to Env.

It furthermore makes it so that declaring the separation logic heap does not force initialization of the SolverEngine, meaning that further declarations/options may be done after setting the heap.

This is in preparation for making the SmtSolver class easier to deep reset.

Remove support for unused `declare-*` commands (#8623)

This commit removes support for
declare-sorts/declare-funs/declare-preds. These commands seem to
be a leftover of an earlier SMT-LIB draft [0]. We only had a test for
declare-funs and Z3 doesn't support declare-funs either.

[0] http://homepage.cs.uiowa.edu/~astump/papers/smt-cmd-lang.pdf

Fix internal type issue for congruence over quantifiers in LFSC post-processor (#8619)

Avoids debug assertions in LFSC proof conversion when doing congruence over closures.

Implement internal support for (definitional) satisfiability modulo oracles (#8618)

Adds implementation of OracleEngine, which adds lemmas of the form (= (f c) d) on demand for I/O pairs (c,d) from oracle calls.

Make LFSC printer robust to internal types (#8616)

This makes the LFSC node converter track the "user declared" symbols and types that it encounters.

It furthermore makes the "dry run" phase of proof printing happen before types and symbols are declared, so that all declared symbols are found before the preamble of LFSC proofs are printed.

These changes are specifically to fix cases where a internal type is generated that does not appear in the input. For example, some preprocessing passes may construct auxiliary uninterpreted sorts.

This fixes 6 more LFSC failures from our regressions.

Implement internal support for synthesis modulo oracles (#8617)

SyMO is implemented as a preprocessor for SMT queries in the verification subsolver of SyGuS.

Remove static calls to rewrite involving array constants (#8613)

The type enumerators for arrays and functions relied on static calls to the rewriter. This is overkill, as the appropriate calls to the utility method normalizeConstant in the array rewriter class suffices.

The eliminates 2 of the remaining static calls to the rewriter.

Improvements to phase shifting + purification lemmas (#8598)

Makes 3 improvements to phase shifting + purification lemmas:
(1) we use purification skolems when possible, e.g. for exp(t), or sin(c) where -pi <= c <= pi, since it is unnecessary to assert c is in proper phase. This also adds proofs for purification of exp, which is hence trivial.
(2) we make the phase shift variable a real for which is_int holds. This avoids mixed int/real arithmetic, in preparation for eliminating subtyping
(3) the proof checker and sine solver use a common utility for getting the phase shift lemma.

Revised partitioning (#8143)

This adds the "revised" partitioning algorithm to the splitter and adds support for collecting literals from the sat solver. There is only one partitioning strategy in this PR, but the others will be added in subsequent PRs.

[proofs] [dot] New way to traverse the proof when printing a .dot DAG (#8610)

Change the way cvc5 traverse and print the proof when --proof-dot-dag option is used. The main change is related to the way the printer tracks visited proof nodes. The new conditions are:

- If the proof node has already been visited inside the current scope.
- If the proof node is closed (i.e. does not contains a subproof whose rule is ASSUME) and has already been visited (here the condition is global and the scope doesn't matter).

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

Integrate oracle checker into quantifiers term registry (#8604)

Also incorporates into sygus term database. For SyMO, oracle function symbols act analogously to recursive function definitions; the oracle checker is used to rewrite terms in the same contexts as when recursive function definitions are evaluated.

Fix spurious assertion involving subtypes (#8611)

Fixes #8609.

Update LFSC version (#8614)

Now has a different expected output ("success" for each check).

Add Relation and Table types to SMTLib parser (#8605)

Fix type issue for FP constants in LFSC node converter (#8612)

Fixes type errors in debug builds.

Fix spurious assertion failure caused by subtyping in LFSC proof postprocessor (#8608)

Also removes an old case for parametric datatypes in getBaseType, which is incorrect since datatypes not longer use subtyping.

This avoids more assertion failures in debug mode for LFSC due to subtypes.

Fix type issue for LFSC null terminator (#8607)

This fixes an assertion failure when producing LFSC proofs in debug mode.

The issue currently does not impact the correctness of the code, although this will be important if subtypes are eliminated.

Add oracle checker utility (#8603)

This is a utility that allocates oracle callers for oracle functions on demand and can be used to convert a term containing oracle function symbols into its evaluated form.

It will be used for both SMTO (for checking consistency of oracle interfaces) and SyMO (as part of refinement lemma evaluation in CEGIS).

Add oracle caller utility (#8599)

The implementation of this class has a placeholder for calling external binaries, which will be filled in a later PR.

Making some benchmarks SMT-LIB compliant for subtypes (#8600)

This makes some of our regressions compliant for arithmetic subtyping. This is required to make these benchmarks parsable when subtyping is eliminated.

We should discuss whether we should be permissive for such benchmarks. Regardless, the majority of our regressions should be SMT-LIB compliant.

Fix more misuses of arithmetic subtypes (#8601)

[proofs] [dot] Print nodes clusters at dot format (#8574)

Add a printer option that allows the dot printer to identify each node type and group them up in node clusters. These cluster are determined according to "part of the proof" whether a node belongs to:

- input
- sat proof
- cnf proof
- theory lemma proof
- preprocessing

Signed-off-by: Vinícius Braga Freire vinicius.braga.freire@gmail.com

More cleaning uses of arithmetic subtyping (#8595)

Towards eliminating arithmetic subtyping.

Add oracle engine to quantifiers engine (#8589)

This class is the subsolver of quantifiers engine for handling oracles in SMTO. The implementation of this class will be added in followup PRs.

It also contains a utility method for constructing oracle interfaces.

Remove spurious case of ppRewrite (#8596)

Constants equal to constants are always rewritten to false.

Add learned literal type and prop learned database (#8582)

In preparation for deep restart feature, and for extending the get-learned-literal interface to multiple types.

Simplify parser (#8592)

This commit simplifies our parser by removing code that is not relevant
anymore since the removal of support for SMT-LIB <=2.6.

Minor refactoring of smt2 printer (#8588)

Do not allow unresolved sorts in smt2 (#8587)

This simplifies the smt2 parser so that we never parse "inlined" unresolved sorts. This infrastructure was used for accomodating the ad-hoc datatype syntax from SMT-LIB <=2.5, and SyGuS 1.0.

We now assume that sorts are fully declared wherever we parse them.

Eliminate more uses of CONST_RATIONAL (#8590)

To eliminate arithmetic subtyping, we require distinguishing CONST_RATIONAL and CONST_INTEGER internally. Code should avoid usage of these kinds and use trusted utilities instead (e.g. mkConstReal, mkConstInst, isConst).

Properly parse numerals as real when integers are disabled (#8591)

SMT-LIB says numerals are real when integers are not included in the logic.

Due to subtyping, we don't complain internally, although if subtyping is eliminated, this fix is necessary.

Generalization for sygus verify utility (#8586)

This is in preparation for synthesis modulo oracles (SyMO), where the verification loop may run multiple times for a given solution. In a follow up PR, the loop introduced in this PR may run multiple times when oracles are present, since oracle invocations in the subsolver may trigger further simplifications to the rewritten form of the specification.

It also makes it so that candidate models are generated for "unknown" results for subsolvers, which is required for SyMO.

Internal representation of oracle interface quantifiers (#8585)

This is the first step towards supporting SMT and synthesis modulo oracles.

It adds the kind required for specifying "oracle interface quantifiers", or, quantified formulas that specify constraints that depend on an external binary.

Add method to get leaves of a NodeTrie (#8583)

From the oracles branch.

Make sets and bags operators left-associative (#8584)

Makes it so that we parse n-ary applications of e.g. set.union in smt2.
Left associativity seems to be the case for difference operators in databases.
See
https://docs.microsoft.com/en-us/sql/t-sql/language-elements/set-operators-except-and-intersect-transact-sql?view=sql-server-ver15

Eliminate SmtSolver dependency on SolverEngineState (#8581)

This is in preparation for making SmtSolver able to be deep reset (reconstructed) within in a SolverEngine instance.

Minor fix for printing nullary operators in smt2 (#8577)

Fix proof checker for SUBS (#8578)

Could lead to proof checking failures when using `--proof-granularity=rewrite`

Fixes for LFSC printing and signatures (#8579)

Ensures we recognize some internal FP symbols, adds a missing string operator, fixes seq.unit operator printing (required for CONG over seq.unit), fix for 0-ary tuple printing.

Start post-release for 1.0.0

Bump version to 1.0.0

api: Fix doc generation for kinds in java API. (#8576)

Plus some more fixes for docs.

Update copyright headers for release 1.0 (#8539)

Update NEWS for cvc5 1.0. (#8460)

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
Co-authored-by: mudathirmahgoub <mudathirmahgoub@gmail.com>
Co-authored-by: Andres Noetzli <andres.noetzli@gmail.com>

Make inst constant attribute robust to purification variables (#8573)

Fixes #8572.

Certain combinations of cegqi/sygus-inst may be solution unsound when combined with E-matching, due to using skolems that have dependencies on instantiation constants are used in instantiations.

Make rewriter more robust against RAN becoming rational (#8564)

We use real algebraic number to represent multiplicities of sum terms within the arithmetic rewriter. Unfortunately, such real algebraic numbers can realize that they are in fact rational at awkward times. This makes isRational() unsuitable for checking this, instead we should construct the node and check afterwards.

api: More fixes in the java API. (#8571)

Be permissive for subtyping in function definitions (#8568)

This is to accommodate the Real theory in SMT-LIB, which says that numerals specify reals.

Instead of making our parser for numerals dependent on the logic, we are more permissive.

This fixes several spurious parsing issues in smtlib.

api: More fixes in C++ API docs. (#8570)

Write-up for Pythonic API quickstart (#8566)

docs: Fix mkTerm calls in theory documentation. (#8567)

api: Fix OptionInfo docs for java API. (#8569)

api: Fixes in docs for Op. (#8565)

api: Fixes for Grammar docs in java API. (#8563)

api: Fixes in java api docs. (#8562)

api: Fixes in docs for DatatypeConstructor. (#8561)

Docs: remove api from package name in java.rst (#8560)

Fix broken links in https://cvc5.github.io/docs/cvc5-0.0.12/api/java/java.html

api: More fixes in docs. (#8559)

api: First batch of fixes in the api docs. (#8558)

Uses `@return <uppercase> .... <period>` and `@param <param> <uppercase> ... <period>`,
plus various fixes in the docs.

Fix links when converting kinds documentation to python (#8557)

This mainly fixes explicit rst links when we convert the kinds comments to python.

python api: More fixes. (#8556)

Start post-release for 0.0.12

Bump version to 0.0.12

Maintain symlink to docs for latest release (#8555)

This PR creates/updates a symlink called latest to the last release. This simplifies permalinks into the documentation.

Remove duplicate lines (#8552)

We remove the arguments from links to solver methods in the Kinds
documentation to turn C++ references into python references. This
oftentimes collapses previously different overload of methods (usually
mkTerm()). This PR generically removes duplicate lines from these
comments using some re magic.

Bump Pythonic (transcendentals) & exception example (#8553)

- Bump version of Pythonic API to include transcendentals.
- Document Pythonic API's transcendentals.
- Add exception Pythonic API example.

api: Various fixes in Python documentation. (#8554)

Various improvements and fixes in the documentation (#8551)

This PR contains a variety of fixed and improvements to the documentation.

Rename getInstantiatedConstructorTerm to getInstantiatedTerm (#8549)

This is in line with the change for non-parametric constructors (getConstructorTerm -> getTerm).

Also adds documentation to make the use of constructors, selectors, testers, updaters more clear.

Use raw symbols in proofs (#8550)

This ensures we don't quote symbols that should not be quoted, fixing two issues:
(1) Proofs in the internal calculus don't convert `:args` to `|:args|`.
(2) LFSC identifiers for terms are not quoted based on SMT-LIB restrictions.

Work towards https://github.com/cvc5/cvc5-projects/issues/466, quoted TypeNode names still need to be addressed.

[proofs] [sat] Make SAT assumption bookeeping robust to incremental (#8536)

Similarly to what happened with proofs of optimized SAT clauses getting lost (in the sense of inserted at lower assertion levels than the current one, during incremental solving), we need to make the bookeeping of the current SAT assumptions in the SAT proof manager robust to context popping. Not doing so can break the final proof construction, which relies on this information. A regression is added which showed the issue via the openness of a step added to the lazy proof chain (even though this did not lead to issues in the final proof).

This commit extends the OptimizedClausesManager to also optionally track a hash set of nodes to have nodes added to it during popping. This is hooked in the SAT proof manager to the SAT assumptions hash set.

There are four instances of notifications to the SAT proof manager of SAT assumptions: two in the proof CNF stream and two in the SAT solver. We only need to worry about the proof CNF stream ones, since the SAT solver ones are for literals (which do
not have assertion levels) and for some cases of the final conflict clause generated, which is always at the current assertion level. For the proof CNF stream ones it suffices to notify the SAT proof manager when the CNF stream itself is notified that a propagation or clause was inserted at an optimized level, as these are the only possible cases.

Fix for get-value with empty uninterpreted sort domain (#8547)

Alternative for https://github.com/cvc5/cvc5/pull/8546.

We were mistakenly using `mkGroundTerm` instead of `mkGroundValue` to make the domain of an uninterpreted sort non-empty.

This ensures that get-value calls do not throw a spurious exception when there is a declared uninterpreted sort and there are no terms of that sort.

As a result, this also required fixing a few further issues regarding how uninterpreted sort constants are printed in models, and fixing the expected results on 2 more regressions.

Start post-release for 0.0.11

Bump version to 0.0.11

use one process more than we have cores (#8545)

This PR uses one process more than we have cores in the CI. This speeds up the CI jobs when time is spent waiting on IO instead of actually using the CPU.

Rename mkSygusGrammar to mkGrammar (#8544)

Remove variant of mkDatatypeDecl with one sort parameter (#8543)

Subsumed by the vector version.

Also marks more methods as experimetnal.

api: Rename get(Selector|Constructor)Term() to getTerm(). (#8537)

Follow renaming within pythonic API (#8532)

We are renaming files in the pythonic API to make it look less like it is somehow part of z3 (but still acknowledge that we took code from z3Py properly). This PR follows the change in cvc5/cvc5_pythonic_api#80.

Always cancel already running CI runs on forks (#8542)

One effect of our changed concurrency policy is that we never cancel runs on forks. This PR changes this, always allowing the concurrency mechanism to cancel on repositories that are not the main repository.

Minor edits in docs. (#8540)

Ignore irrelevant exponential terms (#8534)

Fixes #8517.

docs: Add Python installation instructions for pip. (#8538)

api: Remove DatatypeConstructor::getSelectorTerm(). (#8535)

Require that used model values are constant in CEGQI (#8528)

Fixes #8520.