Add NodeManager::mkOr() (#5360)

This PR adds a convenience method mkOr() just like mkAnd().

run_regression.py to fail on invalid requirements (#5264)

Currently, the following test is skipped when running ctest:

 ; REQUIRES: symfpuuuu
 ; EXPECT: sat
 (set-logic ALL)
 (assert true)
 (check-sat)
I think it is better for such a test to fail, because otherwise it might never run without anyone noticing (this almost happened to me here: c7e277b).

This PR makes such tests to fail by checking whether the REQUIRES value is valid. No regressions fail as a result.

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

Remove more uses of Expr (#5357)

This PR removes more uses of Expr, mostly related to UnsatCore.

It makes UnsatCore a cvc4_private object storing Node instead of Expr.

Fixes for unconstrained variables in nonlinear model (#5351)

This ensures that we explicitly mark x -> 0 as part of the arithmetic model coming from nonlinear for unconstrained variables x that nonlinear extension assumes to be 0.

This fixes #5348.

Convert symbol table from Expr-level to Term-level (#5355)

This task is left over from parser migration.

This PR also drops support for a case of symbol overloading, in particular symbols (constructors, selectors) for parametric datatypes cannot be overloaded. One regression is disabled as a result.

Split NlSolver in multiple subsolvers (#5315)

The NlSolver started as one place for nonlinear reasoning, but has grown significantly since. This PR splits the NlSolver class into multiple smaller classes.

Add rewrites for div/mod in the arithmetic rewriter (#5352)

This adds some basic rewrites for integer div/mod in the rewriter.

This is in preparation for improved preprocessing and rewriting for NIA problems with heavy use of div/mod.

run_regression: Add --skip-timeout option, lower timeout to 600 seconds.  (#5353)

Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)

This PR is part of migrating commands. DeclareSygusVarCommand and SynthFunCommand now call public API function instead of their corresponding SmtEngine functions. Those two commands don't fully initialize the solver anymore. Some operations in SygusInterpol::solveInterpolation, which creates an interpolation sub-solver, depend on the solver being fully initialized and were affected by this change. Those operations are now executed by the main solver instead of the sub-solver, which is not fully initialized by the time they are needed.

Add missing methods involving datatype sorts to the API (#5290)

This is required for migrating the parser's symbol table from Expr -> Term.

Disable --nl-cad option by default (#5350)

This PR disables the `--nl-cad` option by default. It was erroneously enabled with #5345 but leads to errors on, e.g., QF_NIA. Enabling for QF_NRA is done in set_defaults.

Enable --nl-cad by default (#5345)

This PR enables `--nl-cad` for QF_NRA (and QF_UFNRA) by default to improve nonlinear arithmetic solving.
Furthermore, it takes care of disabling it when libpoly is not available. It also adds a fix to the CadSolver that avoids incorrect SATs in the presence of theory combination.

Add DUPICATE_REMOVAL operator to bags (#5336)

This PR adds duplicate removal operator to bags (also known as delta or squash).
Other changes:

print MK_BAG operator as "bag" in smt2 instead of "mkBag"
renamed BAG_IS_INCLUDED operator to SUBBAG.

(proof-new) Add datatypes proof checker (#5340)

This adds the proof rules and proof checker for datatypes.

Send external equalities from collapse selector as lemmas (#5346)

In 20e58d4, a policy change was made for datatypes to keep more inferences as internal facts.

This leads to a crash (issue #5344) where the equality status of two BV terms is asked by TheoryDatatypes, where the TheoryBV was not informed of the term, as datatypes kept it internal.

This refines the policy further such that the collapse selector rule is processed as a lemma for terms of external type. The reason is that this rule may generate new terms of external type. Other rules like unification retain the internal fact policy, as they do not generate new terms.

Fixes #5344.

FYI @barrettcw

Fix issue 5271 (#5335)

This PR fixes #5271 by splitting on the equality of set members which ensures members are distinct when collectModelInfo is called.
Co-authored-by: Andrew Reynolds andrew-reynolds@uiowa.edu

[proof-new] Fix n-ary kind handling in EqEngine explanations (#5332)

Adding missing cases of kinds that are n-ary but whose partial applications are
not true terms in the equality engine. This in the case not only for APPLY_UF
but also for the APPLY_* kinds for datatypes.

Apply alpha equivalence to annotated quantified formulas (#5324)

Previously, alpha equivalence was not applied to quantified formulas with attributes, likely motivated by keeping alpha equivalent quantified formulas with different user patterns. It's not clear this is a good a idea. Moreover, this also implies that quantified formulas with user-provided names (which happens in e.g. Boogie benchmarks) also do not have alpha equivalence applied.

This makes it so that we apply alpha equivalence regardless of annotations.

FYI @barrettcw

Change datatypes lemma policy for equalities not coming from instantiate (#5325)

Recently, the policy for lemma vs fact changed for instantiate rule in datatypes to ensure that other theories were notified of terms having external finite type. This PR further refines the policy so that the instantiate rule is the only rule whose conclusion is an equality that is sent out as a lemma.

This means that equalities from unification and collapsing selectors are always kept internal. The justification for this is that the instantiate rule is applied for all terms with the proper policy, and hence it already covers all cases where we may need to introduce new terms.

Fix related to preregistering boolean term variables in strings (#5331)

We should only add trigger predicates for string predicates, and not arbitrary Boolean terms (which can now occur since we are handling parametric sequences).

This avoids a debug assertion failure reported on as a followup to #4370. In that benchmark BOOLEAN_TERM_VARIABLE was being added as a trigger predicate.

Use theoryof-mode=type for QF_NRA (#5326)

We've observed that our QF_NRA solving benefits significantly from --theoryof-mode=type across the board (of other options that influence QF_NRA solving). This PR sets type as the new default for QF_NRA solving.

Remove unused equality engine types (#5319)

This is leftover from the old proof infrastructure.

Fix issue 5309 (#5327)

This PR fixes #5309 by ensuring singleton terms are added to the model builder as representatives.

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

(proof-new) Make theory preprocessor user-context dependent (#5296)

Previously, theory preprocessing cache was manually cleared whenever the theory preprocess pass was run. However, proofs for theory preprocessing required to be alive for the remainder of the user context. This PR changes theory preprocessing so that both the cache and proofs in theory preprocessing are user-context dependent.

This PR also makes the theory preprocess pass proof producing.

(proof-new) Make circuit propagator proof producing (#5318)

This PR uses the proofs from #5301 to actually produce proofs from the circuit propagator.

Implement bags evaluator (#5322)

This PR implements NormalForm::evaluate for bags

(proof-new) Add arith proof macros file to CMake (#5321)

(proof-new) arith: dedup literals in flattenImpl (#5320)

TheoryArithPrivte uses flattenImplication to turn implications into
clauses. This commit ensures that said clause does not have duplicate
terms. This is important because when we write proofs related to the
clause, the proof machinery doesn't like duplicates.

(proof-new) Updates to lazy proof chain (#5317)

Support for a default proof generator, which is optionally not called recursively.

This is required for preprocessing.

Add operator MakeBagOp for constructing bags (#5209)

This PR removes subtyping rules for bags and add operator MakeBagOp similar to SingletonOp

Add finishInit for getInterpol and getAbduct. (#5316)

This PR removes d_subSolver from SygusInterpol class. findInterpol function now receives the sub-solver as input (possibly through solveInterpolation function). In addition, finishInit is now called for getAbduct and getInterpol functions in smt_engine.cpp.

(proof-new) Fixes for proofs in rewriter (#5307)

This PR fixes proofs in the rewriter so that we use attributes for marking whether a node has been rewritten with proofs instead of consulting the provided TConvProofGenerator for hasRewriteStep. This additionally marks TRUST_REWRITE steps if a rewriter happens to be nondeterministic (e.g. quantifiers). It furthermore decouples rewriteWithProof from reconstruction for theory rewrite steps.

The proof postprocessor is additionally updated so that extended equality REWRITE steps are converted to THEORY_REWRITE steps with identifier RW_REWRITE_EQ_EXT for consistency, since eliminating REWRITE should result in THEORY_REWRITE only. This required generalizing the argument to THEORY_REWRITE to be a MethodId instead of a Boolean.

Fix compiler warnings. (#5305)

(proof-new) Add proofs for circuit propagator (#5301)

This PR adds code to generate proofs for inferences within the (non-clausal) circuit propagator.
It consists of many small methods that each implement simple derivations about single Boolean connectives. It uses already existing proof rules, and thus no separate proof checker is required.
A second PR will use these rules within the circuit propagator class.

(proof-new) Fix for CDProof::isSame (#5297)

Did not check for disequalities properly.

(proof-new) Update add lazy step interface in LazyCDProof (#5299)

Ensuring closed proofs should not be enabled by default, it is actually not used very often as a whole. Moreover, the "trust id" argument is the most useful argument and hence should come as the 3rd argument. This updates all uses of addLazyStep for the change in interface, also changes term conversion generator which had a similar issue with default arguments.

Notice that some calls to addLazyStep were checking closed but without providing a debug string, these I've left alone (they no longer check closed).

Remove some Commands from the API. (#5268)

This PR removes Solver::getAssignment command from the API as there is no way to assign names to terms in the API. It also removes ExpandDefinitionsCommand, an internal functionality in CVC4.

Fix miscellaneous warnings (#5256)

Mostly in cardinality extension, which was cleaned in the previous PR.

Make seq.nth a trigger kind (#5314)

This makes seq.nth a trigger kind, analogous to select in arrays.

This fixes a timeout in seq-unsolved-ematch.smt2, fixing the nightlies.

Handle rewrite to bool in BoundInference (#5311)

The BoundInference class did not properly handle rewrites that yield constant Booleans. This PR fixes this issue by explicitly checking for this case.

Split CheckModels utility to its own file (#5303)

This utility will be undergoing major additions to make it more robust. Thus it should be moved to its own file.

There are no major code changes in this PR, a few things were changed to be consistent to the coding standard.

Integer (CLN): Minor improvements. (#5306)

Review comments by @nafur from #5304.

Expand `seq.nth` lazily (#5287)

Our first support for seq.nth eliminated it eagerly during expandDefinitions.
This PR changes that, by eliminating it lazily, as done with other extended string operators.

Integer: CLN: Move implementation of member functions to .cpp file. (#5304)

This moves the CLN implementation of member functions of class Integer from
the header to the .cpp file. This only moves code, and adds documentation for
previously undocumented or poorly documented functions.

Analogous to #5190.

[proof-new] Fixing resolution proof checker (#5262)

Previously the binary resolution checker was:

- Checking applications in which for a pivot (not l) the literal (not l) would be eliminated from the first clause and l from the second because double negation was handled implicitly. Now whether the binary resolution is such that the pivot is removed as is from the first clause and negated from the second, or the other way around, is marked via an argument.
- Not producing false the remaining set of literals after resolution was empty.

This commit also updates the informal description of the rule accordingly, as well as to clarify the behavior when the pivot does not occur properly in the clauses (in which case the rule application corresponds to weakening).

Co-authored-by: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>

(proof-new) Updates to assertions pipeline and preprocess generator (#5300)

This updates and improves assertions pipeline and preprocess generator so that they avoid cyclic proofs and have better infrastructure for catching pedantic failures.

This is in preparation for making the non-clausal-simplification pass proof producing.

(proof-new) Update preprocessing pass context for proofs (#5298)

This sets up the preprocessing pass context in preparation for proof production.

This PR makes the top level substitutions map into a TrustSubstitutionMap, the data structure that applies substitutions in a way that tracks proofs.

This PR also makes the "apply subst" preprocessing pass proof producing.

[proof-new] Improving cycle checking in lazycdproofchain (#5302)

Safer version of pending lemma processing in inference manager buffered (#5286)

This ensures we don't segfault if the pending lemma vector is cleared while we are processing it. This is potentially possible in datatypes currently. Fixes #5236.

(proof-new) Refactoring cyclic checks (#5291)

This PR makes it so that cyclic checks are only performed eager when proofNewEagerChecking is true.

It refactors the existing cyclic check in ProofNodeToSExpr to have a more consistent style, and adds a cyclic check to getFreeAssumptions.

 (proof-new) Witness axiom reconstruction for purification skolems (#5289)

This formalizes the proofs of existentials that justify purification variables, e.g. those with witness form witness x. x = t for the term t they purify.

This PR generalizes EXISTS_INTRO to do this, and makes some simplifications to SkolemManager.

(proof-new) Implementation of trust substitution (#5276)

Trust substitution is a data structure that is used throughout preprocessing for proofs.

This adds its implementation.

(proof-new) More features for SMT proof post-processor (#5246)

This updates the SMT proof postprocessor with additional stats. It also adds the feature to handle conjunctions as substitution, e.g. a child proof concluding (and (= x t) (= y s)) is interpreted as a substitution for x, y, whereas previously we insisted they must be provided separately.

(proof-new) Improvements for theory engine (#5292)

Avoids use of macro rules in a few places.

Refactor SMT-level model object (#5277)

This refactors the SMT-level model object so that it is a wrapper around TheoryModel instead of a base class. This inheritance was unnecessary.

Moreover, it removes the virtual base models of the SMT-level model which were based on Expr. Now the interface is more minimal and in terms of Node only.

This PR further simplifies a few places in the code that interface with the SmtEngine with things related to models.

Catch more cases of nested recursion in datatypes (#5285)

Fixes #5280.

Previously we were checking for nested recursive datatypes in expandDefinitions. This does not catch cases where the only terms of a malformed nested recursive datatype are variables. The proper place to check is in preRegisterTerm. The benchmark from that issue now gives an error.

bv2int: caching introduced terms (#5283)

The bv-to-int preprocessing pass has a cache that maps each BV node to its translated integer node.
In case the BV node is a function symbol, it's translated integer node is a fresh function symbol.
On current master, if we later process this fresh function symbol in the preprocessing pass, we again create a fresh function symbol as its translation. This is unsound, and was discovered in #5281, whose benchmark is added to regressions.
Closes #5281 if merged.

Add inference enumeration to datatypes (#5275)

This adds an inference enumeration for datatypes, which is analogous to what is done in strings and non-linear arithmetic. Inferences are informal identifiers that serve the purpose of (1) debugging the code, (2) providing hints on how proofs can be reconstructed.

This PR also splits the InferenceManager file in datatypes into 2.

(proof-new) TheoryArithPrivate: farkas lemma proof (#5267)

Use a farkas proof to prove one of arithmetic's lemmas.

These changes were checked-out directly from proof-new, without modification.

Fix issue #5269 (#5270)

This PR fixes issue #5269 of unnecessary calling TheorySetsRels::areEqual in a product relation (which compares the rightmost element of the first child with the leftmost element in the second child). This may violate an assertion in TheorySetsRels::areEqual that the types of the 2 elements should be the same

bv2int: implementing the iand-sum mode (#5265)

There are 3 potential modes to lazily treat the iand operator:
(1) by value (typical CEGAR loop)
(2) by sum (lazily expanding each iand node into a sum of ITEs)
(3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities)

This PR implements (2).

The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.

(proof-new) debug statements & docs for INT_TRUST (#5259)

(proof-new) pfs in TheoryArith(Private) explainations (#5258)

Very simple, just threading the proofs through.

Guard uses of printing approximations for constants (#5247)

Errors with these methods were encountered while working on new techniques for arithmetic preprocessing.

Also, there is obvious inefficiency since approximations for constants are being computed when certain traces are disabled.

(proof-new) pfs for conflicts in TheoryArithPrivate (#5257)

Threads conflict proofs through TheoryArithPrivate.

Mostly just wiring things up.

bv2int: rewritings and unsat cores (#5263)

This commit fixes several issues with bv-to-int preprocessing pass, mostly raised by @ajreynol:

1. make sure to rewrite the processed node before and after processing it
2. use the new `mkAnd` function
3. remove `--no-check-unsat-cores` from tests whenever possible
4. add new tests from #5230 . These tests now pass, and so this PR closes #5230 if merged. This also makes #5253 redundant.
5. remove an unused test

using NOT_NOT_ELIM rather than macros to do double-neg elimination (#5261)

(proof-new) Prove lemmas in Constraint (#5254)

Includes:

T/F splitting lemmas for any arith constraint
Unate lemmas produced early on
The hard part is proving the unate lemmas. In general, they are all implied by 2-constraint farkas proofs, so we ultimately map them all down to proveOr, which constructs that proof.

make check was happy with this change. Hopefully the CI agrees :).

(proof-new) Generalize preprocess proof generator (#5245)

This class is of general use, not just as the overall maintainer of proofs of preprocessing, but also locally within preprocessing passes. This generalizes the interface slightly and also does some minor cleaning.

(proof-new) Simplifications for proof rule checker interface (#5244)

Some of the interfaces in the proof rule checker are unnecessary now and can be deleted.

This also updates STRING_TRUST to have pedantic level 2.

 (proof-new) Miscellaneous minor improvements and fixes to proofs in theory files. (#5241)

(proof-new) New rules for Booleans (#5243)

This adds 2 new rules for convenience to the Boolean checker.

(proof-new) Change merge policy for proof node updater (#5242)

This updates the proof node updater with a mergeSubproofs field which automatically merges subproofs in the same SCOPE that prove the same thing. This is currently enabled by default, it is now configurable and disabled by default.

bv2int: improving bvand tables (#5235)

The bv-to-int preprocessing pass introduces large ite terms that correspond to truth tables of bvand for various bit-widths.
Previously there were two inefficiencies in those tables:

They weren't being cached
The ite was not optimized
This PR adds a cache for the tables that induce the ite terms.
In addition, it computes smaller ite terms by computing the most common value of each table and using it as the default value of the ite.

Remove uf-ss-totality option (#5251)

This option has a number of subtle bugs, it should be reimplemented if/when finite-model-find is refactored. It is not high priority enough to maintain.

This does some additional cleaning of the uf cardinality extension, some methods changed indentation.

Fixes #5239, fixes #4872, fixes #4865.

Eliminate uses of Expr in SmtEngine interface (#5240)

This eliminates all use of Expr in the SmtEngine except in a few interfaces (setUserAttribute, getAssignment) whose signature is currently in question.

The next steps will be to (1) eliminate Expr from the smt/model.h interface, (2) replace Type by TypeNode in Sort.

Ensure uninterpreted sort owner is UF if uf-ho or finite-model-find is enabled. (#5248)

This ensures that arrays is not the owner of uninterpreted sorts if uf-ho or finite-model-find are enabled. In these cases, the UF solver implements special techniques (cardinality, ho reasoning) that should take priority.

Fixes #5233.

SyGuS instantiation modes (#5228)

This PR adds three instantiation modes to the SyGuS instantiation module.

Add conversion of poly polynomial to cvc node. (#5218)

This PR adds a new utility function to convert a poly::Polynomial back to a cvc4 Node.

Provide API version of some SMT Commands. (#5222)

This PR provides an SMT version of the following SMT commands:

get-instantiations
block-model
block-model-values
get-qe
get-qe-disjunct
command.cpp now calls those functions instead of their SmtEngine counterparts. In addition, SEXPR is now an API kind.

bv2int: bvand translation code move (#5227)

This PR is essentially a code move.
It moves the code that translates bvand from the bv_to_int preprocessing pass to a new class IAndHelper, in the new files nl_iand_utils.{h,cpp}. The goal is to have this code in a place which can be shared between the bv2int preprocessing pass and the iand solver.

Future PRs will:

Optimize this utility
Make use of it in the iand solver
The code in nl_iand_utils.{h,cpp} is almost completely a move from bv_to_int.{h,cpp}. The changes are all minor, and include, e.g., the following changes:

the node manager is no longer a member, and so is the constant 0.
using the oneBitAnd function directly, without a function pointer.

Remove deprecated add-path commands and use $GITHUB_PATH instead. (#5232)

use right arith explanation fn to fix regressions (#5231)

Use the Node-returning variants of
Constraint::externalExplainByAssertions in TheoryArithPrivate locations
that aren't computing proofs.

The problem is that the TrustNode returning variant requires that arith
has stored an externally valid literal for the constraint, which is not
always the case.

This is what we did on proof-new, I just forgot.

(proof-new) proofs for arith-constraint explanations (#5224)

Threads proofs through arith::Constraint's machinery for explaining
constraints. Changes, by function:

externalExplainByAssertions:
introduce scope to prove the implication
externalExplainForPropagation:
introduce scope to prove the implication
externalExplainConflict:
use other machinery to prove conflicting constraints
use the CONTRA rule
introduce scope to close the conflict proof
Future commits will pick up these proofs in theory_arith_private.cpp.
Future commits will prove the "split" lemmas produced in constraint.cpp

reset-assertions: Remove all non-global symbols in the parser (#5229)

Fixes #5163. When `:global-declarations` is disabled (the default), then
`(reset-assertions)` should remove all declared and defined symbols. Before
this commit, we would remove the defined function from `SmtEngine` but the
parser would not remove it from its symbol table because the symbol was defined
at (what it considered) level 0. Level 0, however, is reserved for global
symbols that we never want to remove.

This commit adds an additional global `pushScope()`/`popScope()`, similar to
what we have in `SmtEngine`. As a result, user-defined symbols are now defined
at level 1 and get removed from the `SymbolTable` when `(reset-assertions)` is
called. The commit also makes sure that symbols defined by the logic are
asserted at level 0, so that they are not removed by `(reset-assertions)`. It
adds a flag to `defineType` to ignore duplicate definitions because some
symbols are defined by multiple logics, which leads to a failing assertion when
inserting them both at level 0 in the hashmap of the `SymbolTable`. E.g.
strings and integer arithmetic both define `Int`. The commit also fixes
existing unit tests that fail with these stricter semantics of
`(reset-assertions)`.

Signed-off-by: Andres Noetzli <noetzli@amazon.com>

Simplify approach for collapsed selectors over non-closed enumerable types (#5223)

This simplifies the approach for wrongly-applied selectors whose range type involves e.g. uninterpreted sorts. These cases are particularly tricky since uninterpreted constants should never appear in facts or lemmas.

Previously, the rewriter had special cases for either making a ground term or value, and a purify step was used to eliminate the occurrences of uninterpreted sorts afterwards.

This PR leverages mkGroundTerm in this inference instead, and makes the rewriter uniformly use mkGroundValue.

This also required making the type enumerator for datatypes more uniform. In particular, we require that the first value enumerated by the type enumerator is of the same shape as the term required by mkGroundTerm, or else debug-check-model will fail. This is due to the fact that now the inference for wrongly applied selectors uses terms while the rewriter uses values. The type enumerator is updated so that recursive codatatypes also first take mkGroundValue as the zero term, when they are well-founded. Previously this was skipped since the codatatype enumerator uses a different algorithm for computing its ground terms.

This is in preparation for further work on optimizations and proofs for datatypes.

(proof-new) Add lazy proof set utility (#5221)

This is a common pattern that is required in several places in preprocessing.

(proof-new) Theory engine proof producing (#5195)

This completes proof support in TheoryEngine.

The main addition in this PR is to make its getExplanation method proof producing.

(proof-new) Fixes and improvements for smt proof postprocessor (#5197)

This includes several subtle issues encountered in the past month based on our regressions.

It also improves the expansion forms of MACRO_ rules to use EQ_RESOLVE instead of a TRUE_INTRO/TRUE_ELIM scheme. This is both more compact and avoids cyclic proofs for some corner cases of proofs with Boolean constant equalites.

Get correct NodeManagerScope for toStrings in API (#5216)

Gets the correct `NodeManagerScope` for getting the `toString` of a term, op, or sort. The following program had strange output:
```
#include "cvc4/api/cvc4cpp.h"
using namespace CVC4::api;
using namespace std;
int main()
{
  Solver s;
  Term x = s.mkConst(s.getIntegerSort(), "x");
  cout << "x = " << x << endl;
  Solver s2;
  cout << "x = " << x << endl;
  return 0;
}
```

It was outputting:
```
x = x
x = var_267
```

Fixing the scope makes the output `x = x` both times, as expected.

fix unit failures on debug without symfpu (#5212)

The following tests fail (locally) when compiling with debug and without symfpu:

unit/api/sort_black (Failed)
unit/theory/logic_info_white (Failed)
unit/util/floatingpoint_black (Child aborted)

This PR conditions the relevant parts of these tests to the availability of symfpu.

Co-authored-by: Aina Niemetz <aina.niemetz@gmail.com>

(proof-new) proofs in ee -> arith pipeline (#5215)

Threads proofs through the flow of information from the equality engine
into the theory of arithmetic.

Pretty straightforward. You just have to bundle up information from the EE.

New C++ API: Rename Term::isConst() to Term::isValue(). (#5211)

Make sure conflicts are not rewritten (in arithmetic) (#5219)

The arithmetic inference manager did rewrite conflicts, which lead to nodes from the conflict not being assumptions (but rewritten assumptions) triggering an assertion. This rewrite is now removed.
Furthermore rewrites triggering the same assertion within the icp subsolver have been refactored to avoid this issue.

(proof-new) Add the strings proof constructor (#4903)

This is the method for converting strings InferInfo into instructions for building ProofNode. Notice that this is done as a standalone module, and thus the theory of strings uses Inferences only, not PfRule.

The next step will be to integrate this utility into InferenceManager.

Improve OSX support by adding os detection and adapting calls for OSX. (#5023)

On OSX there is another libtoolize tool already available.
The gnu libtoolize version installed with MacPorts or brew is called glibtoolize.
This change makes it easier to run the file on OSX.

Signed-off-by: Malte Mues (mail.mues@gmail.com)

Process pending inferences at the beginning of datatypes post check (#5213)

This fixes a potential crash in datatypes where a pending inference is not processed on a call to Theory::check. This ensures the pending set of inferences in datatypes is empty after each check. This also ensures the pending vectors are cleared before each check in datatypes.

bv-to-int: change order of passes (#5208)

Closes #5095 and replaces #5110.
There are two tests in #5095 that produce two different assertion failures when using bv-to-int.
The first happens because the substitution map wasn't applied after the pass.
The second happens because div (that is introduced in the pass) is not rewritten using witness.
Both problems are solved by making sure that apply-substs, theory-preprocess and ite-removal are executed after bv-to-int.
The two tests from #5095 are included as regressions.

(proof-new) proofs for ArithCongMan -> ee facts (#5207)

Threads proof production through the ArithCongruenceManager's pipeline
of information to the equality engine.

The idea is to define a method:

ArithCongruenceManager::assertLitToEqualityEngine(literal, reason, pf)
This method asserts a literal to the equality engine with the given
proof and reason. It stores the proof of the literal for the equality
engine's future reference, and is smart about symmetric literals.

This machinery uses proofs that are not closed over the reason, as the
equality engine requires.

Other functions in the pipeline:

assertionToEqualityEngine
equalsCostant
construct proofs and call assertLitToEqualityEngine.
Future commits will address the ee -> ArithCongruenceManager pipeline,
and the relationship between ArithCongruenceManager and the rest of
arithmetic.

(proof-new) Add interface for trusted substitution and update ppAssert (#5193)

The current work on proof-new involves proofs for preprocessing. The biggest issue currently is that our preprocessing passes do not track proofs for substitutions.

This adds a "trusted substitution" class with is a layer on substitution map. The proof aspect of this class is not yet implemented, this PR just adds its interface.

This also updates Theory::ppAssert to take a TrustSubstitutionMap instead of a SubstitutionMap, since eventually we will require proofs to be provided for substitutions that are added to this map.