From 80493d9fa63169f02ff8b3c71622c49c6e068357 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 12 Jun 2020 12:57:05 -0500 Subject: (proof-new) Minor updates to strings base solver (#4606) In preparation for proofs, this PR involves flattening AND and removing spurious true literals in conjunctions. This also updates our policy for applying cardinality, where in some rare cases we were applying cardinality for pairs of string terms for length 0 (e.g. "there is at most 1 eqc of length 0"), which is spurious due to our term registry which always splits on emptiness. --- src/theory/strings/base_solver.h | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'src/theory/strings/base_solver.h') diff --git a/src/theory/strings/base_solver.h b/src/theory/strings/base_solver.h index 334fdf596..b8fb71dd3 100644 --- a/src/theory/strings/base_solver.h +++ b/src/theory/strings/base_solver.h @@ -41,10 +41,7 @@ class BaseSolver using NodeSet = context::CDHashSet; public: - BaseSolver(context::Context* c, - context::UserContext* u, - SolverState& s, - InferenceManager& im); + BaseSolver(SolverState& s, InferenceManager& im); ~BaseSolver(); //-----------------------inference steps -- cgit v1.2.3