From cf9b7bed0c6a84e7253ada28d2152b67c7b55ffb Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Wed, 29 Nov 2023 16:03:47 +0100 Subject: [PATCH] imports --- src/math/polysat/types.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/math/polysat/types.h b/src/math/polysat/types.h index 2dbe40499..48892d483 100644 --- a/src/math/polysat/types.h +++ b/src/math/polysat/types.h @@ -19,21 +19,21 @@ Author: #include "util/ref_vector.h" #include "util/sat_literal.h" #include "math/dd/dd_pdd.h" -#include "math/dd/dd_bdd.h" #include "math/dd/dd_fdd.h" namespace polysat { class solver; + class constraint; class clause; using clause_ref = ref; using clause_ref_vector = sref_vector; - typedef dd::pdd pdd; - typedef dd::bdd bdd; - typedef dd::bddv bddv; - typedef dd::val_pp val_pp; + using dd::pdd; + using dd::pdd_monomial; + using dd::pdd_manager; + using dd::val_pp; using pvar = unsigned; using pvar_vector = unsigned_vector;