From b8301cde27c455c8da3e9017072a577a0816939b Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 21 Aug 2020 12:08:14 -0500 Subject: Connect the relevance manager to TheoryEngine and use it in non-linear arithmetic (#4930) This PR activates the use of the relevance manager in TheoryEngine and makes use of it (via Valuation) in the non-linear extension in arith. It removes a deprecated hack (addTautology) for doing this. This addresses CVC4/cvc4-projects#113. Note that the best method for relevance is interleaving, where roughly you gain on SMT-LIB: QF_NIA: +484-53 unsat +792-440 sat QF_NRA: +32-19 unsat +57-23 sat However, this PR does not (yet) enable this method by default. Note that more work is necessary to determine which lemmas require NEEDS_JUSTIFY, this PR identifies 2 cases of lemmas that need justification (skolemization and strings reductions). Regardless, the use of the relevance manager is limited to non-linear arithmetic for now, which is only able to answer "sat" when only arithmetic is present in assertions. --- src/theory/arith/nl/nonlinear_extension.h | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) (limited to 'src/theory/arith/nl/nonlinear_extension.h') diff --git a/src/theory/arith/nl/nonlinear_extension.h b/src/theory/arith/nl/nonlinear_extension.h index 6fb8dbbfa..ee58a9e2e 100644 --- a/src/theory/arith/nl/nonlinear_extension.h +++ b/src/theory/arith/nl/nonlinear_extension.h @@ -254,11 +254,12 @@ class NonlinearExtension * ensureLiteral respectively. */ bool checkModel(const std::vector& assertions, - const std::vector& false_asserts, std::vector& lemmas, std::vector& gs); //---------------------------end check model - + /** compute relevant assertions */ + void computeRelevantAssertions(const std::vector& assertions, + std::vector& keep); /** * Potentially adds lemmas to the set out and clears lemmas. Returns * the number of lemmas added to out. We do not add lemmas that have already @@ -293,6 +294,11 @@ class NonlinearExtension NlStats d_stats; // needs last call effort bool d_needsLastCall; + /** + * The number of times we have the called main check method + * (modelBasedRefinement). This counter is used for interleaving strategies. + */ + unsigned d_checkCounter; /** Extended theory, responsible for context-dependent simplification. */ ExtTheory d_extTheory; /** The non-linear model object -- cgit v1.2.3