Update sygus grammar normalization to use node-level datatype. (#3567)

Refactor sygus stats (#3684)

Minor refactoring of constructor classes in fast enumerator (#3685)

Fix arithmetic rewriter for exponential (#3688)

Fix rep set increment for empty domains (#3682)

Make eq chain an aggressive rewrite in extended rewriter (#3679)

Eliminate spurious postprocessing step for single invocation (#3674)

Ensure literals in FMF decision strategies are in the CNF stream (#3669)

Weaken assertion for models with approximations (#3667)

Move disequality list to solver state in strings (#3678)

Example minimize evaluation utility. (#3671)

External cache argument for evaluator (#3672)

Do not debug check model for models with approximations (#3673)

We don't run check-model for models with approximate values, however we were still running the internal debugCheckModel method, which leads to assertion failures. This disables this check.

Fixes #3652.

Better heuristics for marking congruent variables (#3677)

Modularize more steps in the strings strategy (#3676)

Minor updates to string utilities (#3675)

expectedType in proof-printing code (#3665)

* expectedType in proof-printing code

To print lemma proofs in theories that use multiple sorts that have a
subtype relationship, we need to increase communication between the
TheoryProofEngine and the theory proofs themselves.

This commit add an (optional) argument `expectedType` to many
term-printing functions in TheoryProofEngine and TheoryProof.

Right now it is unused, so always takes on the default value of "null"
(meaning no type expectation), but in the future the TheoryProofEngine
will use it to signal TheoryProof about what type is expected to be
printed.

* TypeNode, Don't mix default args & virtual

* Use TypeNode instead of Type (The former are lighter)
* Don't add default arguments to virtual functions, because these cannot
  be dynamically overriden during a dynamic dispatch.
  * Since we don't want them to be overidable anyway, we use two
    functions: one that is non-virtual and has a default, the other that
    is virtual but has no default. The former just calls the latter.

* clang-format after signature changes

Fix isLeq function in String utility (#3659)

Do not insist on bound values being constant in arithmetic instantiation (#3643)

Avoid PLUS with one child for bv2nat elimination (#3639)

Axioms for affine function bounds. Tests. (#3632)

* Axioms for affine function bounds. Tests.

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Clarify descriptions of th_lira tests

Thanks, Yoni!

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

Fix trivial solve method for single invocation (#3650)

Fix subtyping for instantiations where internal representatives are chosen (#3641)

Fix substitution in nl solver (#3638)

* Fix for 3614

* Add regression

* Remove regression

Co-authored-by: Ahmed Irfan <43099566+ahmed-irfan@users.noreply.github.com>

Fix single invocation partition for non-function non-atomic types (#3642)

Fix check for subtypes in sygus PBE (#3640)

Fix parameteric sorts involving Booleans in sygus default grammars (#3629)

Types and side conditions for affine bounds (#3631)

* Types and side conditions for affine bounds

Bounds (being positive, non-negative) actually have an arithmetic.
This PR defines that.

Useful b/c Farkas proofs are basically just sums of bounded affine
functions.

* Address Yoni's comments. Thanks!

* Moved a positivity-test to th_real
* Describe what an affine bound is in better detail

Affine Axioms (#3630)

Used for proving that real terms are affine functions of their
variables.

Types & side-conditions for linear and affine fns (#3627)

This commit introduces types for linear combinations of arith variables
along with side conditions for their arithmetic.

It does the same for affine functions.

These primitives are ultimately used in our machinery for Farkas proofs.

Axioms (and side conditions) for tightening bounds (#3613)

* Axioms (and side conditions) for tightening bounds

* Side conditions for verifying floor/ceiling-like functions
* Axioms for their correct execution
* Axioms for bound tightening.

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Address Yoni's comments by addings documentation.

Thanks Yoni!

Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

LIRA proof: Arithmetic predicates & reification thereof (#3612)

* Merge branch 'master' into lira-pf-arith-pred

* Shorten reify_arith_pred, thanks Yoni!

Use recursion!

* typo

LIRA sig: int, real terms, and conversions (#3610)

* LIRA sig: int, real terms, and conversions

* Address Yoni's comments.

* Better description of "reify" functions
* explicit (rather than implicit) `fail` when reifying integer division

Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>

Use axioms when checking goal entailment for abduction algorithm (#3611)

New C++ API: Add nullary constructor for Result. (#3603)

Generalize example-based sym breaking to conjectures with constant function apps (#3605)

Disable unsat cores for regression that times out (#3607)

Regression `regress2/strings/issue3203.smt2` is currently timing out
depending on the version of the libraries loaded (see #3606 for more
info). This commit temporarily disables the regression to get the
nightlies to pass again.

Support arbitrary unsigned integer attributes (#3591)

Fixes #3586. On macOS, `size_t` resolves to `unsigned long` whereas `uint64_t`
resolves to `unsigned long long`. Even though the types have the same bit-width
and signedness, they are not considered the same type. This caused issues with
`Attribute`s that store `size_t` values because we only specialized the
`getTable()` struct for `uint64_t`. This commit changes the specialization to
work for arbitrary unsigned integer types of at most 64-bit. It does that by
generalizing the specialization of `getTable()` and by implementing a
`KindValueToTableValueMapping` for unsigned integer attributes of up to 64-bit
that casts integers between the attributes bit-width and `uint64_t`.

Fix side condition check in sygus core connective (#3600)

Fix enum names in AIG bitblaster. (#3599)

Fix printing of models of uninterpreted sorts (#3597)

Track trivial cases in transition inference (#3598)

Optimize str.substr reduction (#3595)

This commit optimizes the `str.substr` reduction by replacing the
if-then-else term for the length of the suffix `len(sk2) = ite(len(s) >=
n+m, len(s) - (n + m), 0)` with `(len(sk2) = len(s) - (n + m) v
len(sk2) = 0) ^ len(skt) <= m`. Experiments have shown that the latter
encoding is more efficient.

Fix backtracking issue in sygus fast enumerator (#3593)

Universe set cardinality for finite types with finite cardinality (#3392)

* rewrote set cardinality for finite-types

* small changes and format

Fix unary minus parse check (#3594)

Update any-constant and normalization policies for sygus grammars (#3583)

Fix finiteness check for bounded fmf (#3589)

Recently, finite model finding via uninterpreted sorts was decoupled from finite bound inference techniques (the BoundedIntegers module in theory/quantifiers/fmf/). This module assumed that finite model finding was enabled in one place. This fixes the issue by adding an additional check. This fixes a model unsoundness issue where bounds on an uninterpreted sort were not being enforced.

This fixes #3587.

[proof] ITE translation fix (#3484)

* Bugfix: convert ifte arms to formulas for printing

We have two kinds of ITEs in our LFSC proofs:
   * ite: for sort-typed expressions
   * ifte: for formulas
Say that we have a Bool-sorted ITE. We had machinery for emitting an
`ifte` for it, but this machinery didn't actually convert the arms of
the ITE into formulas... Facepalm.

Fixed now.

* Test the lifting of ITEs from arithmetic.

This test verifies that booleans ITEs are correctly lifted to formula
ITEs in LRA proofs.

It used to fail, but now passes.

* clang-format

* Typos.

* Add test to CMake

* Set --check-proofs in test

* Address Yoni

* Expand printsAsBool documentation
* Assert ITE typing soundness

* Assert a subtype relation for ITEs, not equality

* Update src/proof/arith_proof.h

Thanks Yoni!

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
Co-authored-by: yoni206 <yoni206@users.noreply.github.com>

Initial support for string reverse (#3581)

Type rules, parsing and printing, basic rewriting including constant evaluation, reduction for string reverse (`str.rev`).

Also improves support in a few places for tolower/toupper.

Define all options modified by ENABLE_BEST using cvc4_option (#3578)

Signed-off-by: Simon Dierl <simon.dierl@cs.tu-dortmund.de>

Fix typo in smt_options.toml. (#3579)

Increment Taylor degree for tangent and secant plane inferences for transcendentals (#3577)

Avoid calling rewriter from type checker (#3548)

Fixes #3536. The type checker for the chain operator was calling the
rewriter. However, the floating-point rewriter was expecting
`TheoryFp::expandDefinition()` to be applied before rewriting. If the
chain operator had subterms that were supposed to be removed by
`TheoryFp::expandDefinition()`, the FP rewriter was throwing an
exception. This commit fixes the issue by not calling the full rewriter
in the type checker but by just expanding the chain operator. This is a
bit less efficient than before because the rewriter does not cache the
result of expanding the chain operator anymore but assuming that there
are no long chains, the performance impact should be negligible. It also
seemed like a reasonable assumption that the rewriter can expect to run
after `expandDefinition()` because otherwise the rewriter has to expand
definitions, which may be too restrictive.

Generate code for options with modes. (#3561)

This commit adds support for code generation of options with modes (enums). From now on option enums can be specified in the corresponding *.toml files without the need of extra code. All option enums are now in the options namespace.

Fix spurious parse error for rational real array constants (#3554)

Currently we can't parse constant arrays that store real values that are given as rationals `(/ n m)`. We throw a spurious parse error for `((as const (Array Int Real)) (/ 1 3))`, indicating that the argument of the array is not constant. This is caused by the fact that `(/ 1 3)` is parsed as a *division* term not a rational value.

This adds a special case to constant array construction so that we compute the result of a constant division instead of using the division term `(/ n m)` when constructing an array constant.

Use the evaluator utility in the function definition evaluator (#3576)

Improves performance on ground conjectures with recursive functions. We use the evalutator to (partially) evaluate bodies of recursive functions, instead of relying on substitution+rewriting.

Extend model construction with assignment exclusion set (#3377)

This extends the core model building algorithm in CVC4 with "assignment exclusion sets".  This functionality is useful for assigning values to terms of finite type that have specific restrictions on what their value cannot be.

In detail, previously, all unassigned terms of finite type were always assigned the first term in the type enumeration.  This is done since it is assumed that theories (e.g. datatypes) always do enough work to ensure that *arbitrary* values can be assigned to terms of finite type, and *fresh* values can be assigned to terms of infinite type. However, there are compelling cases (sets+cardinality for finite element types) where one may want to impose restrictions on what values can be assigned to terms of finite types.  Thus, we now provide `setAssignmentExclusionSet` as a way of communicating these restrictions.

This commit also refactors a few parts of `TheoryEngineModelBuilder::buildModel` to be clearer, in particular by adding a few helper functions, and by caching certain information early in the function instead of recomputing it.

This is work towards #1123.

Support ackermannization on uninterpreted sorts in BV (#3372)

Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.

Move Datatype management to ExprManager (#3568)

This is further work towards decoupling the Expr layer from the Node layer.

This commit makes it so that ExprManager does memory management for Datatype while NodeManager maintains a list of DType.

As a reminder, the ownership policy (and level of indirection through DatatypeIndex) is necessary due to not being able to store Datatype within Node since this leads to circular dependencies in the Node AST.

Fix evaluator for non-evaluatable nodes (#3575)

This ensures that the Evaluator always returns the result of substitution + rewriting for constant substitutions.

This requires a few further extensions to the code, namely:
(1) Applying substutitions to operators,
(2) Reconstructing all nodes that fail to evaluate by taking into account evaluation of their children.

Revert evaluate as node. (#3574)

Trace tags for dumping the decision tree in org-mode format (#2871)

This would add tracing options to print the decision tree in [org-mode](https://orgmode.org/) format which can be viewed with emacs or [vim-orgmode](https://github.com/jceb/vim-orgmode).

In the raw format, the number of asterisks denote the decision level of a decision, and within a propagation node, the number of spaces denote the level. Most viewers render the asterisks as indented bullets.

There are some options for controlling verbosity:
`dtview` - prints the decisions (basic option)
`dtview::command` - also prints smt-lib commands as they're issued
`dtview::conflict` - also prints conflicts
`dtview::prop` - also prints propagations

Example usage:
`cvc4 -t dtview -t dtview::command -t dtview::conflict -t dtview::prop <example smt2 file> &> example-trace.org`

The resulting file when opened with an org-mode viewer has collapsible nodes, where "..." marks a node with children.

Minor improvement to evaluator (#3570)

Fixes a bug where we don't return the partially evaluated version (for unevaluatable nodes). Also adds `NONLINEAR_MULT` whose semantics is identical to `MULT`.

Simple optimizations for the core rewriter (#3569)

In some SyGuS applications, the bottleneck is the rewriter.  This PR makes a few simple optimizations to the core rewriter, namely:
(1) Minimize the overhead of `theoryOf` calls, which take about 10-15% of the runtime in the rewriter.  This PR avoids many calls to `theoryOf` by the observation that nodes with zero children never rewrite, hence we can return the node itself immediately.  Furthermore, the `theoryOf` call can be simplified to hardcode the context under which we were using it: get the theory (based on type) where due to the above, we can assume that the node is not a variable.
The one (negligible) change in behavior due to this change is that nodes with more than one child for which `isConst` returns true (this is limited to the case of `APPLY_CONSTRUCTOR` in datatypes) lookup their theory based on the Kind, not their type, which should always be the same theory unless a theory had a way of constructing constant nodes of a type belonging to another theory.
(2) Remove deprecated infrastrastructure for a "neverIsConst" function, which was adding about a 1% of the runtime for some SyGuS benchmarks.

This makes SyGuS for some sets of benchmarks roughly 3% faster.

Eliminate Expr-level calls in TypeNode (#3562)

Add support for set comprehension (#3312)

Disable check-synth-sol in regression with recursive functions (#3560)

 FP converter: convert: Use std::vector as instead of std::stack. (#3563)

The word-blasting function `FpConverter::convert` used a `std::stack` with `deque` as an underlying data structure (default) for node traversal. Previous experiments suggested that using `std::stack<T, std::deque<T>>` performs worse than using `std::vector<T>`, and we decided, as a guideline, to always use `std::vector` for stacks: https://github.com/CVC4/CVC4/wiki/Code-Style-Guidelines#stack.

This PR refactors `FpConverter::convert` to use `std::vector`. Runs on all incremental and non-incremental FP logics in SMT-LIB showed a slight improvement over the previous (`std::stack<T, std::deque<T>>`) implementation, and an even greater (albeit still slight) improvement over using `std::stack<T, std::vector<T>>`.

Make CEGIS sampling robust to non-vanilla CEGIS (#3559)

Fix Unif+PI algorithm with symbolic unfolding (#3558)

Use the node-level datatypes API (#3556)

Fixes for regressions (#3557)

Fix CEGIS refinement for recursive functions evaluation (#3555)

Activate node-level datatype API (#3540)

Do not substitute beneath arithmetic terms in the non-linear solver (#3324)

Support symbolic unfolding in UNIF+PI (#3553)

Incorporate rewriting on demand in the evaluator (#3549)

Fix ufho issues (#3551)

Allow unsat cores with sygus inference (#3550)

Disable sygus inference when combined with incremental and proofs (#3539)

Fix case of uninterpreted constant instantiation in FMF (#3543)

Fixes #3537.
This benchmark triggers a potential unsoundness caused by instantiating with an uninterpreted constant (which is unsound).

Make theory rewriters non-static (#3547)

This commit changes theory rewriters to be non-static. This refactoring
is needed as a stepping stone to making our rewriter configurable: If we
have multiple solver objects with different rewrite configurations, we
cannot use `static` variables for the rewriter table in the BV rewriter
for example. It is also in line with our goal of getting rid of
  singletons in general. Note that the `Rewriter` class is still a
  singleton, which will be changed in a future commit.

[Regressions] Require proof support for abduction (#3546)

Simplify rewrite for character matching (#3545)

Use str.subtr in str.to.int/int.to.str reduction (#3544)

Previously, we were using UFs to encode substrings in the
`str.to.int`/`int.to.str` reductions. Our experiments have shown,
however, that using `str.substr` is more efficient instead.

Throw exception instead of warning for approximate models (#3542)

Add lemma for str.to.int/int.to.str (#3541)

This commit adds a lemma to our encoding of `str.to.int` and
`int.to.str` that relates the integer value in the encodings to the
value of partial results.

Optimize the rewriter for DT_SYGUS_EVAL (#3529)

This makes it so that we don't construct intermediate unfoldings of applications of DT_SYGUS_EVAL, which wastes time in node construction. It makes the sygusToBuiltin utility in TermDbSygus use this implementation.

New algorithm for interpolation and abduction based on unsat cores (#3255)

Add ExprManager as argument to Datatype (#3535)

[proof] Eliminate side-condition from ER signature (#3230)

* [proof] Eliminate the side condition in er.plf

By tweaking the axioms a bit, I got rid of the lone SC in the Extended
Resolution signature.

* [proof] Changed er_proof.cpp in line with signature

The new signature requires slightly different proof printing.

* [proof] clang-format er_proof.cpp

* Fix tests

* [proof] Actually delete the SC

* Apply suggestions from code review

Co-Authored-By: yoni206 <yoni206@users.noreply.github.com>
* Add LFSC-checking unit test for ER proof

* Gate the lfsc invocation on the build system

* Properly gate the lfsc check on the build system

* gate the plf_signatures forward def on the build system

contrib: Setup all dependencies in deps/ directory. (#3534)

Introduce the Node-level Datatypes API (#3462)

This adds classes corresponding to the Node-level Datatype API "DType", which is a specification for a datatype type. It does not enable the use of this layer yet. A followup PR will update the Expr-level Datatype to use the Node-level code, which is currently verified to be functional on this branch: https://github.com/ajreynol/CVC4/tree/dtype-integrate. Futher PRs will make the internal (Node-level) code forgo the use of the Expr-layer datatype, which will then enable the Expr-layer to be replaced by the Term-layer datatype.

Most of the documentation for the methods in DType/DTypeConstructor/DTypeSelector was copied from Datatype/DatatypeConstructor/DatatypeConstructorArg.

Make nonlinear solver intercept model assignments from the linear arithmetic solver (#3525)

Refactor mode options for Unif+PI (#3531)

Bi-directional unrolling of R* regular expressions (#3532)

Add mkOp for a single Kind (#3522)

Fix the subtyping relation for functions (#3494)

New grammar construction modes for SyGuS (#3486)