Infrastructure for tautological literals in nonlinear solver (#3795)

Work towards CVC4/cvc4-projects#113 and #3783.

This PR adds the ability to mark certain literals as being tautological, since they can be assumed to hold in all models. This is important for internally generated literals whose purpose is to guide models generated by the linear solver but should not hinder our ability to answer "sat".

This PR is required for further refactoring of check-model for transcendental functions.

Use side effect utility for non-linear lemmas (#3780)

Fixes #3647.

Previously, when doing incremental linearization for transcedental functions, we would add points to the list of secant points at the time when linearization lemmas were generated. However, our strategy has been updated such that lemmas may be abandoned (say in the case that a higher priority lemma is found). Thus, our list of secant points had spurious points corresponding to lemmas that weren't sent. This led to assertion failures, and likely led to gaps in our linearization, hindering our ability to say sat/unsat.

This PR introduces a "lemma side effect" class to ensure that modifications to the state of the nonlinear solver are in sync with the lemmas we send out.

Fix regression (#3827)

More fixes for printing sygus commands (#3812)

Towards v1 -> v2 sygus conversion.

This makes several fixes and improvements related to printing sygus commands:
(1) The logic is extended with LIA, DT, UF internally during setDefaults instead of during parsing. This is the correct place for this extension of the logic since it should be applied regardless of the parser. 5 existing logic bugs were discovered as a result of this in regressions, which are fixed by this PR.
(2) Ensures that terms in sygus grammars are printed without letification, since this is prohibited in sygus. Notice the formulas printed by constraints need to be letified (otherwise we can't convert large lustre benchmarks). Thus, the letification threshold should determine this but always be overridden for grammar terms.
(3) Ensures final options are set for all sygus-specific commands, which follows the standards prescribed by sygus v2 (all set-* commands come before other commands).

Basic support for regular expression complement (#3437)

Fixes #3408 .

Adds basic rewriter, parsing, type checking and implements the required cases in regexp_operation.cpp. It also adds some missing documentation in regexp_operation.h

Refactor type ascriptions in the parser (#3825)

Towards parser migration.

This consolidates two blocks of code (cvc/smt2) that do type ascriptions to a utility function in the parser. It updates this function to use the new API.

This code will be further refactored when the interface for parametric datatype constructors is further developed in the new API.

Minor improvement to ParseOp (#3808)

Use default consts when not using any const during grammar normalization (#3807)

Fixes #3802.

If we decide not to add the any constant constructor due to insufficient cegqi algorithms (or if the sort is Boolean), then we should add the default constants for a sort.

Fix node arity issue in reduction of int2bv (#3777)

Move equivalence class info to its own file in strings (#3799)

Code move only, no updates to behavior or content of code in this PR.

Support for witnessing choice in models (#3781)

Fixes #3300.

This adds an option --model-witness-choice that ensures that choices in models are of the form (choice ((x Int)) (or (= x c) P)), which is helpful if the user wants to know a potential value in the range of the choice.

Remove portfolio leftovers (#3821)

Commit 1c09572e0e2031519a103caa2a4af0d9bd34a9c5 removed the portfolio
build but there were some leftovers. This commit removes them.

Minor cleaning of smt2 parser (#3823)

Towards parser migration, will make the diff of the eventual conversion a bit smaller.

Embed mkAssociative utilities within the API. (#3801)

Towards parser/API migration.

Sets & Relations Java example (#3816)

Fixes [(Bugzilla #677)](https://github.com/CVC4/cvc4-projects/issues/25).

Sets & Relations Java example (#3816)

remove redundant includes (#3815)

I came across these two redundant includes in theory_uf.h and removed them.

bv_to_int preprocessing pass

Introduces a preprocessing pass that translates bv problems to integer problems.

Fixes for quantifiers documentation (#3811)

Minor fixes discovered during development of sygus-inst.

Utilities for words (#3797)

This adds a utility file for handling operations over constant "words" (this will eventually generalize string or sequence constants). This is work towards CVC4/cvc4-projects#23.

Also improves documentation in regexp.h.

Convert parser input interface to api::Term (#3809)

Fix bugs related to printing Sygus commands (#3804)

With this commit, most Sygus problems should print correctly. The current printing functionality was tested on 158 Sygus regress files (0, 1, and 2) and 153 of them were printed in Sygus2 format and contained "(check-synth)". The printing functionality was tested again on the generated files and gave almost the same results.

Add missing functions to new C++ API (#3769)

Make lambda rewriter more robust (#3806)

The lambda rewriter was not robust to the case where the lambda of the
array representation contained a disequality, e.g. `not(x = 1))`. It
would process it as `ite(not(x = 1), true, false)` instead of `ite(x =
1, false, true)`, which meant that it wasn't able to turn it into an
array representation when checking const-ness. Additionally, the
rewriter had issues when the lambda was of the form `ite((= x c1), true,
(= y c2))` (after turning it into an array and then into a lambda)
because it is expecting the false branch of the `ite` to not contain `y`
variables, making it non-constant despite the array being constant. This
commit solves that issue by normalizing `ite(not(c), x, y) ---> ite(c,
y, x)`.

Minor refactoring of equality notifications (#3798)

Towards moving functionalities to proper places in strings. Also removes a block of code that was duplicated as a result of splitting the ExtfSolver.

RIP th_lra.plf (#3796)

Rest in Peace, old LRA signature.

 Move check memberships to reg exp solver (#3793)

There was previously a function in TheoryStrings to make the proper call to checkMembership. In the refactored code, this is no longer necessary and the interface to RegExp can be simplified.

Move cardinality inference scheme to base solver in strings (#3792)

Moves handling of cardinality to the base solver, refactors how cardinality is accessed.

No intended behavior change in this commit.

Dump boolean propagations and conflicts for decision tree org-mode viewer (#3788)

PR #2871 added trace tags for dumping the decision tree in org-mode format. However, it only dumped theory propagations/conflicts. This could be confusing because it would appear to backtrack without reaching a conflict (but actually the conflict was at the propositional level). This commit also adds dumping of boolean propagations and conflicts.

Switch to th_lira.plf (#3741)

Switches arith_proof.cpp from th_lra to th_lira.

Changes:

Eliminate the d_realMode hack.
instead: modify printOwnedTermAsType prints as integers OR
reals, depending on expectedType.
simultaneously: write printOwnedTermAsType more concisely
also: reimplement printOwnedSort.
Change to the LIRA axioms:
Because they reason about bound types using side conditions, we
no longer need to worry about choosing the correct strictness for
our axiom.
This allows us to cut out a lot of code, rewriting & shrinking
printTheoryLemmaProof.
They also have different names.
This requires us to change a lot of string literals
enable proof-checking for many tests.

New C++ API: Remove TOTAL kinds. (#3794)

Simple changes towards unicode string standard (#3791)

This updates --lang=smt2.6.1 with the minor syntactic differences from the current syntax and the standard here: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml.

The next steps will be to address the more invasive changes required to support the standard.

Adding checks to the validation of 'bv-sat-solver' to ensure that the selected SAT solver is compiled-in (#3771)

Split extended functions solver in strings (#3768)

Remove IntReal tightening axioms from th_lira.plf (#3787)

Remove front-end support for Chain (#3767)

Remove unused code (#3782)

Minor removals (#3786)

Found while working on parser migration of datatypes.

Remove parser from bindings (#3779)

resource manager: Add statistic for every resource. (#3772)

This commit adds statistics for all resource steps. A resource statistic is incremented by 1 if the resource is spent (via `spendResource`).

Fixes #3751.

Fix symmetry breaking for multiple sygus types (#3775)

Add Python bindings using Cython -- see below for more details (#2879)

Delay enumerative instantiation if theory engine does not need check (#3774)

Change Record to shared_ptr (#3778)

Fix approximate bounds for transcendental functions whose model values rewrite (#3747)

* Fix bounds for negative sine apps

* Format

* Comment

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

Change datatype selector/constructor/tester to terms (#3773)

Add missing kinds for the new API (#3757)

Option to limit the number of rounds of enumerative instantiation (#3760)

 Fix soundness bug in reduction of integer div/mod (#3766)

This was introduced 7 years ago in https://github.com/CVC4/CVC4/commit/9098391fe334d829ec4101f190b8f1fa21c30752.

This impacted any case of integer div/mod of the form `(mod c t)` or `(div c t)` where c is a constant and `t` is not.

Fixes #3765.

Also improves `--dump=t-lemmas` trace to result in smt-lib compatible output, which was required for debugging this.

Using ParseOp in TPTP (#3764)

Support dumping Sygus commands. (#3763)

Fix simple issue with cache (#3762)

Add temporary global API conversion utilities. (#3759)

Activate reverse variant of F-Split inference (#3745)

This commit activates the reverse variant of the F-Split inference.

Disable regression (#3761)

Should fix recurring issue with nightlies.

Also fixes a warning.

Move proxy variables to InferenceManager in strings (#3758)

Remove quantifiers rewrite rules infrastructure (#3754)

Update sygus v1 parser to use ParseOp utility (#3756)

Forcing rewrite pass rather than asserting if formula has been rewritten (#3748)

This ensures that users or developers don't accidentally break the solver either via options or changing the SMT engine flow so that the formula is not rewritten up to a given point.

Const input for sygus print callback (#3755)

[Python] Properly destroy CVC4 object (#3753)

Rename Java package to edu.stanford.CVC4 (#3752)

Ensure ext rewrites for associative ops dont throw assertions for kind arities (#3681)

run_regression: Distinguish between timeout and failure. (#3750)

If --use-skip-return-code is enabled and a regression test times out it
will return EXIT_SKIP instead of EXIT_FAILURE.

Fix non-linear equality solving that involves mixed real/integer arithmetic (#3739)

* Fix non-linear equality solving that involves mixed real/integer.

* Format

* Fix

* Revert

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

cmake: Remove unused ENABLE_OPTIMIZED option. (#3749)

Fix term simplification based on entailment in quantifiers rewriter (#3746)

Update issue templates

Remove `--strings-binary-csp` option (#3743)

Refactor `CoreSolver::processSimpleNEq()` (#3736)

This commit refactors and documents `CoreSolver::processSimpleNEq()`.
This method processes equalities between normal forms.

Use example evaluation cache instead of sygus PBE  (#3733)

Implement LFSCArithProof::equalityType. (#3740)

Also, missed an armType use.

Add function for tightening literals (#3732)

* Add function for tightening literals

The function tightens a literal if it can be tightened, and prints a
proof of the result.

* Include a #include

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

cmake: Use ld.gold if available for faster link times. (#3738)

Add more IntReal predicates (#3731)

Fix rewrite rules sat regressions (#3734)

Quantifier rewrite rules are not robust to preprocessing within our check-model infrastructure. This disables check-model on 2 satisfiable rewrite rules regressions. Fixes nightlies.

Make "unknown" non-critical for unsat cores check (#3728)

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.