yosys-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
demo_bit.cc File Reference
#include "ezminisat.h"
#include <stdio.h>
+ Include dependency graph for demo_bit.cc:

Go to the source code of this file.

Functions

void print_results (bool satisfiable, const std::vector< bool > &modelValues)
 
int main ()
 

Function Documentation

int main ( )

Definition at line 35 of file demo_bit.cc.

36 {
37  ezMiniSAT sat;
38 
39  // 3 input AOI-Gate
40  // 'pos_active' encodes the condition under which the pullup path of the gate is active
41  // 'neg_active' encodes the condition under which the pulldown path of the gate is active
42  // 'impossible' encodes the condition that both or none of the above paths is active
43  int pos_active = sat.AND(sat.NOT("A"), sat.OR(sat.NOT("B"), sat.NOT("C")));
44  int neg_active = sat.OR("A", sat.AND("B", "C"));
45  int impossible = sat.IFF(pos_active, neg_active);
46 
47  std::vector<int> modelVars;
48  std::vector<bool> modelValues;
49  bool satisfiable;
50 
51  modelVars.push_back(sat.VAR("A"));
52  modelVars.push_back(sat.VAR("B"));
53  modelVars.push_back(sat.VAR("C"));
54 
55  printf("\n");
56 
57  printf("pos_active: %s\n", sat.to_string(pos_active).c_str());
58  satisfiable = sat.solve(modelVars, modelValues, pos_active);
59  print_results(satisfiable, modelValues);
60 
61  printf("neg_active: %s\n", sat.to_string(neg_active).c_str());
62  satisfiable = sat.solve(modelVars, modelValues, neg_active);
63  print_results(satisfiable, modelValues);
64 
65  printf("impossible: %s\n", sat.to_string(impossible).c_str());
66  satisfiable = sat.solve(modelVars, modelValues, impossible);
67  print_results(satisfiable, modelValues);
68 
69  return 0;
70 }
int NOT(_V a)
Definition: ezsat.h:197
void print_results(bool satisfiable, const std::vector< bool > &modelValues)
Definition: demo_bit.cc:23
int AND(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:201
std::string to_string(int id) const
Definition: ezsat.cc:237
bool solve(const std::vector< int > &modelExpressions, std::vector< bool > &modelValues, const std::vector< int > &assumptions)
Definition: ezsat.h:122
int VAR(_V a)
Definition: ezsat.h:193
int OR(_V a=0, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:205
int IFF(_V a, _V b=0, _V c=0, _V d=0, _V e=0, _V f=0)
Definition: ezsat.h:213

+ Here is the call graph for this function:

void print_results ( bool  satisfiable,
const std::vector< bool > &  modelValues 
)

Definition at line 23 of file demo_bit.cc.

24 {
25  if (!satisfiable) {
26  printf("not satisfiable.\n\n");
27  } else {
28  printf("satisfiable:");
29  for (auto val : modelValues)
30  printf(" %d", val ? 1 : 0);
31  printf("\n\n");
32  }
33 }

+ Here is the caller graph for this function: