diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-02-11 15:55:31 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-11 15:55:31 +0100 |
| commit | 1d0492104a200f6fa5cc7a1cee539436ee26ea99 (patch) | |
| tree | a66ff6b0bc869f1e84dceb03ddbcc7910e23c77c /src/theory/strings/infer_proof_cons.h | |
| parent | b3f05d5c25facaf0c34ee79faed060bda3f61a8d (diff) | |
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.
Diffstat (limited to 'src/theory/strings/infer_proof_cons.h')
| -rw-r--r-- | src/theory/strings/infer_proof_cons.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/strings/infer_proof_cons.h b/src/theory/strings/infer_proof_cons.h index 1b066b4b3..49fd338b5 100644 --- a/src/theory/strings/infer_proof_cons.h +++ b/src/theory/strings/infer_proof_cons.h @@ -100,7 +100,7 @@ class InferProofCons : public ProofGenerator * In particular, psb will contain a set of steps that form a proof * whose conclusion is ii.d_conc and whose free assumptions are ii.d_ant. */ - void convert(Inference infer, + void convert(InferenceId infer, bool isRev, Node conc, const std::vector<Node>& exp, |