summaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-09-22ICP-based solver for nonlinear arithmetic (#5017)Gereon Kremer
This PR adds a new icp-based solver to be integrated into the nonlinear extension. It is not meant to be used as a stand-alone ICP solver. It does not implement splits (only propagations) and implements a rather aggressive budget mechanism that aims to quickly stop propagation to allow other solvers to take over. Additionally, it enforces a maximum bit size to avoid divergence.
2020-09-21Require dumping in a dumping test (#5108)yoni206
Add ; REQUIRES: dumping to a dumping test. Fixes nightlies.
2020-09-21(proof-new) Add the arrays proof checker (#5047)Andrew Reynolds
Includes adding the standard method for constructing the extensionality skolem using the skolem manager.
2020-09-20More flexible design for model manager distributed (#4976)Andrew Reynolds
This PR makes it so that the distributed model manager can be used independently of the architecture for equality engine management for theories, meaning the choice of using a separate equality engine for the model can be done in both the current distributed architecture, or the proposed central architecture (where there would be 2 equality engines, the central one and the model one). The "central model manager" on the other hand will only be combined with the central architecture. This will make it easier to test the centralized equality engine manager, since all things related to model construction can be preserved when using a central architecture. This PR moves some of the responsibilities from the (distributed) equality engine manager to the distributed model manager, including the management of the context of the model equality engine and the allocation of its equality engine. This PR is not intended to make any behavior changes to the current architecture.
2020-09-19Standardize equality engine notifications in sets (#5098)Andrew Reynolds
2020-09-18Fix assertion list for globally defined recursive functions (#5084)Andrew Reynolds
This was uncovered by a (spurious) proof checking failure on proof-new.
2020-09-18Add the shared solver (#4982)Andrew Reynolds
This PR adds the definition for the "shared solver", it does not connect it to TheoryEngine/CombinationEngine yet. This is an object that behaves like a "glue" theory solver and has a special role in TheoryEngine. In the current architecture, the "SharedTermsDatabase" is the "shared solver", although in the central architecture, the shared solver will be required to behave differently. This PR adds the abstract definition of shared solver, where notice SharedSolverDistributed is a thin layer on top of SharedTermsDatabase. In a followup PR, CombinationEngine will maintain a shared solver and ~5 blocks of code in TheoryEngine will be callbacks to the SharedSolver. Also, eventually the code for SharedTermsDatabase should be split: the parts involving equality reason/propagation/explanation should be migrated into SharedSolverDistributed, and the parts related to registration will remain in SharedTermsDatabase (to also be used in the planned SharedSolverCentral). FYI @barrettcw
2020-09-18bv2int: quantifiers support (#5080)yoni206
This PR adds quantifiers support for bv2int preprocessing pass, and adds regressions that use quantifiers.
2020-09-18Fix muzzled builds (#5093)Andres Noetzli
Commit 2c2f05c moved some function definitions from dump.h to dump.cpp, which is good. However, the corresponding definitions for muzzled builds weren't moved, so muzzled builds defined the operator << multiple times. This made our nightly competition build fail. This commit fixes the issue by moving the alternative definitions to the source file as well.
2020-09-18[proof-new] Proof utilities for normalizing clauses at the Node level (#5089)Haniel Barbosa
Extends Theory Proof Step Buffer. These utilities are used so that we can account for the fact that Minisat silenly does these transformations on added clauses.
2020-09-18Logic exception for arrays indexed by arrays (#5073)Andrew Reynolds
This throws a logic exception when a term of array type whose index is also an array is registered to the theory of arrays. It refactors the preRegisterTermInternal method of arrays so that all non-equality terms are added to the equality engine in the same block of code, which also checks for the type. Fixes #4237. FYI @barrettcw
2020-09-18[Strings] Fix extended equality rewriter (#5092)Andres Noetzli
Fixes #5090. Our extended equality rewriter was performing the following unsound rewrite: (= (str.++ Str13 Str5 Str16 Str13) (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs")) ---> (and (= (str.++ Str13 Str5) Str5) (= (str.++ Str16 Str13) (str.++ Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs"))) The rule being applied was SPLIT_EQ_STRIP_R. The rewrite was applied due to the following circumstances: The rewriter found that (str.++ Str13 Str5) is strictly shorter than (str.++ Str5 Str16 Str13 "cjyfqapanogtdznjbtqlfrmmfauwjdpvnhfpfhzsxaarlfvlvs") The rewriter stripped the symbolic length of the former from the latter stripSymbolicLength() was only able to strip the first component, so there was a remaining length of (str.len Str13) The rule SPLIT_EQ_STRIP_R, however, was implicitly assuming that the symbolic length can either be stripped completly or not at all and was not considering the case where only a part of the length can be stripped. The commit adds a flag to stripSymbolicLength() that makes the function only return true if the whole length can be stripped from the input. The commit also refactors the code in stripSymbolicLength() slightly. Note: It is not necessary to try to do something smart in the case where only a partial prefix can be stripped because the rewriter tries to apply the rule to all the different prefix combinations anyway.
2020-09-17(proof-new) Updates to proof node updater algorithm (#5088)Andrew Reynolds
This updates the proof node updater so that we apply updates to a fixed point, stopping if the proof node is not updated or if the callback explicitly tells us not to continue. This also fixes an issue where proof nodes would be updated to SCOPE and incorrectly traversed after updating. This additionally adds debugging feature to proof node updater to track the moment at which an unexpected free assumption is introduced by an update.
2020-09-17(proof-new) Rewrites involving operators in term conversion proof generator ↵Andrew Reynolds
(#5072) In some cases, e.g. witness form conversion, we require traversing to operators in term conversion proofs. This updates the term conversion generator to support (term-context-sensitive) rewrites involving operators using HO_CONG. This requires updating the term context utilities with support for operators.
2020-09-17(proof-new) Fixes for theory engine proof generator (#5087)Andrew Reynolds
Fixes an issue where conflicts stored in the theory engine proof generator where expecting to be (=> F false) instead of (not F).
2020-09-17[proof-new] Have mkScope agnostic to True assumptions (#5086)Haniel Barbosa
2020-09-17(cad-solver) Fix square-free-basis computation (#5085)Gereon Kremer
This PR fixes a subtle issue when making the polynomials of two subsequent (overlapping) intervals relative square-free. We now make sure that the resulting polynomials are ignored (if constant) or pushed to the lower dimension (if lower main variable). Also, we now appropriately update the main polynomials of the corresponding intervals.
2020-09-17Reduce recursion in term formula removal (#5052)Andrew Reynolds
This reduces the use of recursion in term formula removal module. The recursion depth is now limited to the number of term positions on a path where a formula must be removed, instead of being limited to the overall formula depth. This PR also fixes some documentation. Notice for its main cache d_tfCache, this class uses a CDInsertHashMap (instead of a CDHashMap) which does not allow inserting more than once, hence an auxliary "processedChildren" vector had to be introduced to track whether we have processed children. It's not clear to me whether we should just use the more standard CDHashMap, which would simplify this. One non-linear arithmetic regression went unsat -> unknown, I added --nl-ext-tplanes to fix this. This should fix #4889. It is possible to further reduce the recursion in this pass, which can be done on a followup PR if needed.
2020-09-17Use new inference manager in transcendental solver (#5022)Gereon Kremer
This refactors the transcendental solver to add lemmas to the new inference manager instead of using the old lemma collection scheme.
2020-09-17Do not allow to build Python bindings if building statically (#4784)Andrew V. Jones
This PR disables building the Python bindings if you're doing a static build (which makes sense, because there's no such thing as a "static" Python module). Signed-off-by: Andrew V. Jones andrew.jones@vector.com
2020-09-16Further standardization of datatypes (#5076)Andrew Reynolds
We now have no custom calls to equality engine explain, and only 2 manual calls to equality engine (in its entailment check). This also updates the notify class to the standard one. This commit makes datatypes ready to start work on proofs.
2020-09-16Dumping internal define-funs with no arguments (#5077)yoni206
Currently, --dump=assertions:... fails if a define-fun command is executed internally (an example for this can be found here. The failure occurs because the printer expects a range type whenever a define-fun command is executed. However, when this command is used for 0-ary functions (variables), the getter for the range fails. This PR fixes this by asking for a range only if the type is indeed a function. Otherwise, the original type is printed. A test that currently fails but passes with this PR is included.
2020-09-16Only rewrite replace_re(_all) if regexp is const (#5075)Andres Noetzli
Fixes #5074. This commit fixes an issue in the rewriter of str.replace_re and str.replace_re_all. For both operators, we do two kinds of rewrites: (1) If the first argument is a constant, then we check whether the regular expression appears in that constant and (2) we check whether the regular expression matches the empty string. Both of those checks were assuming a constant regular expression but there was no guard in place for it. This commit adds the missing guard.
2020-09-16Dump commands in internal code using command printing functions. (#5040)Abdalrhman Mohamed
This is work towards migrating commands to the new API. Internal code that creates command objects just for dumping is replaced with direct calls to functions that print the those commands.
2020-09-16Add buffered inference manager to TheorySep (#5038)Andrew Reynolds
This makes TheorySep use a standard buffered inference manager. Notice the behavior in TheorySep::doPending was simplified to assert both facts and lemmas. Previously, this was doing something strange: if there were any lemmas, then both facts and lemmas would be processed as lemmas, otherwise the facts would be processed as facts. Notice that TheorySep currently does not use facts by default. This design can be addressed in the future. Note this PR eliminates the need for a custom explain method in TheorySep.
2020-09-16[proof-new] Adds Lazy CDProof chain data-structure (#5060)Haniel Barbosa
A proof generator to facilitate connection of locally independent but globally dependent proofs. In particular this will be used to model the resolution chains done in Minisat.
2020-09-16Refactor collectModelInfo in TheoryArith (#5027)Andrew Reynolds
This is work towards updating the arithmetic solver to the new standard, and in particular isolating TheoryArithPrivate as the "linear solver", and TheoryArith as the overall approach for arithmetic. This transfers ownership of the non-linear extension from TheoryArithPrivate to TheoryArith. The former still has a pointer to the non-linear extension, which will be removed with further refactoring. This PR additionally moves the code that handles the interplay of the non-linear extension in TheoryArithPrivate::collectModelInfo to TheoryArith, and simplifies the model interface for TheoryArithPrivate.
2020-09-15bv2int: support models in tests (#5068)yoni206
Previous changes in this preprocessing pass have already enabled model generation when using it. However, the satisfiable tests still had --no-check-models. The changes in this PR: All --no-check-models from current tests for the preprocessing pass are removed. Refactoring of the relevant part of the code. Solves CVC4/cvc4-projects#128. Remark: disabling white-spaces when reviewing this PR is recommended.
2020-09-16[proof-new] Extending eqproof conversion to HO congruence (#5071)Haniel Barbosa
2020-09-16[proof-new] Resolution rules and checkers (#5070)Haniel Barbosa
2020-09-15[proof-new] A simple proof generator for buffered proof steps (#5069)Haniel Barbosa
This commit also modifies proof equality engine to use this new proof generator rather than the FactProofGenerator, on which this new one is based. Co-authored-by: Andrew Reynolds <andrew.j.reynolds@gmail.com>
2020-09-15(proof-new) Make proofs mandatory in proof equality engine (#5059)Andrew Reynolds
All uses of proof equality engine are now guarded such that the ordinary equality engine is used when proofs are not enabled. Thus, we can make proofs mandatory in proof equality engine. This eliminates the need for some guards. Some indentation changed, but there are no additions in this PR.
2020-09-15Move sets member propagation to SolverState (#5045)Andrew Reynolds
This eliminates the parent relationship from solver state to theory sets.
2020-09-14Rename system tests to api tests and remove obsolete Java test. (#5066)Aina Niemetz
2020-09-14Move quantifiers engine private to own file (#5053)Andrew Reynolds
This moves and renames the quantifiers engine private class to QuantifiersModules. This is in preparation for using a standard state and inference manager object in TheoryQuantifiers and QuantifiersEngine. Initializing quantifiers engine is a bit non-standard since it is intentionally a separate entity from TheoryQuantifiers. However, the plan is for quantifiers engine to use the state and inference manager of TheoryQuantifiers. This PR additionally moves the initialization of quantifiers modules to a QuantifiersEngine::finishInit() method. The motivation for is that we do not have a state and inference manager during construction of QuantifiersEngine, since these will live in TheoryQuantifiers and will be passed to QuantifiersEngine during TheoryQuantifiers::finishInit. This means that we need a final pass to initialize quantifiers engine after these are initialized, which thus must come as the last step of TheoryEngine::finishInit. The next PR will connect the state and inference manager to QuantifiersEngine during TheoryQuantifiers::finishInit. Then, the plan is for many of the core utilities in QuantifiersEngine to migrate to state/inference manager, and finally for its modules to reference state and inference manager instead of QuantifiersEngine.
2020-09-14Fix needsModel method for CEGQI (#5048)Andrew Reynolds
There was a bug in CEGQI's needModel method which could say that it doesnt need a model built when there are no active quantifiers. However, computing active quantifiers is not done in QuantifiersEngine::check until after this method is called, meaning it was using stale data on whether a quantifier was active or not. This could lead to the use of bogus models in CEGQI in incremental mode in some corner cases, leading to the assertion failure in #5019. Fixes #5019.
2020-09-14Standard equality engine notify class for Theory (#5042)Andrew Reynolds
This makes a standard equality engine notify class that forwards the 3 mandatory callbacks to the provided inference manager (the other 3 callbacks may be specific to the theory). It updates TheoryUF to use this class, other theories will be updated to this style as more inference manager are added. Notice that we could also forward the other 3 callbacks in this class to Theory, making eqNotifyNewClass, eqNotifyMerge, and eqNotifyDisequal virtual methods in Theory, which can be done on a future PR if needed.
2020-09-14Fix ABC build (#5061)Andres Noetzli
For some reason, our ABC build was including cnf_stream.h in an extern "C" block instead of outside of it, which made the build fail because the header indirectly includes cdqueue.h, which uses templates. This change is older (e9bfbb2) but only started causing problems with our nightly builds recently.
2020-09-14Interpolation: Add implementation for SyGuS interpolation module (final) (#5063)Ying Sheng
Add interface for SyGuS Interpolation module. Adding the API for (get-interpol s B), which is aim for computes an I that A->I and I->B. Here A is the assertions in the stack.
2020-09-14bv2int: simpler translation for plus and times (#5055)yoni206
This PR makes the translation of plus and times by: using plain mod rather than introducing a skolem. If this proves to be a bottleneck, we can try to tackle it where mod is treated in the solver in the future. This will make it easier to introduce support for quantifiers, as we don't need to introduce new variables under quantification. Making sure everything is binarized in more places of the translation.
2020-09-14Refactoring the rewriter of sets (#4856)Andrew Reynolds
Changes it so that we don't flatten unions if at least one child is non-constant, since this may lead to children that are non-constant by mixing constant/non-constant elements and is generally expensive for large unions of singleton elements. The previous rewriting policy was causing an incorrect model in a separation logic benchmark reported by Andrew Jones, due to unions of constant elements that were unsorted (and hence not considered constants). We now have the invariant that all subterms that are unions of constant elements are set constants. Note this PR changes the normal form of set constants to be (union (singleton c1) ... (union (singleton cn-1) (singleton cn) ... ) not (union ... (union (singleton c1) (singleton c2)) ... (singleton cn)). It changes a unit test which was impacted by this change which was failing due to hardcoding the enumeration order in the unit test. The test is now agnostic to the order of elements.
2020-09-14Fix type for Windows build (#5062)Andres Noetzli
The BVToInt preprocessing pass was using uint, which appears to be undefined when we cross-compile for Windows. This commit fixes the issue by using size_t.
2020-09-14Standardize uses of inference manager in datatypes (#5035)Andrew Reynolds
Datatypes now has an inference manager. This is work towards making it use the inference manager in all places where it should. In particular, this makes many of the places where conflicts are determined using `InferenceManager::conflictExp` (explained conflict) instead of `InferenceManager::conflict` + custom calls to explain in TheoryDatatypes. The goal here is to ensure that all explanations from the equality engine are managed by inference manager, which is required for proofs.
2020-09-11(proof-new) Add SMT proof manager (#5054)Andrew Reynolds
This module is responsible for constructing the proof checker, proof node manager, and implementing dumping and checking of the final proof. This PR includes setting up some connections into the various modules for proof production.
2020-09-11(proof-new) Update TheoryEngine lemma and conflict to TrustNode (#5056)Andrew Reynolds
This updates the theory engine interfaces for conflicts and lemmas to be in terms of TrustNode not Node. This also updates the return value of getExplanation methods in TheoryEngine to TrustNode, but it does not yet add the proof generation code to that method yet, which will come in a separate PR.
2020-09-11Move finite model minimization to UF last call effort (#5050)Andrew Reynolds
This moves model minimization happen in TheoryUF's last call effort check instead of being a custom call in quantifiers finite model finding. This is both a better design and avoids bugs when quantifiers are not enabled (for QF_UF+cardinality constraints). Fixes #4850.
2020-09-11(proof-new) Handle mismatched assumptions in proof equality engine during ↵Andrew Reynolds
mkScope (#5012) This modifies the fix for Boolean equalities with constants so that is addressed lazily during ProofNodeManager mkScope instead of when asserting assumptions to the proof equality engine. This ensures that the default method for asserting facts to the equality engine for external assertions does not have any special cases. A previously abandoned solution to this issue had made this a part of CDProof. Instead, this PR modifies the mkScope method only. The fix makes mkScope robust to any assumption mismatches in mkScope that can be fixed by rewriting, not just Boolean equality with constants. It is intended to be used infrequently as a last resort when mkScope has mismatched assumptions. The handling of mismatches due to symmetry remains in this method.
2020-09-11(proof-new) Use deep copy for final lemma step in proof equality engine (#5013)Andrew Reynolds
Previously, strings on proof-new used a ProofStepBuffer for deriving the final conclusion of lemmas in proof equality engine (assertLemma). This was recently changed to use the more standard ProofGenerator interface of assertLemma. However, there was a bug in this method: the steps from this proof need to be deep copied into the proof we are generating or otherwise the explanation of these literals are not connected in the CDProof. This updates the proof equality engine so that it instructs the proof generator to do a deep copy in this case. Notice this is very rarely more than a single step.
2020-09-10Add witness to cvc printer. (#5057)Andrew Reynolds
2020-09-10bv2int: refactoring the main translation loop (#5051)yoni206
This PR introduces a refactoring of the main translation loop in bv2int preprocessing pass. Many parts are wrapped by helper functions and so the main loop becomes smaller. remark: selecting "Hide whitespace changes" cuts the diff by ~50%.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback