From 26b272528a1fce1dec75485a29bed59cbdb6d19f Mon Sep 17 00:00:00 2001 From: tmeissner Date: Fri, 5 Aug 2022 14:51:30 +0200 Subject: [PATCH] Add patch file to get ExtAvy compiled --- packages/avy.patch | 36 ++++++++++++++++++++++++++++++++++++ 1 file changed, 36 insertions(+) create mode 100644 packages/avy.patch diff --git a/packages/avy.patch b/packages/avy.patch new file mode 100644 index 0000000..937a975 --- /dev/null +++ b/packages/avy.patch @@ -0,0 +1,36 @@ +diff --git a/src/ItpGlucose.h b/src/ItpGlucose.h +index 657253d..66a0cd4 100644 +--- a/src/ItpGlucose.h ++++ b/src/ItpGlucose.h +@@ -126,7 +126,7 @@ namespace avy + ::Glucose::Solver* get () { return m_pSat; } + + /// true if the context is decided +- bool isSolved () { return m_Trivial || m_State || !m_State; } ++ bool isSolved () { return bool{m_Trivial || m_State || !m_State}; } + + int core (int **out) + { +@@ -182,7 +182,8 @@ namespace avy + bool getVarVal(int v) + { + ::Glucose::Var x = v; +- return tobool (m_pSat->modelValue(x)); ++ boost::logic::tribool y = tobool (m_pSat->modelValue(x)); ++ return bool{y}; + } + }; + +diff --git a/src/ItpMinisat.h b/src/ItpMinisat.h +index d145d7c..7514f31 100644 +--- a/src/ItpMinisat.h ++++ b/src/ItpMinisat.h +@@ -124,7 +124,7 @@ namespace avy + ::Minisat::Solver* get () { return m_pSat.get (); } + + /// true if the context is decided +- bool isSolved () { return m_Trivial || m_State || !m_State; } ++ bool isSolved () { return bool{m_Trivial || m_State || !m_State}; } + + int core (int **out) + { \ No newline at end of file