Slight API change

Encoders may depend on underlying SAT backend, not the other way around.
whaaswijk · May 7, 2018 · dd600fd · dd600fd
1 parent 4924961
commit dd600fd
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 11 deletions.
diff --git a/include/percy/percy.hpp b/include/percy/percy.hpp
@@ -418,21 +418,30 @@ namespace percy
         The following are constructor functions that allocate new synthesizer
         objects. This is the preferred way of instantiating new synthesizers.
     ***************************************************************************/
-    template<int FI=2, typename E=knuth_encoder<FI>, typename S=sat_solver*>
+    template<
+        int FI=2, 
+        typename S=sat_solver*, 
+        typename E=knuth_encoder<FI, S>>
     auto
     new_std_synth()
     {
         return std::make_unique<std_synthesizer<FI, E, S>>();
     }
 
-    template<int FI=2, typename E=fence_encoder<FI>, typename S=sat_solver*>
+    template<
+        int FI=2, 
+        typename S=sat_solver*, 
+        typename E=fence_encoder<FI, S>>
     auto
     new_fence_synth()
     {
         return std::make_unique<fence_synthesizer<FI, E, S>>();
     }
 
-    template<int FI=2, typename E=dag_encoder<dag<FI>>, typename S=sat_solver*>
+    template<
+        int FI=2,
+        typename S=sat_solver*,
+        typename E=dag_encoder<dag<FI>,S>>
     auto
     new_dag_synth()
     {
@@ -441,8 +450,8 @@ namespace percy
 
     template<
         int FI=2, 
-        typename E=floating_dag_encoder<FI>, 
-        typename S=sat_solver*>
+        typename S=sat_solver*,
+        typename E=floating_dag_encoder<FI, S>> 
     auto
     new_floating_dag_synth()
     {

diff --git a/test/cms_equivalence.cpp b/test/cms_equivalence.cpp
@@ -16,8 +16,7 @@ void check_std_equivalence(bool full_coverage)
     synth_spec<static_truth_table<NrIn>> spec(NrIn, 1);
 
     auto synth1 = new_std_synth();
-    auto synth2 = new_std_synth<2, 
-         knuth_encoder<2, CMSat::SATSolver*>, CMSat::SATSolver*>();
+    auto synth2 = new_std_synth<2, CMSat::SATSolver*>();
 
     spec.verbosity = 0;
 

diff --git a/test/glucose_equivalence.cpp b/test/glucose_equivalence.cpp
@@ -16,8 +16,7 @@ void check_std_equivalence(bool full_coverage)
     synth_spec<static_truth_table<NrIn>> spec(NrIn, 1);
 
     auto synth1 = new_std_synth();
-    auto synth2 = new_std_synth<2, 
-         knuth_encoder<2, Glucose::Solver*>, Glucose::Solver*>();
+    auto synth2 = new_std_synth<2, Glucose::Solver*>();
 
     spec.verbosity = 0;
 

diff --git a/test/synth_equivalence.cpp b/test/synth_equivalence.cpp
@@ -190,6 +190,8 @@ int main(int argc, char **argv)
         4, 
         3>(full_coverage);
     //check_equivalence<STD,DAG, 4, 3>(full_coverage);
+    //
+    auto synth = new_std_synth<3, Glucose::MultiSolvers*>();
 
     return 0;
 }

diff --git a/test/syrup_equivalence.cpp b/test/syrup_equivalence.cpp
@@ -16,8 +16,7 @@ void check_std_equivalence(bool full_coverage)
     synth_spec<static_truth_table<NrIn>> spec(NrIn, 1);
 
     auto synth1 = new_std_synth();
-    auto synth2 = new_std_synth<2, 
-         knuth_encoder<2, Glucose::MultiSolvers*>, Glucose::MultiSolvers*>();
+    auto synth2 = new_std_synth<2, Glucose::MultiSolvers*>();
 
     spec.verbosity = 0;