From 6898ab93a3858e78b20af38e537fe48ee9140c58 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Thu, 29 Oct 2020 10:00:08 -0500 Subject: (proof-new) Update the strings inference manager for proofs (#5220) This updates the inference manager in strings in two ways: (1) It now inherits from InferenceManagerBuffered, meaning that the custom methods for process the current pending lemma/fact vectors are removed in favor of the standard ones. (2) It has support for proof generation via the InferProofCons utility. This PR standardizes three methods processFact, processLemma, and processConflict which take InferInfo and processes any string-specific behavior pertaining to processing facts, lemmas and conflicts with the inference manager. These methods are intended to preserve the previous behavior of this class. --- src/theory/strings/infer_info.h | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'src/theory/strings/infer_info.h') diff --git a/src/theory/strings/infer_info.h b/src/theory/strings/infer_info.h index 13e9a3f64..4c5674d2b 100644 --- a/src/theory/strings/infer_info.h +++ b/src/theory/strings/infer_info.h @@ -21,6 +21,7 @@ #include #include "expr/node.h" +#include "theory/theory_inference.h" #include "util/safe_print.h" namespace CVC4 { @@ -347,6 +348,8 @@ enum LengthStatus LENGTH_GEQ_ONE }; +class InferenceManager; + /** * An inference. This is a class to track an unprocessed call to either * send a fact, lemma, or conflict that is waiting to be asserted to the @@ -368,11 +371,15 @@ enum LengthStatus * - (main equality) x ++ y ++ v1 = z ++ w ++ v2, * - (length constraint) len(y) = len(w). */ -class InferInfo +class InferInfo : public TheoryInference { public: InferInfo(); ~InferInfo() {} + /** Process this inference */ + bool process(TheoryInferenceManager* im, bool asLemma) override; + /** Pointer to the class used for processing this info */ + InferenceManager* d_sim; /** The inference identifier */ Inference d_id; /** Whether it is the reverse form of the above id */ -- cgit v1.2.3