summaryrefslogtreecommitdiff
path: root/src/theory
AgeCommit message (Collapse)Author
2021-11-04Merge branch 'master' into privateGetprivateGetAndrew Reynolds
2021-11-04Update theory.hAndres Noetzli
2021-11-03Refactor skolem construction (#7561)Andrew Reynolds
This makes all methods for constructing skolems local to SkolemManager. It removes infrastructure for node manager listeners being notified when skolems are constructed. This was used for 2 things: (1) The old dumping infrastructure, where skolems could contribute in part to traces to print benchmarks. This code will be deleted soon. (2) The miplib preprocessing pass, which used this functionality to listen to what skolems were constructed, and subsequently assumed these skolems coincided with what Boolean variables appeared in assertions. This is highly error prone, and has been replaced by a simple traversal to collect Boolean variables in assertions. This is in preparation for a lazy lambda lifting technique, which will require more infrastructure in SkolemManager.
2021-11-03Formalize more string skolems (#7554)Andrew Reynolds
This properly formalizes all string skolems used in reduction and preprocessing. This avoids proof checking failures due to non-deterministism when checking steps for these modules. Fixes cvc5/cvc5-projects#334. Fixes cvc5/cvc5-projects#331.
2021-11-03Fix preregistration for floating point theory (#7558)Andrew Reynolds
Preregistering terms must always add them to the equality engine of TheoryFp, otherwise there may be preregistered terms that do not occur in the equality engine of TheoryFp, thus leading to crashes during theory combination. Fixes cvc5/cvc5-projects#329.
2021-11-02bv: Disable equality engine for --bitblast=eager and bitblast-internal. (#7560)Mathias Preiner
When we eagerly bitblast to the main SAT solver, we have to make sure that we don't use the equality engine in order to not start propagating equalities below BITVECTOR_EAGER_ATOM predicates. Fixes the nightly failure.
2021-11-02bv: Remove remaining Rewriter::rewrite calls. (#7545)Mathias Preiner
2021-11-01Eliminate calls to Rewriter::rewrite and options:: in sets and bags (#7550)Andrew Reynolds
There is 1 remaining call to Rewriter::rewrite in the bags type enumerator which is not straightforward to eliminate; it should perhaps call an intermediate call to a normal form utility instead of the full rewriter.
2021-11-01Weaken assertion in CEGQI (#7548)Andrew Reynolds
The assertion can be violated in mixed Int/Real arithmetic. The instantiator utility nevertheless safe guards Int vs Real subtyping. Fixes #7537.
2021-11-01bv: Remove layered solver. (#7455)Mathias Preiner
This commit removes the old bit-vector solver code.
2021-11-01Fix upwards closure for relations (#7515)Andrew Reynolds
This PR fixes an issue where we did compute upwards closure (for join, product, etc.) on equivalence classes whose membership cache had already been initialized (perhaps recursively from the computation of upwards/downwards closures on other terms). It also generalizes the fix from #7511. Instead of doing explicit splitting, we mark shared terms and let theory combination (when necessary) do splitting. This is required to fix a more general version of the benchmark from the previous PR, where instead now a term c+1 is used in a position that is relevant to a join. It disables a regression that times out after these fixes, and does further cleanup.
2021-11-01Replace more static options accesses (#7531)Gereon Kremer
This replaces a bunch of static accesses to options (`options::foo()`) by using the `EnvObj::options()` method.
2021-10-31Fix soundess issue for bags with negative multiplicity (#7539)mudathirmahgoub
This PR fixes soundness issues found by cvc5 fuzzy sygus when it answers unsat for sat problems. One error was with the rewrite rule (bag.count x (bag x c) = c which did not account for cases when c is negative. This conflicts with fact that all multiplicities are non-negative. Another error was that the difference_remove inference rule didn't consider the negative case for (count e B) (= (count e (difference_remove A B)) (ite (= (count e B) 0) (count e A) 0))) ; not enough (= (count e (difference_remove A B)) (ite (<= (count e B) 0) (count e A) 0))) ; the right rule
2021-10-31Remove assertSkeleton for bag elements during model building (#7538)mudathirmahgoub
This PR fixes a bug found by cvc5 fuzzy sygus.
2021-10-29Fix proof of nl lemma for a corner case (#7530)Gereon Kremer
This PR fixes the proof generated for the nonlinear monomial bounds check lemmas. In some cases, it implies an equality (multiplied by a monomial) not from the equality but from the two weak inequalities. We now properly detect this special case and add a rather involved proof. Fixes cvc5/cvc5-projects#326.
2021-10-29Minor cleanup of proof messages (#7494)Andrew Reynolds
Also deletes unused code encountered in TheoryArrays while investigating cyclic proofs.
2021-10-29Fix model construction for higher order involving irrelevant function terms ↵Andrew Reynolds
(#7526) This fixes a bug in HO model construction where we were communicating information about irrelevant function terms to the model, leading to incorrect models.
2021-10-29Add PfRule ARITH_POLY_NORM (#7501)Andrew Reynolds
This is a coarse grained proof rule for showing that two terms are equivalent up to polynomial normalization. It will be used as a hard coded case in proof reconstruction with DSL granularity.
2021-10-28Fix proof for xor in circuit propagator (#7525)Gereon Kremer
This PR fixes another double negation issue in the circuit propagator. Fixes cvc5/cvc5-projects#332.
2021-10-28[proofs] Fix assertion in EqProof conversion (#7522)Haniel Barbosa
Also improves a few traces. Fixes cvc5/cvc5-projects#330
2021-10-28Properly guard proof construction for STRINGS_EXTF_EQ_REW (#7519)Andrew Reynolds
Fixes one of the issues raised in cvc5/cvc5-projects#331, the other involves missing skolem definitions for str.replace_all_re @4tXJ7f . This properly guards cases of proof reconstruction for STRINGS_EXTF_EQ_REW where an intermediate step in the proof checker inferring something stronger than what it is asked to prove. In particular, substitution+rewriting is more powerful than congruence+rewriting: s=x => (str.<= t s) ----> (= r "") since (str.<= t "") ----> (= r "") but additionally: (str.<= t s) * { s -> x } ----> true, which is possible if s occurs as a subterm of t. The proof reconstruction for STRINGS_EXTF_EQ_REW is not precise as there are several other aspects that are not covered. After this PR, we properly guard and fail to reconstruct if the above issue arises, so the assertion failure will not throw.
2021-10-28Make `Theory::get()` privateAndres Noetzli
Now that theories have been refactored to use common interfaces, they should not access `Theory::get()` anymore because facts are consumed by `Theory::check()`.
2021-10-27Add comments for arith type rules. (#7488)Gereon Kremer
Add comments for the arithmetic type rules. Fixes cvc5/cvc5-projects#273.
2021-10-27Require ITE branches to be first class types (#7508)Andres Noetzli
Fixes cvc5/cvc5-projects#316.
2021-10-27Fix care graph computation for higher-order (#7474)Andrew Reynolds
Since we apply a lazy schema for app completion, this may omit terms from the care graph that are relevant for theory combination. This corrects the care graph for UF when higher-order is enabled by considering the HO_APPLY version of all partially and fully applied prefixes of APPLY_UF terms during TheoryUF::computeCareGraph. Fixes #5741. Fixes #5744. Fixes #5201. Fixes #5078. Fixes #4758.
2021-10-27Fix model unsoundness for relation join (#7511)Andrew Reynolds
This fixes a model unsoundness issue in the theory solver for relations.
2021-10-27Avoid non-terminating check with assumptions in strings rewriter (#7503)Andrew Reynolds
These rewrites introduce the possibility of non-termination in the rewriter, as demonstrated in the included regression. Instead, these rewrites are now moved to the extended rewriter.
2021-10-27Deterministic variables for RE elim (#7489)Andrew Reynolds
Fixes #6766.
2021-10-26Disable automatic symmetry in proofs of theory explanations (#7493)Andrew Reynolds
This avoids cyclic proofs in a rare case where theory explanations involve an equality and its symmetric form. This PR disables auto-symmetry on lazy proofs used for theory explanations, which is slightly less convenient but avoids potentials for cyclic proofs. Note this complication would not arise if the theory engine did not allow non-rewritten equalities to be propagated between theories. Fixes cvc5/cvc5-projects#311.
2021-10-26[proofs] Fix and simplify CHAIN_RESOLUTION checker (#7492)Haniel Barbosa
Fixes cvc5/cvc5-projects#319
2021-10-25Add new method for enumerating unsat queries with SyGuS (#7459)Andrew Reynolds
This adds a new option for --sygus-query-gen=unsat to generate unsat queries (previously, only satisfiable queries were supported). The algorithm can be seen as a variant of abduction where we conjoin predicates that both (1) refine the current model and (2) avoid repeated unsat cores. It does some minor refactoring of ExprMinerManager to support the new module.
2021-10-25Fix spurious checks to closed proofs (#7484)Andrew Reynolds
This leads to issues when (1) proofs are enabled, (2) unsat cores are enabled and full proofs are disabled in a subsolver. This is the case for the abduction algorithm that uses unsat core learning, when proofs are explicitly enabled. This led to spurious assertion failures when testing proof new.
2021-10-25Fix more missing uses of CDProof::isSame (#7491)Andrew Reynolds
Fixes cvc5/cvc5-projects#306.
2021-10-25Add inference for count map (#7264)mudathirmahgoub
2021-10-24Add new eager conflict detection in strings for integer equivalence classes ↵Andrew Reynolds
(#7453) Required to address Zelkova bottlenecks. This generalizes the methods for eager prefix/suffix conflicts for strings to do eager lower/upper bound conflicts for integer equivalence classes based on string-specific reasoning about length terms. This avoids cases where Simplex fails to show a concise conflict due to not having access to string reasoning (e.g. strings::ArithEntail) for arithmetic bounds. The approach can still be improved by inferring fixed length for regular expression memberships, analogous to what is done for prefix/suffix conflicts. It also changes EqcInfo to store (str.len x) instead of x for length terms.
2021-10-23Remove spurious assertoin (#7458)Andrew Reynolds
Fixes #7439. That benchmark is now "unknown".
2021-10-22Remove stale pointer to proof node manager from skolemize utility (#7471)Andrew Reynolds
Issue was introduced when cleaning this utility to the new style (to not take explicit pnm).
2021-10-22[proof] Fixing CHAIN_RESOLUTION checker (#7465)Haniel Barbosa
Previously the checker was doing things in a smart way that could lead to issues when a clause coincided with a singleton clause as a literal of another clause within the chain. Fixes cvc5/cvc5-projects#310
2021-10-22Fix out-of-sync pruning in CDCAC proofs (#7470)Gereon Kremer
This PR resolves a subtle issue with CDCAC proofs. The CDCAC proof is maintained as a tree where (mostly) every node corresponds to an (infeasible) interval generated within the CDCAC method. We prune these intervals regularly to get rid of redundant intervals, which also sorts intervals. The pruning however relied on a stable ordering of both intervals and child nodes within the proof tree, as there was no easy way to map nodes back to intervals. This PR adds an objectId field to the proof tree nodes and assigns ids to the CDCAC intervals. This allows for a robust mapping between the two, even if the interval list is reordered. Fixes cvc5/cvc5-projects#313.
2021-10-22Fix another double negation proof issue (#7468)Gereon Kremer
This PR fixes another subtle proof issue in the circuit propagator concerning negated ites. Fixes cvc5/cvc5-projects#309.
2021-10-22Remove `--uf-ho` option (#7463)Andrew Reynolds
This option was previously a way of knowing whether higher-order was enabled, which now should be queried via LogicInfo::isHigherOrder. It also adds an optimization to hasFreeVar required for QCF to be robust and not take a performance hit due to HO operators.
2021-10-22Fix symmetry issue in theory engine conflicts (#7469)Andrew Reynolds
Fixes --check-proofs on proof-new on regress0/strings/issue5384-double-conflict.smt2.
2021-10-22Add more abduction regressions (#7461)Andrew Reynolds
Fixes #5848. This also fixes an issue leftover from #6605 where a spurious assertion failure was thrown. Also introduces subfolder regress/regress1/abduction.
2021-10-22Make CAD proofs user context dependent (#7466)Gereon Kremer
Given that arithmetic lemmas can survive the current (sat) context by being buffered in the inference manager, their proofs need to do as well. This PR changes the CAD proofs to be user context dependent. Fixes cvc5/cvc5-projects#315.
2021-10-22Refactor theory inference manager constructor (#7457)Andrew Reynolds
Eliminates a style where proof node manager was passed as an argument to indicate proofs enabled if non-null. All theory inference managers now check Env::isTheoryProofProducing instead. Since BV did not pass a proof node manager to its inference manager, this PR also incidentally enables equality engine proofs for BV.
2021-10-22Making `IntBlaster` inherit from `EnvObj` (#7431)yoni206
This PR makes the IntBlaster class inherit from EnvObj, along with derived modifications.
2021-10-22Do not use global proxy variable attribute for strings (#7460)Andrew Reynolds
Fixes #6180.
2021-10-22Fix memory management of `ErrorInformation` (#7388)Andres Noetzli
Fixes https://scan6.coverity.com/reports.htm#v37053/p11644/fileInstanceId=125548448&defectInstanceId=32441274&mergedDefectId=1453884.
2021-10-22Make expression mining use configurable options and logic (#7426)Andrew Reynolds
Required for doing options-specific internal fuzzing using SyGuS.
2021-10-21Also fix case of negated ite (#7454)Gereon Kremer
This PR follows #7452 and fixes the proofs generated for backward propagation of negated ite terms.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback