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.
Gereon Kremer [Thu, 18 Feb 2021 21:33:10 +0000 (22:33 +0100)]
Add InferenceIds for sets theory. (#5900)
This PR introduces new InferenceId for the theory of sets and uses them instead of InferenceId::UNKNOWN.
Gereon Kremer [Thu, 18 Feb 2021 20:37:30 +0000 (21:37 +0100)]
New InferenceIds for BV theory (#5909)
This PR introduces new InferenceId for the BV theory and uses them instead of InferenceId::UNKNOWN.
Andrew Reynolds [Thu, 18 Feb 2021 07:21:38 +0000 (01:21 -0600)]
Document UF inferences (#5917)
Document UF entries of InferenceId enum.
Andrew Reynolds [Thu, 18 Feb 2021 03:15:39 +0000 (21:15 -0600)]
Eliminate non-static members in term util (#5919)
This makes it so that TermUtil is now a collection of static methods. Further refactoring will make this a standalone file of utility methods.
This breaks all dependencies on the TermUtil object in QuantifiersEngine. It also starts breaking some of the depenendencies on quantifiers engine in sygus.
Andrew Reynolds [Thu, 18 Feb 2021 02:41:19 +0000 (20:41 -0600)]
Move first order model for full model check to own file (#5918)
This moves the derived model class used in finite model finding to its own file, in the src/theory/quantifiers/fmf directory.
Updates the code to meet guidelines, no behavior changes.
Andrew Reynolds [Wed, 17 Feb 2021 19:34:54 +0000 (13:34 -0600)]
Move methods from term util to quantifiers registry (#5916)
Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.
Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.
Andrew Reynolds [Wed, 17 Feb 2021 17:00:41 +0000 (11:00 -0600)]
Compute fact or lemma in datatypes prior to buffering (#5914)
This is necessary for the planned refactoring of TheoryInference::process. This forces datatypes to decide lemma vs. fact prior to buffering inferences.
Gereon Kremer [Wed, 17 Feb 2021 15:50:15 +0000 (16:50 +0100)]
Use InferenceId in sep theory. (#5912)
This PR uses the new InferenceIds in the separation logic theory.
Gereon Kremer [Wed, 17 Feb 2021 15:10:43 +0000 (16:10 +0100)]
TheoryIds for UF theory. (#5901)
This PR introduces new InferenceId for the uf theory and uses them instead of InferenceId::UNKNOWN.
Gereon Kremer [Wed, 17 Feb 2021 14:39:42 +0000 (15:39 +0100)]
Add InferenceIds for theory of arrays (#5910)
This PR introduces new InferenceIds for the theory of arrays and uses them instead of InferenceId::UNKNOWN.
Gereon Kremer [Wed, 17 Feb 2021 13:42:50 +0000 (14:42 +0100)]
Add InferenceId to buffered inference manager (#5911)
This PR collects the InferenceId in the InferenceManagerBuffered class.
Gereon Kremer [Wed, 17 Feb 2021 08:17:03 +0000 (09:17 +0100)]
Add new IntegralHistogramStat (#5898)
This PR adds a new statistics class that improves on HistogramStat if we know that the type is integral (also supporting enums).
Instead of using a comparably slow std::map like HistogramStat, IntegralHistogramStat uses a std::vector that is resized appropriately.
The integral values are simply cast to std::int64_t and used as indices into the vector.
Mathias Preiner [Wed, 17 Feb 2021 00:36:57 +0000 (16:36 -0800)]
Add bit-level propagation support to BV bitblast solver. (#5906)
This commit adds support for bit-level propagation for the BV bitblast solver to quickly detect conflicts on effort levels != FULL. Bit-level propagation for the bitblast solver is by default disabled for now. Further, bit-blasting of facts is now handled more lazily with a bit-blast queue.
Aina Niemetz [Tue, 16 Feb 2021 16:08:55 +0000 (08:08 -0800)]
google test: parser: Migrate parser_builder_black. (#5896)
Gereon Kremer [Mon, 15 Feb 2021 08:08:47 +0000 (09:08 +0100)]
Remove now obsolete sendLemmas and inferences stat from arith::nl (#5903)
This PR removes some obsolete code from the nonlinear solver.
The statistics will soon be replaced by a generic statistic in the theory inference manager.
Andrew Reynolds [Sat, 13 Feb 2021 14:42:36 +0000 (08:42 -0600)]
Moving methods from quantifiers engine to quantifiers state (#5881)
Towards eliminating dependencies on quantifiers engine.
Mathias Preiner [Sat, 13 Feb 2021 14:08:37 +0000 (06:08 -0800)]
Properly set up equality engine for BV bitblast solver. (#5905)
Theory BV now sets up the default equality engine for BV solvers that do not use their own equality engine like e.g. the BV bitblast solver. This commit also adds the missing equality engine pieces to the BV bitblast solver (getEqualityStatus, explain).
Andrew Reynolds [Fri, 12 Feb 2021 09:45:29 +0000 (03:45 -0600)]
Simplify and fix decision engine's handling of skolem definitions (#5888)
This PR changes the front end of prop engine to distinguish input formulas from skolem definitions, which is required by the decision engine. This PR breaks the dependency of PropEngine on the AssertionsPipeline, as now the determining of whether an input formula is a skolem definition is handled externally, in SmtSolver.
With this PR, we should not be required to satisfy skolem definitions that are not relevant based on the techniques already implemented in the decision engine. Currently, we are not distinguishing input formulas from skolem definitions properly, meaning we assert more literals than we need to.
This also simplifies related interfaces within decision engine.
We should test this PR with --decision=justification on SMT-LIB.
Andrew Reynolds [Fri, 12 Feb 2021 08:51:22 +0000 (02:51 -0600)]
(proof-new) Option to not automatically consider symmetry in CDProof (#5895)
There are compelling use cases not to automatically introduce SYMM steps in CDProof, e.g. in CDProofs used within ProofNodeUpdater for external conversions.
Aina Niemetz [Thu, 11 Feb 2021 23:34:58 +0000 (15:34 -0800)]
google test: parser: Migrate parser_black. (#5886)
Gereon Kremer [Thu, 11 Feb 2021 20:25:50 +0000 (21:25 +0100)]
Make most methods of TheoryInferenceManager expect an InferenceId. (#5897)
This PR makes most methods of the TheoryInferenceManager expect an InferenceId.
All classes that inherit from TheoryInferenceManager are adapted accordingly and InferenceIds are passed everywhere.
In some cases, there are no appropriate InferenceIds yet. We use InferenceId::UNKNOWN for the time being and introduce proper values in future PRs.
The InferenceIds are not yet used, but will be used for statistics and debug output.
Gereon Kremer [Thu, 11 Feb 2021 19:00:18 +0000 (20:00 +0100)]
Add InferenceId member to TheoryInference, adapt all derived classes. (#5894)
This PR adds a new InferenceId member to the TheoryInference class.
All classes derived from TheoryInference are adapted accordingly.
Haniel Barbosa [Thu, 11 Feb 2021 16:13:18 +0000 (13:13 -0300)]
[proof-new] Adding a proof-producing ensure literal method (#5889)
The ensureLiteral method in CnfStream may apply CNF conversion to the given literal (for example if it's an IFF), which needs to be recorded in the proof. This commit adds a proof-producing ensureLiteral to ProofCnfStream, which is called by the prop engine if proofs are enabled.
This commit also simplifies the interfaces on ensureLit and convertAtom by removing the preRegistration flag, which was never used.
Gereon Kremer [Thu, 11 Feb 2021 14:55:31 +0000 (15:55 +0100)]
Merge InferenceIds into one enum (#5892)
This PR is the first step in consolidating the various variants of Inferences, InferenceIds and InferenceManagers of the theories.
It merges all InferencedIds into one global enum and makes all theories use them.
Andrew Reynolds [Thu, 11 Feb 2021 14:08:57 +0000 (08:08 -0600)]
Fix spurious assertion failure in regexp normalization (#5852)
Fixes #5816.
Andrew Reynolds [Thu, 11 Feb 2021 13:17:53 +0000 (07:17 -0600)]
Simplify interface for preprocessor (#5890)
This does a minor simplification to the interface for preprocessor. It has a postProcess call that is called after another unrelated call at the SmtSolver level (notifyPreprocessedAssertions) is made. This makes it so that Preprocessor::postProcess is inlined as the last step of process.
Andrew Reynolds [Wed, 10 Feb 2021 19:42:23 +0000 (13:42 -0600)]
Refactor term registration visitors (#5875)
This refactors the term registration visitors (PreRegisterVisitor and SharedTermsVisitor), which are responsible for calling Theory::preRegisterTerm and Theory::addSharedTerm.
The purpose of this PR is to resolve a subtle bug in the implementation of PreRegisterVisitor (see explanation below), and to improve performance in particular on the Facebook benchmarks (where preregistering terms is currently 25-35% of runtime on certain challenge benchmarks).
This PR makes it so that that SharedTermsVisitor now subsumes PreRegisterVisitor and should be run when sharing is enabled only. Previously, we ran both PreRegisterVisitor and SharedTermsVisitor, and moreover the former misclassified when a literal had multiple theories since the d_theories field of PreRegisterVisitor is never reset. This meant we would consider a literal to have multiple theories as soon as we saw any literal that had multipleTheories. After this PR, we run SharedTermsVisitor only which also handles calling preRegisterTerm, since it has the ability to anyways (it computes the same information as PreRegisterVisitor regarding which theories care about a term).
The refactoring merges the blocks of code that were copy and pasted in term_registration_visitor.cpp and makes them more optimal, by reducing our calls to Theory::theoryOf.
FYI @barrettcw
Andrew Reynolds [Wed, 10 Feb 2021 16:27:44 +0000 (10:27 -0600)]
Fix open proof for factoring lemma (#5885)
We need to add to the current proof, regardless of whether we have used the factor skolem previously.
Fixes bugs found by @HanielB on SMT-LIB runs.
Andrew Reynolds [Wed, 10 Feb 2021 15:11:02 +0000 (09:11 -0600)]
Simplify method for inferring proxy lemmas in strings (#5789)
This PR simplifies our heuristic for inferring when an explanation for a strings lemma can be minimized based on proxy variable definitions. In particular, we do not turn solved equalities for proxy variables into substitutions. This aspect of the heuristic is incompatible with the new eager solver work, and moreover is buggy since substitutions should not be applied within string terms. The latter was leading the incorrect models on the 2 issues fixed by this PR.
Current results on the eager solver on SMT-LIB shows this change has very little performance impact.
Fixes #5692, fixes #5610.
Andrew Reynolds [Wed, 10 Feb 2021 02:43:59 +0000 (20:43 -0600)]
Remove track instantiations infrastructure (#5883)
This was used in the old method for unsat core tracking for instantiation lemmas, which will soon be subsumed.
This is also work towards eliminating the dependencies on quantifiers engine from Instantiate.
Andrew Reynolds [Wed, 10 Feb 2021 02:07:33 +0000 (20:07 -0600)]
Optimize get skolems method (#5876)
This method is used to determine which skolems have definitions according to term formula removal. This optimizes the method using attributes similar to how expr::getFreeVariables works.
It will be used heavily for SAT relevancy. We should also consider updating the justification heuristic to use this method.
Andrew Reynolds [Wed, 10 Feb 2021 00:21:56 +0000 (18:21 -0600)]
Do not traverse quantifiers in term formula removal (#5859)
Our current policy for term formula removal leaves quantifier bodies unchanged. This simplifies the code based on this observation.
Mathias Preiner [Tue, 9 Feb 2021 23:18:14 +0000 (15:18 -0800)]
cmake: Make Python3 default and improve toml error messages. (#5884)
./configure.sh will now fail if Python3 is not installed on the system. Since Python2 is now deprecated the user has to explicitly enable it via --python2. This commit also removes the --python3 configure flag.
Andrew Reynolds [Tue, 9 Feb 2021 22:09:54 +0000 (16:09 -0600)]
Eliminating dependencies from inst utils (#5882)
Towards eliminating dependence on QuantifierEngine from inst_match_trie.
Andrew Reynolds [Tue, 9 Feb 2021 21:35:40 +0000 (15:35 -0600)]
Make term database optionally SAT-context-dependent (#5877)
This makes the terms registered to the term database (those considered by E-matching) optionally stored in a SAT-context-dependent manner. The motivation is to have a more flexible/fine-grained set of terms considered by E-matching, e.g. if preregistration becomes lazier in the future.
This uncovered 2 issues:
The induction techniques in "conjecture generator" were using private interfaces, this PR removes the friend relaionship and cleans the code
The conflict-based instantiation module was accessing the signature tables for BOUND_VARIABLES when an operator of an APPLY_UF was a BOUND_VARIABLE. This is possible when options::ufHo is enabled. This makes conflict-based instantiation skip such terms.
Aina Niemetz [Tue, 9 Feb 2021 20:04:13 +0000 (12:04 -0800)]
google test: expr: Migrate node_manager_black. (#5857)
Aina Niemetz [Tue, 9 Feb 2021 18:40:06 +0000 (10:40 -0800)]
google test: main: Migrate interactive_shell_black. (#5878)
Aina Niemetz [Tue, 9 Feb 2021 17:47:53 +0000 (09:47 -0800)]
google test: expr: Migrate type_cardinality_black. (#5871)
Aina Niemetz [Tue, 9 Feb 2021 16:01:29 +0000 (08:01 -0800)]
google test: expr: Migrate node_self_iterator_black. (#5865)
Haniel Barbosa [Tue, 9 Feb 2021 03:37:10 +0000 (00:37 -0300)]
[quantifiers] Fix prenex computation (#5879)
Previously our prenex computation could generate quantifiers of the form forall x y y. F, which would lead to an assertion failure in getFreeVariablesScope, as it assumes that no shadowing occurs. This commit makes the prenex computation take a set rather than a vector, thus avoiding duplications of prenexed variables. It also changes mkForall to take a constant vector, since it does not modify the given vector.
Fixes #5693
Aina Niemetz [Tue, 9 Feb 2021 01:44:21 +0000 (17:44 -0800)]
google test: expr: Migrate type_node_white. (#5872)
Andrew Reynolds [Mon, 8 Feb 2021 22:50:16 +0000 (16:50 -0600)]
Use quantifiers inference manager for lemma management (#5867)
Towards eliminating dependencies on quantifiers engine.
This replaces the custom implementation of lemma management in quantifiers engine with the standard one.
It makes a few minor changes to the standard inference manager classes to ensure the same behavior for quantifiers.
Note that some minor changes in behavior are introduced in this PR, such as being more consistent about caching/rewriting lemmas. This should not have any major impact.
Andrew Reynolds [Mon, 8 Feb 2021 21:55:32 +0000 (15:55 -0600)]
Fix disequality between seq.unit terms (#5880)
This adds a missing inference for disequality between seq.unit terms, which was not handled previously.
Fixes #5666.
Aina Niemetz [Mon, 8 Feb 2021 20:03:05 +0000 (12:03 -0800)]
google test: expr: Migrate node_white. (#5869)
Haniel Barbosa [Mon, 8 Feb 2021 19:32:18 +0000 (16:32 -0300)]
Fix dumping of assertions for monolithic preprocessing passes (#5866)
Previously we were unable to dump assertions in ProcessAssertions::apply for the definition-expansion, simplify and repeat-simplify passes.
Andrew Reynolds [Mon, 8 Feb 2021 18:29:58 +0000 (12:29 -0600)]
Remove support for inst closure (#5874)
This was a feature implemented for "Deciding Local Theory Extensions via E-matching" CAV 2015 that is not used anymore, and will be a burden to maintain further with potential changes to term database.
It also simplifies the TermDatabase::addTerm method (which changed indentation).
Aina Niemetz [Mon, 8 Feb 2021 17:55:38 +0000 (09:55 -0800)]
Use consistent names for fixtures in unit tests. (#5863)
Aina Niemetz [Mon, 8 Feb 2021 17:26:32 +0000 (09:26 -0800)]
google test: expr: Migrate node_traversal_black. (#5868)
Andrew Reynolds [Mon, 8 Feb 2021 15:17:31 +0000 (09:17 -0600)]
Avoid spurious traversal of terms during preregistration (#5860)
This simplifies a few places in the code which unecessarily traverse terms during preregistration (which already traverses terms).
Andrew Reynolds [Sat, 6 Feb 2021 01:14:01 +0000 (19:14 -0600)]
Do not combine theories if theory engine needs check (#5861)
In rare cases, theory combination would be run when theory engine still needs check. This was limited to cases where the output channel is used but no lemmas were sent (TheoryEngine::needCheck() vs. d_lemmasAdded).
This led to problems in the theory of sets, which does not run a full effort check if theory engine needs check (since it knows it will be called to check again). However, running theory combination in these cases is not safe since theory of sets computes information pertaining to the care graph during its full effort check. Running theory combination otherwise would lead to theory of sets using stale data, leading to crashes due to terms not appearing in the equality engine.
This fixes #4124 (which appears not to trigger on master anyways currently).
This bug has also appeared on my sat relevancy development branch, hence fixing on master.
Aina Niemetz [Fri, 5 Feb 2021 22:32:33 +0000 (14:32 -0800)]
google test: expr: Migrate symbol_table_black. (#5870)
Andrew Reynolds [Fri, 5 Feb 2021 20:53:47 +0000 (14:53 -0600)]
Minor cleaning of quantifiers engine (#5858)
This member is currently unused.
Aina Niemetz [Fri, 5 Feb 2021 20:11:54 +0000 (12:11 -0800)]
google test: expr: Migrate node_manager_white. (#5864)
Aina Niemetz [Fri, 5 Feb 2021 19:36:32 +0000 (11:36 -0800)]
Remove obsolete include from node_black unit test. (#5862)
Aina Niemetz [Fri, 5 Feb 2021 17:20:46 +0000 (09:20 -0800)]
google test: expr: Migrate node_builder_black. (#5855)
Andrew Reynolds [Fri, 5 Feb 2021 16:04:30 +0000 (10:04 -0600)]
Miscellaneous cleaning in theory engine (#5854)
This statistic is unused, I believe it is leftover from deleted code.
yoni206 [Thu, 4 Feb 2021 23:46:12 +0000 (15:46 -0800)]
Adding an option to optimize polite combination for datatypes (#5856)
This PR makes the optimization introduced in
bbca987 optional.
Andrew Reynolds [Thu, 4 Feb 2021 22:55:00 +0000 (16:55 -0600)]
Introduce quantifiers registry utility (#5829)
This is a simple module for determining which quantifiers module has ownership of quantified formulas.
This is work towards eliminating dependencies of quantifiers modules.
Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.
yoni206 [Thu, 4 Feb 2021 21:58:38 +0000 (13:58 -0800)]
Clarifying documentation of `--static-binary` (#5844)
The documentation regarding --static-binary is improved.
Andrew Reynolds [Thu, 4 Feb 2021 21:18:05 +0000 (15:18 -0600)]
Eliminate equality query dependence on quantifiers engine (#5831)
This class will be renamed "RepSelector" on a future PR. It no longer needs to depend on quantifiers engine and can be initialized after the modules it depends on.
Haniel Barbosa [Thu, 4 Feb 2021 14:59:56 +0000 (11:59 -0300)]
[proof-new] Catch trivial cycles in SAT proof generation (#5853)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare
case (i.e., not previously in our regressions!!) in which we generate
a trivial cycle during SAT proof generation, which can lead to
problematic cycles when expanding MACRO_RESOLUTION steps. For example,
we can go from
l1 v l2 ~l1 v l3 ~l2 v l3
(ok) ------------------------------
l3
in which l3 = l1 v l2, to
l1 v l2 ~l1 v l3 ~l2 v l3
(bad) ------------------------------
l3 v l3
---------
l3
This commit now catches the trivial cycle before it's generated.
Mathias Preiner [Wed, 3 Feb 2021 20:38:09 +0000 (12:38 -0800)]
Add BV solver bitblast. (#5851)
This PR adds a new bit-blasting BV solver, which can be enabled via --bv-solver=bitblast. The new bit-blast solver can be used instead of the lazy BV solver and currently supports CaDiCaL and CryptoMiniSat as SAT back end.
Haniel Barbosa [Wed, 3 Feb 2021 15:11:26 +0000 (12:11 -0300)]
[proof-new] Fix MACRO_RESOLUTION expansion for singleton clause corner case (#5850)
Evaluating the proof infrastructure in SMT-LIB has uncovered a rare case (i.e., not previously in our regressions!!) in which the resulting clause from crowding literal elimination is a singleton. This commit makes the expansion code robust to that and adds an example of a problematic benchmark as a regression.
Also improves a bit tracing and some comments.
Andrew Reynolds [Tue, 2 Feb 2021 21:12:45 +0000 (15:12 -0600)]
(proof-new) Miscellaneous fixes and regressions (#5841)