Implement --no-strings-lazy-pp as a preprocessing pass (#5777)

This option eliminates extended functions in strings eagerly. This was incorrectly done at ppRewrite previously, which should not add lemmas. Instead, this makes this technique into a preprocessing pass. To do this, the interface for the strings preprocessor was cleaned to have fewer dependencies, and made to track a cache internally.

Fixes #5608, fixes #5745, fixes #5767, fixes #5771, fixes #5406.

Updates to theory preprocess equality (#5776)

This makes 3 changes related to arithmetic preprocessing of equalities which revert to the original behavior of master before a129c57.

For background, the commit a129c57 unintentionally changed the default behavior slightly in 3 ways (each corrected in this PR), which led a performance regression on QF_LIA in current master.

The 3 fixes are:
(1) Rewrite equalities should be applied as a post-rewrite, not a pre-rewrite in the theory-rewrite-eq preprocessing pass. This is particularly important for equalities between ITE terms that contain other equalities recursively.
(2) theory-rewrite-eq should apply after rewriting and just before the normal theory preprocessing.
(3) The arith-brab test should call ppRewrite on the arithmetic equality it introduces, as it has a choice of whether to eliminate the equality before the lemma is sent out.

Split eager solver from strings solver state (#5775)

This splits the eager solver from solver state. The solver state contains the EqcInfo data, while the eager solver is responsible for populating it.

This is in preparation for adding new techniques to the eager solver.

No behavior changes in this PR, only reorganization.

Add unit test for api getInterpolant() -- issue #5593 (#5772)

The pull request addressed issue #5593 for adding an unit test.

Do not call ppRewrite on Boolean equalities (#5762)

Was causing arithmetic to process a Boolean equality when --arith-rewrite-equalities is true.

Fixes #5761.

google test: expr: Migrate node_black. (#5764)

google test: Use ASSERT_* instead of EXPECT_*. (#5765)

Use ASSERT instead of EXPECT for consistency. There's no real benefit
for us to use EXPECT -- the main difference is that within a test,
EXPECT failures do not terminate the test, while ASSERT failures do.

This further fixes a minor issue in theory_sets_type_rules_white.h
(which is still not migrated to google test yet).

Foreign theory rewrite option (#5763)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the third and final step. It adds the user-facing option that turn this feature on, as well as regression tests.

Merge theory registrar and theory proxy (#5758)

The motivation of this PR is to make TheoryProxy the single point of contact to TheoryEngine from PropEngine.

This merges the helper class TheoryRegistrar into TheoryProxy.

Further simplifications in preparation for removing Expr layer (#5756)

This deletes variable flags from NodeManager::mkVar and moves ExprManager sort flags to NodeManager.

These flags are used for determining when a variable or sort should be printed via the old dump infrastructure. The old dump infrastructure is simplified in this PR accordingly.

This PR should preserve behavior of the previous dumping with a minor exception that the internal trace "declarations" will also included symbols introduced from define-fun. This will be further refactored later. This is in preparation for removing the includes expr.h/expr_manager.h from node_manager.h.

Remove extended rewrite for arithmetic (#5760)

This rewrite is no longer needed since our philosophy on rewriting extended arithmetic symbols has changed (we employ aggressive rewriting for extended arithmetic symbols in the normal rewriter). Moreover there was a soundness bug in the extended rewriter for division and mod by 0.

Fixes #5737, fixes #5740.

Strings arith checks preprocessing pass: step 2 (#5750)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the second step. It includes the implementation of the main function, as well as unit tests for it.

A subsequent PR will add a user-level option that will turn on this preprocessing pass, as well as regression tests.

Fix issue 5513 (#5757)

Fix issue5513 by throwing an exception for unsupported bag operators

Rename getAntecedent to getPremises (#5754)

Changes:

renamed d_new_skolem to d_newSkolem
renamed d_ant to d_premises (antecedent is usually used with consequent, and premise is used with conclusion)

[proof-new]  Implementing getProof in the API and SMT engine (#5751)

A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).

Add bags inference generator  (#5731)

This PR adds inference generator for basic bag rules.

bv-to-int: avoid binarizing nodes twice (#5749)

In bv-to-int, we first binarize the applications of associative-commutative operators (like bvadd etc.).
With this PR, we first check whether we already binarized a node, and only if we didn't, we perform binarization.

Make sure polynomials are properly factorized in nl-cad (#5733)

CAD theory (used in nl-cad) requires that polynomials are properly factorized (a finest square-free basis). This PR replaces usage of raw std::vector by a new wrapper PolyVector that ensures proper factorization whenever a polynomial is added. This fixes one piece of code that omitted factorization, leading to soundness issues as in #5726.
Fixes #5726.

Remove dependency on expression layer in TPTP parser (#5753)

Fix warning in TPTP parser  (#5752)

strings arith checks preprocessing pass: step 1 (#5747)

We are adding a preprocessing pass that simplifies arithmetic constraints related to strings.
For example, len(s) >= 0 would be replaced by true.
This will make use of CVC4::theory::strings::ArithEntail::check.

This PR is the first step. It only includes the preprocessing pass infrastructure, with an empty implementation of the main function StrLenSimplify::simplify. It also adds the pass to the registry.
The implementation of this function is not complicated, but is left for a future PR in order to keep the PR short.

Future PRs will include an implementation of the main function, tests, and a command line option to turn on the pass.

Add new interfaces to term formula removal and theory preprocess (#5717)

This is in preparation for lazy lemmas for term formula removal.

Adding str.len to triggers (#5746)

This PR adds str.len to symbols that are considered for instantiations.
It is motivated by a benchmark that originated from Boogie.
A minimized version of that benchmark is added as a regression.

Remove a few miscellaneous references to the expr layer (#5661)

Leftover from a development branch.

[proof-new] Only use old proofs for unsat cores if no proof new (#5725)

Now the old proofs are used for unsat cores only if proofNew is disabled. Later commits will generate unsat cores from the new proofs when requested. Eventually we will compare them and when we confirm the new unsat core generation is better we will delete the old one.

This also does some minor refactoring in some preprocessing. No behavior is changed.

Dumping unsat cores after check-sat-assuming/QUERY (#5724)

Previously we were not printing unsat cores when passing the option to dump them if we used the check-sat-assuming command or the QUERY command. This commit fixes this.

It also kills the redundant dump-synth option, as it simplifies a bit what is going on in the command executor.

Add option to track and notify from CNF stream (#5708)

This adds functionality to CNF stream to allow e.g. TheoryProxy to be notified when a formula is asserted (not just literals).

This will be required for SAT relevancy.

No behavior changes in this PR.

Remove quant EPR option (#5716)

This was an experimental option used in combination with separation logic.

[proof-new] Adding a manager for the new unsat cores (#5723)

Based on proof nodes of refutations.

(proof-new) Miscelleneous fixes from proof-new (#5714)

Add proofs for nonlinear sign lemmas. (#5707)

This PR adds proof support for NL_SIGN lemmas.

Minor simplification to Theory::theoryOf (#5719)

This removes the special case of constants based on the observation that the theory that owns the type of a constant and the theory that owns its kind always should be the same.

This should lead to a small (maybe 1%) performance improvement, as this method is run ~191M times in our coverage build.

Delete duplicated code (#5718)

Move slow regression to regress3 (#5715)

Make theory preprocess rewrite equalities a preprocessing pass (#5711)

Some theories rewrite equalities during ppRewrite. An example is arithmetic with the option arith-rewrite-eq, which rewrites (= x y) to (and (>= x y) (<= x y)) during theory preprocessing.

This PR makes it so that ppRewrite is only called on equalities in preprocessing, during a new preprocessing pass "TheoryRewriteEq". On the other hand, ppRewrite is never called on new equalities generated in lemmas from TheoryEngine.

In detail, the motivation for this change:

(1) Rewriting equalities during ppRewrite is dangerous since it may break invariants wrt theory combination. In particular, equalities in splitting lemmas originating from theory combination must not be theory-preprocessed, or else we may be non-terminating or solution unsound. This can happen if a theory requests a split on (= x y) but is not notified of this atom when another theory rewrites (= x y) during ppRewrite.

(2) After this PR, we can simplify our policy for all lemmas generated, in particular, we can say that all lemmas must be theory preprocessed before their literals are asserted to TheoryEngine. This is now possible as the invariant cannot be broken (theoryRewriteEq is relegated to the preprocessor, which is only applied once). This will make LemmaProperty::PREPROCESS obsolete, which in turn will simplify several lemma caches for nonlinear and quantifiers. It will also significantly simplify proof production for the theory preprocessor (which maintains two stacks of utilities for preprocessed vs non-preprocessed lemmas).

(3) Simplifications to the above policy will make it significantly easier to implement theory-preprocessing apply when literals are asserted. It is currently not possible to implement this in a coherent way without tracking which literals were a part of lemmas marked as "do not theory-preprocess".

Remove preregister instantiation heuristic (#5713)

This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.

Add proof for pi bound lemma (#5709)

This PR adds proofs for lemmas that introduce bounds on the constant representing pi.

Have unsat core regression agnostic to number of assertions in core (#5712)

Changing our unsat core infrastructure may change the cores we produce. This can be problematic for regressions that hardcode the number of assertions we get (such as this one). This commit changes such a regression to rather expect any core. It is motivated by exactly the previously described issue occurring after using the new proof infrastructure to generate unsat cores, which yielded a smaller core.

Kudos to @4tXJ7f for the sed magic.

Move ownership of theory preprocessor to TheoryProxy (#5690)

With this PR, TheoryEngine is independent of theory preprocessing. All theory preprocessing is handled at the level of PropEngine.

No significant behavior changes in this PR.

The next step will make theory preprocessing not mandatory in preprocessing, and optionally done instead at the time when literals are asserted to TheoryEngine.

Add proof for sine shift lemmas. (#5710)

This PR adds proofs for the sine shift lemmas that add equivalent instances of the sine function where the argument is in its "main phase" between minus pi and pi.

(proof-new) Make nl-ext factoring lemmas proof producing. (#5698)

This PR adds proofs for the lemmas from the nonlinear factoring check.

Eliminate recursion from the internals of term formula removal (#5701)

This makes all recursion (applying term formula removal on lemmas introduced by term formula removal) optionally happen at the top level call.

This is in preparation for making term formula removal lazier, in which case we will only apply one step of term formula removal at a time.

One QF_UFNIA regression times out due to changing the search, an option is changed for this benchmark.

Fix issue with selector triggers (#5689)

Code could segfault if the number of wrongly applied selector applications was different from correctly applied ones.

(proof-new) Setup proof infrastructure for transcendental solver (#5703)

This PR introduces the infrastructure for adding proofs to the transcendental solver:

a CDProofSet to easily create new proofs
a proof checker

Simplify internal API for sygus (#5687)

This makes simplifications to the internal sygus API now that the SmtEngine interface is independent of parsing.

Add proof checker for nl tangent lemma (#5704)

This PR is a follow-up to #5700 which lacked the proof checker for the proof that was added for nonlinear tangent plane lemmas.

Bugfix: proofs for props of non-normal arith lits  (#5702)

Arith has a normal form for literals, which the rewriter computes.

Nonetheless, arith sometimes gets (and ultimately propagates) non-normal
literals. It normalizes them internally and goes about its business.

However, when asked for an explanation, it must prove the non-normal
literal, rather than the normal one.

Also includes a regression for the bug, courtesy of Andy.

Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

(proof-new) Add proof for tangent plane lemmas (#5700)

This PR adds a proof for the tangent plane lemmas from nl-ext.
As this lemma uses some insight about the tangent plane of a multiplication term, this PR adds a new proof rule.

Add proof for split zero check. (#5699)

This PR adds a proof for the nl-ext check to split at zero. As we can use the SPLIT rule, this requires no new proof rule.

(proof-new) Minor updates to term conversion proof generator (#5691)

Minor updates to term conversion proof generator

Always consider rewritten lemmas for caching. (#5696)

The TheoryInferenceManager cached lemmas as they came in. This PR always rewrites before consulting the cache, making caching more consistent and robust. This change is coming in from proof-new.

(proof-new) Prepare nonlinear extension and nl-ext for proofs. (#5697)

This PR prepares the nonlinear extension itself and the nl-ext part for proofs. In particular

    we add a proof checker for nl-ext
    we add a CDProofSet for nl-ext

Simplify term formula removal interface (#5695)

This no longer needs some methods that were previously used specifically for ITE preprocessing and check-model.

Simplify and fix check models (#5685)

Currently --check-models is implemented by replaying several preprocessing steps, including theory-specific expand definitions, and then checking whether the result evaluates to true.

However, by having --check-models rely on complex preprocessing machinery defeats its purpose, as these steps are part of its trusted base.

Moreover, issue #5645 demonstrates that this may lead to spurious errors where we incorrectly conclude that an input assertion is false, when it is not.

This PR significantly simplifies --check-models so that it only relies on define-fun expansion + rewriting + evaluation. This ensures that --check-models is "sound" i.e. it does not falsely report a formula as evaluating to false. As a consequence, this makes check-models give warnings more often, i.e. when partial operators are involved, thus -q is added to silence warnings on some regressions.

A followup PR will use a satisfiability check on the input formula post-expand-definitions to properly implement a trustworthy version of check-models that is robust for partial operators.

Fixes #5645.

[proof-new] Only use old proof code for unsat cores if new proofs are off (#5688)

This is so that eventually we can compare the performance of the old unsat cores vs the new ones.

Simplify preprocessing (#5647)

This simplifies preprocessing so that the only call to theory-preprocess and ite-removal is at the very end. (One exception is early-theory-pp which is used by default in combination with ite-simp to maintain the performance on QF_LIA/nec).

This is in preparation for making theory preprocessing happen lazily, post-CNF conversion.

@HanielB has done SMT-LIB performance runs, see below.

Mark quantifier instantiations as needs justify (#5684)

This avoids a solution soundness issue when disabling all NL strategies and using --nl-rlv=always.

Simplify synth-fun printer (#5682)

Simplifies synth-fun printing to assume that the function-to-synthesize should be printed with the proper name and return type.

Renamed InferInfo::getAntecedant to InferInfo::getAntecedent (#5683)

Renamed InferInfo::getAntecedant to InferInfo::getAntecedent

(proof-new) Use bound variable manager (#5679)

This uses BoundVarManager for several key places where bound variables are introduced, including for array extensionality witness terms, string preprocessing, quantifiers rewriting, and skolemization.

This is motivated by making certain steps in solving deterministic for the sake of proofs, and gives a more consistent pattern in general for constructing bound variables.

Move ownership of term formula removal to theory preprocessor (#5670)

This is work towards refactoring ITE removal (more generally, term formula removal) so that it happens at a configurable time, preferably post-CNF conversion.

This moves the TermFormulaRemover to the TheoryPreprocessor and changes several interfaces as a consequence of this move.

The next step will move the TheoryPreprocessor inside prop::TheoryProxy.

There are no behavior changes to solving in this PR. One aspect of CheckModels is simplified.

Use uint64 utility when parsing tuple selectors in smt2 (#5681)

The smt2 parser is now 100% independent from the Expr-layer.

Move trigger trie to own file (#5680)

Also updates minor things to meet coding standards and makes it so that children in the trie are not dynamically allocated.

Improvements related to quantifiers printing (#5678)

Also fixes a bug where patterns would be printed with the wrong scope (that included the bound variable list).

Proper expand definitions for sets (#5676)

In the new view, expandDefinitions is used for eliminating partial operators and is not called during solving, and ppRewrite is called during preprocessing.

For sets, choose is a partial operator that should be applied in expand definitions, and in ppRewrite. On the other hand, is_singleton should not be expanded in expandDefinitions since it is not a partial operator, so it should only be handled in ppRewrite.

It also removes some outdated documentation regarding expandDefinitions with universe set, which is now handled by preventing universe set from occurring in solved substitutions.

This is in preparation for refactoring check-model.

Consolidate basic sygus utilities regarding sygus conjectures (#5421)

This is required for new work on generalizing CAV 2015 single invocation techniques.

It adds a new system of marking solutions for synthesis conjectures as attributes, which will be used as a way of eliminating functions from a conjecture while still preserving their solution in a response to check-synth.

Fix datatypes compute ground value (#5671)

We were using the wrong cache on one call, leading to non-constant values being enumerated.

Fixes #5659, for that benchmark, CVC4 now answers "unknown".

Remove bv divide by zero option (#5672)

This is required to avoid failures in the planned refactoring of check-models.

This removes the SMT-LIB 2.5 semantics option for bvdiv/bvrem.

It still remains to merge the BITVECTOR_UDIV / BITVECTOR_UDIV_TOTAL kinds, calling the total version "BITVECTOR_UDIV", and analogously for UREM.

FYI @barrettcw

Add getters to retrieve constants from api::Term (#5677)

This PR adds method to obtain constant values from api::Term that are either integers or strings.

[proof-new] Making the CDCL(T) Minisat proof producing (#5669)

This closely follows the old proof code in terms of where Minisat is hooked to the SatProofManager, other than a few places like registering removed clauses and removal of redundant literals. Note that this together with the thorough handling from SatProofManager makes the new SAT proofs perceptibly more robust than the old ones.

This PR also adds some traces to better track what Minisat does.

[proof-new] Make prop engine proof producing (#5667)

Properly implement datatype selector triggers (#5624)

This ensures that datatype selectors are properly handled as triggers in E-matching.

This is challenging since selectors in quantified formulas are of kind APPLY_SELECTOR but are theory-preprocessed to APPLY_SELECTOR_TOTAL/APPLY_UF. Hence, we must match on 2 possible operators, and ones that do not match the operator of the trigger. This adds a custom candidate generator for this case.

It also removes a deprecated option that is no longer used (in part due to our use of shared selectors).

This is in preparation for further work on optimizing cvc4 on benchmarks from Facebook.

Note that there is not a convienient way to call expandDefinitions currently (which is required to get the proper operators to match). This PR calls smt::getCurrentSmtEngine() to do this, although we should find a better solution soon, e.g. adding expandDefinitions to the rewriter.

FYI @barrettcw

[proof-new] Updating interfaces between prop engine and minisat (#5664)

This is in preparation to make the prop engine proof producing. This PR also renames "DPLLSatSolverInterface" to the more appropriate name "CDCLTSatSolverInterface".

Note that most of the diff is due to formatting of the previously super ad-hoc formatting of the minisat code.

(proof-new) Add bound variable manager (#5655)

This is a common utility for constructing canonical bound variables.

Fix and improve evaluator (#5563)

This fixes a segfault in the evaluator for substitutions of the form x -> t where t is not constant.

This consolidates 2 cases where we did not evaluate children (when we are variable or are an application term with an unevaluated child). This was problematic previously since we would access children of currNode instead of currNodeVal.

This also makes our handling of APPLY_UF more consistent, so that it is added to the main switch statement.

Fix SAT-context dependent issue in strings preregistration (#5564)

This makes preregistration of terms SAT-context dependent in strings instead of user-context dependent.

Fixes #5547.

This is required to avoid model unsoundness on sequence benchmarks, as demonstrated in that issue.

It furthermore impacts how we have been handling theory combination with arithmetic for str.len and impacts how propagation is setup for the strings equality engine.

I will do performance testing on this PR.

Flush statistics through NodeManager in SmtEngine (#5652)

This removes the dependency on the Expr layer from src/main.

This requires moving the flushing of NodeManager statistics within SmtEngine.

This is a temporary solution until we have a permanent solution for statistics.

bv-to-int: new tests from an issue (#5654)

#5293 pointed to assertion failures when employing --bv-to-int, starting from commit 94e3d9a.
The bug is not reproduced on current master, and so we would have this PR close #5293 .
This PR adds the benchmarks from #5293 .

 [proof-new] Updating theory proxy to new proof infrastructure (#5653)

Fix length assumption for deq norm emp rule (#5623)

There is an assumption that is not guaranteed to hold in this rule, thus we should not try to explain in the equality engine.

Fixes #5611.

Note this inference was not previously covered in our coverage build.

Refactor KindMap (#5646)

The KindMap class is only used in the EqualityEngine and implements way more than necessary.
This PR removes all the functionality that is never used.

google test: expr: Migrate node_algorithm_black. (#5643)

Refactor regressions (#5639)

This adds a net +82 regressions to regress[0-2] and adds several additional disabled regressions to regress3 and regress4. This involved fixing the status on several regressions, and ensuring CMakeLists.txt includes all files (exactly once) in the test/regress/ subdirectory.

It also moves several regressions to the proper regression levels (those that take >30 seconds in debug are moved to regress3+).

google test: expr: Migrate kind_black. (#5634)

Fixed a bunch of clang warnings. (#5637)

Fix compiler warnings. (#5644)

(proof-new) Make theory preprocessor proofs self contained (#5642)

Previously, there was a block of code in TheoryEngine::lemma for processing the proofs from theory preprocessing.

It is much cleaner if this block was self contained in TheoryPreprocessor.

This is required for the planned move of TheoryPreprocessor from TheoryEngine -> PropEngine.

google test: expr: Migrate kind_map_black. (#5640)

kind_map: Remove unused Accessor class. (#5641)

google test: expr: Migrate attribute_white. (#5632)

Make decision engine independent of AssertionsPipeline (#5626)

This PR makes decision engine independent of AssertionsPipeline, which consequently allows some of the key PropEngine interfaces to be consolidated. It also modifies PropEngine to take TrustNode for assertLemma, which is the first step for making PropEngine manage proofs from TheoryEngine.

This is in preparation for modifying the interplay between PropEngine, TheoryEngine, TheoryPreprocessor, and new proposed SAT relevancy heuristic.

There are no intended behavior changes in this PR.

Marking "major" since this impacts several current directions (including proof-new integration, lazy theory preprocessing, SAT relevancy).

Remove obsolete regressions (#5633)

This removes benchmarks for the following reasons:

- regress1/arith/arith-int are removed since there are many similar regressions (10 from this set are already enabled)
- bitvector cvc benchmarks are removed since their *.smt2 benchmarks are enabled
- other benchmarks are removed due to features we do not plan to support
- one placeholder benchmark is removed

google test: context: Migrate context_white. (#5630)

google test: context: Migrate context_white.

Split initial exp lemma into separate lemmas. (#5622)

This PR refactors the initial lemmas for the exponential function, very similar to the sine lemmas.

Delete obsolete unit tests for Expr and ExprManager. (#5631)

This is already in preparation for removing the Expr layer.

Ensure CEGQI is applied for parametric datatypes when applicable (#5628)

Previously was a bug computing the argument types of parametric datatypes.

Do not check FP at last call if not necessary (#5627)

This makes the theory of floating points not request a last call effort check, if that call is known to do nothing.

This should make CVC4 (more) agnostic to whether --symfpu is enabled during configuration.

ite_utilities: Fix infinite loop in compressTerm. (#5629)

Fixes #4610.

update doc (#5619)

The current help message for --bv-div-zero-const only mentions bvudiv (in which the result is -1) and not bvurem (in which the result is the first argument).
I think this is a bit misleading, because in practice, this option controls also the behavior of bvurem:
CVC4/src/theory/bv/theory_bv.cpp

Line 134 in 0309ef4

 if (options::bitvectorDivByZeroConst())
This PR is an attempt to provide a more accurate help message.

google test: context: Migrate context_mm_black. (#5592)