Split strings finite model finding strategy (#3727)

Split core solver from the theory of strings (#3713)

This splits the main procedure from Liang et al CAV 2014 to its own file, the "core solver" of theory of strings.

I have intentionally not updated or clang-formatted the code in core_solver.cpp since I would prefer this PR to involve as little change to behavior as possible (it is copied verbatim from theory_strings.cpp). Future PRs will clean this code up.

Interface for example evaluation cache utilities (#3726)

This adds interfaces in synth_conjecture for getting an ExampleEvalCache, per enumerator.
It also adds a specialization `checkRefinementEvalLemmas` of `getRefinementEvalLemmas` in the cegis module, which does evaluation on CEGIS refinement lemmas without structural generalization.  This function will be used as an alternative to `getRefinementEvalLemmas` for fast enumerators.

The next PR will update all utilities to use ExampleEvalCache instead of SygusPbe for evaluating examples.

Univeset Cardinality constraints for infinite types (#3712)

Refactor check-model handling in SmtEngine (#3723)

Propagate expected types through UF arguments (#3717)

Add `ArithProof::{printInteger,getLfscFunction}` (#3716)

Statistics for fast enumerator (#3699)

Example evaluation cache utility (#3698)

Fix exact sqrt (#3721)

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

Generalize containsQuantifiers to hasClosure (#3722)

Fix QF_NIA smt comp script (#3715)

Update INSTALL.md (#3714)

Co-authored-by: Mathias Preiner <mathias.preiner@gmail.com>

Articulate proof-related debug statements in arith (#3700)

--fp-exp: Better warning message. (#3709)

Fix header installation on MacOS. (#3660)

On MacOS sed -i requires a suffix to be set.

Split base solver from the theory of strings (#3680)

Revert semantic change from refactoring (#3711)

Regression tests for arithmetic proofs. (#3701)

* Add more arith proof regression tests

These tests are designed to test interesting cases of arithmetic proofs,
such as mixing integers and reals and tightening bounds.

Right now, they have the --no-check-proofs flag set, which prevents them
from testing the proof machinery. However, once we check that machinery
into master, we'll remove that flag, thus enabling the full effect of
the tests.

* A few comments explaining things.

* Add another tightening test

* Add new test to CMake

* No --no-check-models. There are no models anyway.

* Delete smt-lib-version, per Yoni

Increase regression test time limit to 1200s. (#3704)

Fixes #3565.

Fix corner case - might need to REWRITE_AGAIN (#3706)

Utility function for getting component types (#3703)

Minor fixes to regressions (#3702)

Fixes two issues in regressions, fixes regress1.

Fix cardinality of uninterpreted types when univset is not used (#3663)

* Fixed bug 3662

* format

* small change

* added bug3663.smt2 file

* throw Logic Exception

* throw Logic Exception

* ;EXIT: 1

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

Split on model values when repaired model from non-linear is inconsisent (#3668)

Fix invariant template inference for trivially infeasible conjecture (#3693)

Fix corner case of empty domains in bounded fmf (#3690)

Example inference utility (#3670)

Renaming '--bsd' to '--no-gpl' (#3609)

Signed-off-by: Andrew V. Jones <andrew.jones@vector.com>

Handle `expectedType` in TheoryProofEngine (#3691)

`TheoryProofEngine` now uses the `expectedType` optional argument.
  * When printing terms, it sets this for theories that it dispatches too
  * It occasionally asks theories for help determining the `expectedType` using `equalityType`, which has a sensible default implementation.
  * It is mindful of `expectedType` when using the let map.

I also moved to hpp function implementations into the cpp.

Allow PBE symmetry breaking with sygus stream (#3686)

Refactor relevance vectors for asserted quantifiers (#3666)

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)