Gereon Kremer [Wed, 3 Mar 2021 16:50:45 +0000 (17:50 +0100)]
More cleanup of includes to reduce compilation times (#6037)
Similar to #6031, this PR implements suggestions from iwyu to reduce the number of includes in header files by introducing forward declarations and moving includes to source files.
Abdalrhman Mohamed [Wed, 3 Mar 2021 10:28:45 +0000 (04:28 -0600)]
Remove uses of SExpr class. (#6035)
This PR is a step towards removing SExpr class. It replaces SExpr with std::string for set-info and set-option commands.
mudathirmahgoub [Wed, 3 Mar 2021 08:16:32 +0000 (02:16 -0600)]
Add tuple projection operator (#5904)
This PR adds tuple projection operator to the theory of data types.
It Also adds helper functions for selecting elements from a tuple.
Mathias Preiner [Tue, 2 Mar 2021 23:22:03 +0000 (15:22 -0800)]
Remove non-ASCII characters from source files. (#6039)
Make collect_tags.py more robust for non-ASCII characters.
Gereon Kremer [Tue, 2 Mar 2021 22:49:29 +0000 (23:49 +0100)]
Improve handling of utf8 encoded inputs (#5694)
This PR fixes an issue where utf8 encoded inputs are incorrectly parsed into CVC4::String. We now use std::mbtowc to first turn the char sequence from the std::string input into a std::wstring and then process this std::wstring one charactor (wchar_t) at a time.
Fixes #5673
Aina Niemetz [Tue, 2 Mar 2021 22:06:38 +0000 (14:06 -0800)]
Remove obsolete dependency on CxxTest. (#6038)
Mathias Preiner [Tue, 2 Mar 2021 08:26:29 +0000 (00:26 -0800)]
Add aarch64 (ARM64) cross-compile support. (#6033)
This commit adds support for cross-compiling for aarch64 platforms and simplifies cross-compilation handling for Windows. The configure script now automatically downloads and cross-compiles the required dependencies ANTLR3 and GMP when passing option --arm64 or --win64.
Fixes #1479 #5769.
Mathias Preiner [Tue, 2 Mar 2021 04:18:24 +0000 (20:18 -0800)]
Fix nightly errors. (#6034)
Fixes warnings with CVC4_FALLTHROUGH and -Werror for debug/production with gcc/clang. Clang detects that a CVC4_FALLTHROUGH after an Assert(false); is unreachable and issues a warning, while gcc issues a warning about an implicit fall-through if CVC4_FALLTHROUGH is not present.
Andrew Reynolds [Tue, 2 Mar 2021 03:37:03 +0000 (21:37 -0600)]
Introduce quantifiers term registry (#5983)
This groups utilities related to ground terms into TermRegistry which will be passed to quantifier modules.
Gereon Kremer [Tue, 2 Mar 2021 00:58:20 +0000 (01:58 +0100)]
Clean up includes to reduce compile times (#6031)
This PR cleans up a ton of includes, based on the suggestions of iwyu.
Mostly, it removes includes from header files in favor of forward declarations and adds includes to source files.
Aina Niemetz [Tue, 2 Mar 2021 00:07:25 +0000 (16:07 -0800)]
google test: util: Migrate floatingpoint_black. (#6021)
Aina Niemetz [Mon, 1 Mar 2021 23:32:16 +0000 (15:32 -0800)]
google test: theory: Migrate theory_quantifiers_bv_inverter_white. (#5991)
Aina Niemetz [Mon, 1 Mar 2021 22:46:53 +0000 (14:46 -0800)]
google test: util: Migrate bitvector_black. (#6015)
Aina Niemetz [Mon, 1 Mar 2021 22:00:51 +0000 (14:00 -0800)]
google test: theory: Migrate theory_quantifiers_bv_instantiator_white. (#5989)
Gereon Kremer [Mon, 1 Mar 2021 21:17:54 +0000 (22:17 +0100)]
Refactor collection of debug and trace tags (#5996)
We have a mechanism to collect all debug and trace tags used throughout the code base to allow checking for valid tags.
This mechanism relies on a collection of more or less readable shell scripts.
#5921 hinted to a problem with the current setup, as it passes all source files via command line.
This PR refactors this setup so that the scripts collect the files internally, and only the base directory is passed on the command line.
As I was touching this code anyway, I ported everything to python and combined it into a single script, in the hope to make it more maintainable.
Fixes #5921.
Mathias Preiner [Mon, 1 Mar 2021 18:36:58 +0000 (10:36 -0800)]
Make -Werror optional but enable it for CI. (#6032)
Aina Niemetz [Mon, 1 Mar 2021 16:40:11 +0000 (08:40 -0800)]
google test: util: Migrate stats_black. (#6029)
Aina Niemetz [Mon, 1 Mar 2021 16:04:01 +0000 (08:04 -0800)]
google test: util: Migrate real_algebraic_number_black. (#6028)
Aina Niemetz [Mon, 1 Mar 2021 15:39:26 +0000 (07:39 -0800)]
google test: util: Migrate rational_white. (#6027)
Aina Niemetz [Mon, 1 Mar 2021 15:08:33 +0000 (07:08 -0800)]
google test: util: Migrate rational_black. (#6026)
Aina Niemetz [Mon, 1 Mar 2021 14:46:01 +0000 (06:46 -0800)]
google test: util: Migrate output_black. (#6025)
Aina Niemetz [Mon, 1 Mar 2021 14:02:54 +0000 (06:02 -0800)]
google test: util: Migrate integer_black. (#6023)
Aina Niemetz [Mon, 1 Mar 2021 13:42:33 +0000 (05:42 -0800)]
google test: util: Migrate datatype_black. (#6019)
Aina Niemetz [Mon, 1 Mar 2021 13:07:19 +0000 (05:07 -0800)]
google test: util: Migrate configuration_black. (#6018)
Aina Niemetz [Mon, 1 Mar 2021 12:44:11 +0000 (04:44 -0800)]
google test: util: Migrate boolean_simplification_black. (#6014)
Aina Niemetz [Mon, 1 Mar 2021 12:22:48 +0000 (04:22 -0800)]
google test: util: Migrate array_store_all_white. (#6008)
Aina Niemetz [Mon, 1 Mar 2021 11:55:20 +0000 (03:55 -0800)]
google test: util: Migrate integer_white. (#6024)
Aina Niemetz [Mon, 1 Mar 2021 09:31:23 +0000 (01:31 -0800)]
google test: theory: Migrate theory_strings_skolem_cache_black. (#6002)
Aina Niemetz [Mon, 1 Mar 2021 09:00:46 +0000 (01:00 -0800)]
google test: theory: Migrate theory_strings_word_white. (#6003)
Aina Niemetz [Sat, 27 Feb 2021 03:51:25 +0000 (19:51 -0800)]
google test: util: Migrate exception_black. (#6020)
Aina Niemetz [Sat, 27 Feb 2021 02:54:23 +0000 (18:54 -0800)]
google test: util: Migrate check_white. (#6017)
Aina Niemetz [Sat, 27 Feb 2021 00:30:39 +0000 (16:30 -0800)]
google test: util: Migrate cardinality_black. (#6016)
Aina Niemetz [Sat, 27 Feb 2021 00:04:58 +0000 (16:04 -0800)]
google test: theory: Migrate theory_white. (#6006)
This moves test utils for theory tests to test_smt.h and consolidates
two implementations of dummy theories into one.
Aina Niemetz [Fri, 26 Feb 2021 23:16:57 +0000 (15:16 -0800)]
google test: theory: Migrate type_enumerator_white. (#6007)
Haniel Barbosa [Fri, 26 Feb 2021 22:52:15 +0000 (19:52 -0300)]
Some formatting and better tracing in prop engine (#6022)
Miscellaneous changes from proof-new.
Aina Niemetz [Fri, 26 Feb 2021 22:11:49 +0000 (14:11 -0800)]
google test: theory: Migrate theory_sets_type_rules_white. (#6001)
Aina Niemetz [Fri, 26 Feb 2021 21:28:22 +0000 (13:28 -0800)]
google test: theory: Migrate theory_sets_type_enumerator_white. (#6000)
Mathias Preiner [Fri, 26 Feb 2021 20:48:33 +0000 (12:48 -0800)]
Fix -Werror issues with clang and use clang for debug-cln build. (#6004)
This fixes some issues that break the nightly ASAN builds with clang.
Aina Niemetz [Fri, 26 Feb 2021 19:59:38 +0000 (11:59 -0800)]
google test: util: Migrate binary_heap_black. (#6012)
Aina Niemetz [Fri, 26 Feb 2021 19:25:05 +0000 (11:25 -0800)]
google test: util: Migrate assert_white. (#6011)
Andrew Reynolds [Fri, 26 Feb 2021 18:47:05 +0000 (12:47 -0600)]
Minor improvement and fix to smt2 printer (#6009)
This permits access to the static method string smtKindString(Kind k, Variant v) which is required for LFSC proof conversion. It also makes a fix to how a string kind is printed.
Andrew Reynolds [Fri, 26 Feb 2021 17:44:23 +0000 (11:44 -0600)]
Optionally permit creation of non-flat function types (#6010)
This is required for creating the representation of closues in LFSC, which are of the form ((forall x T) P) where notice that forall has non-flat function type (-> Int Sort (-> Bool Bool)).
Gereon Kremer [Fri, 26 Feb 2021 05:02:43 +0000 (06:02 +0100)]
Store Node instead of TNode (#5993)
The justification heuristic stores a "copy" of assertions as TNode. As witnessed by #5938, these TNodes may invalid.
This PR changes this to store Nodes instead.
Fixes #5938.
Andrew Reynolds [Fri, 26 Feb 2021 03:41:27 +0000 (21:41 -0600)]
(proof-new) Fix regular expression unfolding under substitution (#5958)
This case was previously unhandled and exercised by a recently added regression.
Gereon Kremer [Thu, 25 Feb 2021 23:46:17 +0000 (00:46 +0100)]
Move (optional) rewrite from TrustSubstitutionMap to SubstitutionMap. (#5992)
This PR adds optional rewriting to the SubstitutionMap class. Before, only the new TrustSubstitutionMap added optional rewriting, leading to unexpected inconsistencies between the two. In particular, cases exist where the substitution and the rewriting cancel each other (see #5943).
This PR moves the optional rewriting from TrustSubstitutionMap into SubstitutionMap. While the former enables it by default, it is disabled by default for the latter and thus does not change current behavior.
We now use this new option in an assertion in the non-clausal simplification.
Fixes #5943.
Andrew Reynolds [Thu, 25 Feb 2021 22:40:24 +0000 (16:40 -0600)]
Move slow regressions to regress1 (#5999)
Moves regressions taking >4 seconds (summing all configs) in debug to regress1.
yoni206 [Thu, 25 Feb 2021 20:36:05 +0000 (12:36 -0800)]
Datatypes lemmas: share only external types (#5997)
Forcing lemmas in datatypes used to be done only for external types.
This was changed to consider all types, which is not needed.
This PR brings back the restriction to external types.
Aina Niemetz [Thu, 25 Feb 2021 19:44:48 +0000 (11:44 -0800)]
google test: Merge Node(Manager) fixtures. (#5998)
Gereon Kremer [Thu, 25 Feb 2021 13:34:40 +0000 (14:34 +0100)]
Add regression. (#5994)
This PR adds the test case from #5187 as a regression.
Fixes #5187.
Aina Niemetz [Thu, 25 Feb 2021 13:07:17 +0000 (05:07 -0800)]
google test: theory: Migrate theory_bv_white. (#5987)
Aina Niemetz [Thu, 25 Feb 2021 12:27:15 +0000 (04:27 -0800)]
google test: theory: Migrate theory_bv_rewriter_white. (#5986)
Aina Niemetz [Thu, 25 Feb 2021 11:43:56 +0000 (03:43 -0800)]
google test: printer: Migrate smt2_printer_black. (#5970)
Mathias Preiner [Thu, 25 Feb 2021 00:26:44 +0000 (16:26 -0800)]
Enable -Werror. (#5969)
Aina Niemetz [Wed, 24 Feb 2021 22:35:22 +0000 (14:35 -0800)]
google test: theory: Migrate theory_bags_type_rules_white. (#5984)
Aina Niemetz [Wed, 24 Feb 2021 20:25:10 +0000 (12:25 -0800)]
google test: theory: Migrate theory_engine_white. (#5988)
Aina Niemetz [Wed, 24 Feb 2021 18:24:14 +0000 (10:24 -0800)]
google test: theory: Migrate theory_black. (#5985)
Gereon Kremer [Wed, 24 Feb 2021 15:41:49 +0000 (16:41 +0100)]
Ensure static-learning adds rewritten assertions. (#5982)
The static-learning preprocessing sometimes added non-rewritten assertions, despite being used in a part of the preprocessor that assumes all assertions to be rewritten. This may then break other passes further down, in the case of #5729 the non-clausal simplification which explicitly asserts that assertions are rewritten. This PR rewrites the respective assertion properly in the static-learning pass.
Fixes #5729.
Gereon Kremer [Wed, 24 Feb 2021 15:04:59 +0000 (16:04 +0100)]
(proof-new) Add proofs for CAD solver (#5981)
This PR adds proofs for the CAD solver, based on the proof generator from the previous PR.
Note that the level of detail of these CAD proofs is significantly higher than for other proofs. Making these proofs more fine-grained and maybe at some point accessible to proof checkers is probably still quite a bit of work.
Thus, the CAD proof rules are both trusted rules for now.
Aina Niemetz [Wed, 24 Feb 2021 12:22:21 +0000 (04:22 -0800)]
google test: theory: Migrate sequences_rewriter_white. (#5975)
Aina Niemetz [Wed, 24 Feb 2021 11:17:42 +0000 (03:17 -0800)]
google test: theory: Migrate theory_bags_normal_form_white. (#5978)
Aina Niemetz [Wed, 24 Feb 2021 10:39:00 +0000 (02:39 -0800)]
google test: theory: Migrate logic_info_white. (#5973)
Aina Niemetz [Wed, 24 Feb 2021 09:13:09 +0000 (01:13 -0800)]
google test: theory: Migrate theory_bags_rewriter_white. (#5979)
Aina Niemetz [Wed, 24 Feb 2021 08:53:23 +0000 (00:53 -0800)]
google test: theory: Migrate theory_arith_white. (#5977)
Aina Niemetz [Wed, 24 Feb 2021 08:17:55 +0000 (00:17 -0800)]
google test: theory: Migrate evaluator_white. (#5972)
Aina Niemetz [Wed, 24 Feb 2021 07:38:38 +0000 (23:38 -0800)]
google test: prop: Migrate cnf_stream_white. (#5971)
Andrew Reynolds [Wed, 24 Feb 2021 01:51:21 +0000 (19:51 -0600)]
Add state and inference manager to inst match generator (#5968)
In preparation for refactoring E-matching to not pass QuantifiersEngine pointer to its utilities.
Andrew Reynolds [Wed, 24 Feb 2021 01:12:32 +0000 (19:12 -0600)]
Add interface to TheoryState for sort inference and facts (#5967)
This eliminates the need for direct references to TheoryEngine from quantifiers and UF+cardinality.
This PR also eliminates an unnecessary reference to TheoryEngine in TheoryModelBuilder and breaks a few more dependencies in quantifiers modules.
Mathias Preiner [Tue, 23 Feb 2021 23:56:16 +0000 (15:56 -0800)]
Switch to C++17. (#5959)
Co-authored-by: Gereon Kremer <nafur42@gmail.com>
Aina Niemetz [Tue, 23 Feb 2021 23:16:41 +0000 (15:16 -0800)]
google test: theory: Migrate regexp_operation_black. (#5974)
Aina Niemetz [Tue, 23 Feb 2021 22:34:20 +0000 (14:34 -0800)]
google test: theory: Migrate strings_rewriter_white. (#5976)
Gereon Kremer [Tue, 23 Feb 2021 18:31:28 +0000 (19:31 +0100)]
Add proof for mult sign lemma (#5966)
This PR adds the proof for a nonlinear refinement lemma that infers the sign of a monomial from the sign of the variables.
Haniel Barbosa [Tue, 23 Feb 2021 17:31:38 +0000 (14:31 -0300)]
[proof-new] Fix dangling pointer in SAT proof generation (#5963)
When a clause is being explained, the negation of each of its literals, other than the one it propagates, needs to be explained. This process may lead to the creation of new clauses in the SAT solver (because if a literal being explained was propagated and an explanation was not yet given, it will then be computed and added). This may lead to changes in the memory where clauses are, which may break the reference to the original clause being explained. To avoid this issue we store the literals in the reason before we start explaining their negations. We then iterate over them rather than over the clause, as before.
Gereon Kremer [Tue, 23 Feb 2021 16:51:53 +0000 (17:51 +0100)]
Add proof for monomial bounds check (#5965)
This PR adds proofs for a nonlinear refinement lemma that deals with multiplication of inequalities with some term. This lemma is split into two proof rules for positive or negative factors.
Gereon Kremer [Tue, 23 Feb 2021 16:17:45 +0000 (17:17 +0100)]
(proof-new) Add proof generator for CAD solver (#5964)
This PR adds a proof generator for the CAD solver, including two new proof rules. The code is not yet used, but will be integrated into the CAD solver itself in another PR.
Haniel Barbosa [Tue, 23 Feb 2021 14:59:32 +0000 (11:59 -0300)]
[proof-new] Fix handling of removable clauses in proof cnf stream (#5961)
Previously the removable information was not being communicated from the proof cnf stream to the cnf stream, which is the one that actually uses this when asserting clauses into the SAT solver. This commit fixes this by having the proof cnf stream directly use the cnf stream d_removable attribute.
Gereon Kremer [Tue, 23 Feb 2021 04:35:46 +0000 (05:35 +0100)]
Add trans secant proofs. (#5957)
This PR adds proofs for secant lemmas in the transcendental lemmas for both exponential and sine functions.
It also adds proof rules and corresponding proof checkers.
Andrew Reynolds [Tue, 23 Feb 2021 03:53:45 +0000 (21:53 -0600)]
Explanation of failure for instantiate, use in enumerative instantiation (#5951)
This makes enumerative instantiation generalize the failures in Instantiate::addInstantiate and increment its enumeration accordingly.
This leads to (+104-6) using enumerative instantiation only on SMT-LIB quantified benchmarks, 60 second timeout.
This is in preparation for further improvements to enumerative instantiation.
Aina Niemetz [Tue, 23 Feb 2021 01:32:55 +0000 (17:32 -0800)]
google test: preprocessing: Migrate pass_bv_gauss_white. (#5935)
Andrew Reynolds [Mon, 22 Feb 2021 23:19:20 +0000 (17:19 -0600)]
Eliminate raw use of output channel and valuation in quantifiers (#5933)
This makes all lemmas in quantifiers sent through the inference manager. It begins adding InferenceId values for some of these calls. All uses of Valuation are replaced by calls to QuantifiersState.
Andrew Reynolds [Mon, 22 Feb 2021 22:35:20 +0000 (16:35 -0600)]
Move quantifiers attributes to quantifiers registry (#5929)
This moves the utility class beneath quantifiers registry.
Andrew Reynolds [Mon, 22 Feb 2021 22:07:16 +0000 (16:07 -0600)]
(proof-new) Change proof-new option to proof (#5955)
Also moves several proof-specific options to proof_options.
Gereon Kremer [Mon, 22 Feb 2021 21:27:30 +0000 (22:27 +0100)]
(proof-new) Add proofs for exponential functions (#5956)
This PR adds proofs for lemmas concerned with the exponential function. If also adds the necessary proof rules and corresponding proof checker.
Andrew Reynolds [Mon, 22 Feb 2021 20:15:43 +0000 (14:15 -0600)]
Require length-in-conclusion form for strings inferences (#5953)
Previously, it was optional whether to put length constraints in conclusion for deq string inferences. However, due to optimizations in skolem caching, it is now required to guard these length constraints.
It furthermore changes the policy to not ignore the lengths for the registered skolem, since it may be shared elsewhere.
Fixes #5940.
Notice that proof-new already requires this option to be enabled when proofs are enabled. Hence, this will simplify proof-new when merged.
Andrew Reynolds [Mon, 22 Feb 2021 19:38:15 +0000 (13:38 -0600)]
(proof-new) Option to automatically add SYMM steps during proof node update. (#5939)
Required for work on external proof conversions.
Haniel Barbosa [Mon, 22 Feb 2021 19:03:22 +0000 (16:03 -0300)]
[proof-new] Optionally print conclusion in the AST proof (#5954)
Adds an option to optionally print conclusion in the AST proof.
Aina Niemetz [Mon, 22 Feb 2021 18:20:17 +0000 (10:20 -0800)]
google test: preprocessing: Migrate pass_foreign_theory_rewrite_white. (#5936)
Gereon Kremer [Mon, 22 Feb 2021 17:37:47 +0000 (18:37 +0100)]
Add the LazyTreeProofGenerator. (#5948)
This PR adds a new proof utility to construct tree-shaped proofs in a lazy fashion.
The LazyTreeProofGenerator is currently intended to be used for CAD proofs, where we need to construct proofs that consist of nested case-splits, but the exact split (in a form suitable for proof construction) is only known when the whole subtree is finished.
We thus store the proof in a tree structure similar to proof nodes, and transform the whole proof to a proper proof node once all data is available.
Gereon Kremer [Mon, 22 Feb 2021 16:58:47 +0000 (17:58 +0100)]
(proof-new) Add new arithmetic kind INDEXED_ROOT_PREDICATE. (#5949)
This PR introduces a new arithmetic kind for indexed root predicates.
An indexed root predicate compares a real variable to the k'th root of a given polynomial as follows:
Let IRP_k(x ~ 0, p) an indexed root predicate with k a non-negative number, x some real variable, ~ an arithmetic relation (e.g. =, <, ...), and p a polynomial over x (and possibly other variables).
If p contains variables apart from x, we can only evaluate the expression over a suitable assignment for at least these variables.
The evaluation of this expression is equivalent to computing the k'th real root of p in x (with all other variables evaluated over a given assignment) and comparing this real root to zero (according to the relation symbol ~).
Note that we currently do not intend to use this structure for solving, but require it for representing and printing CAD proofs.
Gereon Kremer [Mon, 22 Feb 2021 16:25:38 +0000 (17:25 +0100)]
(proof-new) Add proofs for sine lemmas in the transcendental solver (#5952)
This PR adds proofs for the lemmas related to the sine function in the transcendental solver.
It introduces several new proof rules with corresponding proof checkers and produces proofs in the sine solver.
Gereon Kremer [Mon, 22 Feb 2021 15:07:40 +0000 (16:07 +0100)]
Cleanup in transcendental solver, add ApproximationBounds struct. (#5945)
This PR merges some cleanup in the transcendental solver from proof-new.
It adds a new struct ApproximationBounds that replaces an opaque std::vector and does some general refactoring in the TaylorGenerator class, removing dead code and using fixed-width integers.
Gereon Kremer [Mon, 22 Feb 2021 14:44:44 +0000 (15:44 +0100)]
add pruneRedundantIntervals (#5950)
Adds a simple helper for CAD to prune redundant intervals. It is just a wrapper for cleanIntervals right now, but will be responsible to making sure the CAD proof is pruned as well.
Andrew Reynolds [Mon, 22 Feb 2021 13:01:18 +0000 (07:01 -0600)]
Fix datatypes inference manager when proofs are enabled (#5937)
Accidentally was not sending lemmas in one interface when proofs are enabled due to recent refactoring.
Andrew Reynolds [Fri, 19 Feb 2021 18:16:42 +0000 (12:16 -0600)]
Simplify interface to instantiate (#5926)
Does not support InstMatch interfaces anymore, which are spurious.
Andrew Reynolds [Fri, 19 Feb 2021 16:44:45 +0000 (10:44 -0600)]
Fill in missing inference ids in datatypes theory (#5931)
Also updates its inference manager to not track stats since the standard ones are now used.
This also sets up some dependencies in the sygus extension which will be used to implement InferenceId for the sygus extension, to be done on a separate PR.
Andrew Reynolds [Fri, 19 Feb 2021 15:26:36 +0000 (09:26 -0600)]
Refactoring theory inference process (#5920)
This PR refactors TheoryInference so that it is not responsible for calling back into InferenceManager, instead it sets data so that InferenceManagerBuffered has enough information to do this itself. It also makes the decision of whether to cache lemmas in theory inference manager a global choice per-theory instead of per-lemma.
Andrew Reynolds [Fri, 19 Feb 2021 14:43:22 +0000 (08:43 -0600)]
Fix rewrite for contains over replace (#5924)
Fixes model soundness issue (fixes #5915).
Andrew Reynolds [Fri, 19 Feb 2021 10:07:27 +0000 (04:07 -0600)]
Remove string stat for inferences (#5932)
This is now subsumed by the general stat in TheoryInferenceManager
Gereon Kremer [Fri, 19 Feb 2021 08:34:36 +0000 (09:34 +0100)]
Cleanup of inferences in arithmetic theory (#5927)
This PR cleans up several issues in the arithmetic theory mostly related to its usage of InferenceId and the TheoryInferenceManager:
remove the ArithLemma class and uses SimpleTheoryLemma instead
only use NlLemma if we actually need it
use proper InferenceIds everywhere
remove unused code in the nonlinear extension
Aina Niemetz [Fri, 19 Feb 2021 00:22:40 +0000 (16:22 -0800)]
Add Gereon to AUTHORS list. (#5930)
Gereon Kremer [Thu, 18 Feb 2021 22:59:37 +0000 (23:59 +0100)]
Add statistic for InferenceId to TheoryInferenceManager. (#5913)
This PR uses the IntegralHistogramStat to obtain statistics about the sent inferences within the TheoryInferenceManager. All theories are adapted to provide a proper name (prefix) for the name of the statistic.