path: root/libs/ezsat/ezsat.h
diff options
authorClifford Wolf <>2013-06-09 14:21:18 +0200
committerClifford Wolf <>2013-06-09 14:21:18 +0200
commit41932e8b64414da138e941c75f03077f43654c89 (patch)
treeb9678439aa0461b3403ba2ff2c63304014463d13 /libs/ezsat/ezsat.h
parentb7ba90910dfc06d89bf45b6ead9e40e9bf985fe1 (diff)
Added ezSAT api support for don't care values in models
Diffstat (limited to 'libs/ezsat/ezsat.h')
1 files changed, 3 insertions, 0 deletions
diff --git a/libs/ezsat/ezsat.h b/libs/ezsat/ezsat.h
index ea873a85..8371071e 100644
--- a/libs/ezsat/ezsat.h
+++ b/libs/ezsat/ezsat.h
@@ -98,6 +98,9 @@ public:
// If you are planning on using the solver API (and not simply create a CNF) you must use a child class
// of ezSAT that actually implements a solver backend, such as ezMiniSAT (see ezminisat.h).
+ // Note: Solvers that can output don't-care values for model variables return a twice as big modelValues
+ // vector. The first half contains the values and the second half the don't-care flags.
virtual bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions);
bool solve(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) {