mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 14:13:23 +00:00
Code Activity

imports

Browse source
This commit is contained in:
Jakob Rath 2023-11-29 16:03:47 +01:00
parent e76c6b0fdc
commit cf9b7bed0c
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/math/polysat/types.h
View file

@ -19,21 +19,21 @@ Author:
#include "util/ref_vector.h" #include "util/ref_vector.h"
#include "util/sat_literal.h" #include "util/sat_literal.h"
#include "math/dd/dd_pdd.h" #include "math/dd/dd_pdd.h"
#include "math/dd/dd_bdd.h"
#include "math/dd/dd_fdd.h" #include "math/dd/dd_fdd.h"
namespace polysat { namespace polysat {
class solver; class solver;
class constraint;
class clause; class clause;
using clause_ref = ref<clause>; using clause_ref = ref<clause>;
using clause_ref_vector = sref_vector<clause>; using clause_ref_vector = sref_vector<clause>;
typedef dd::pdd pdd; using dd::pdd;
typedef dd::bdd bdd; using dd::pdd_monomial;
typedef dd::bddv bddv; using dd::pdd_manager;
typedef dd::val_pp val_pp; using dd::val_pp;
using pvar = unsigned; using pvar = unsigned;
using pvar_vector = unsigned_vector; using pvar_vector = unsigned_vector;