diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-06-12 12:57:05 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-06-12 12:57:05 -0500 |
| commit | 80493d9fa63169f02ff8b3c71622c49c6e068357 (patch) | |
| tree | 12d07413edd66d3d40ebcd2a5262b33f395e73d0 /src/theory/strings/base_solver.h | |
| parent | 3c733d68aabc1c90b4f0f8a3e7a6a25f24896744 (diff) | |
(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.
Diffstat (limited to 'src/theory/strings/base_solver.h')
| -rw-r--r-- | src/theory/strings/base_solver.h | 5 |
1 files changed, 1 insertions, 4 deletions
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<Node, NodeHashFunction>; public: - BaseSolver(context::Context* c, - context::UserContext* u, - SolverState& s, - InferenceManager& im); + BaseSolver(SolverState& s, InferenceManager& im); ~BaseSolver(); //-----------------------inference steps |