Gymbo

sat.h
Go to the documentation of this file.
1
7 #pragma once
8 #include <memory>
9
10 #include "type.h"
11
12 namespace gymbosat {
13
17 typedef enum { VAR, AND, OR, NOT, CONST } OpCode;
18
22 typedef enum { Positive, Negative, Mixed } Polarity;
23
28 class Expr : public std::enable_shared_from_this<Expr> {
29 public:
30 OpCode opcode;
31 std::string name;
36 virtual ~Expr() {}
37
42 virtual std::string to_string() = 0;
43
48 virtual bool evaluate() = 0;
49
55 virtual bool unConst() = 0;
56
62 virtual std::pair<bool, std::string> freeVar() = 0;
63
71 virtual std::shared_ptr<Expr> guessVar(std::string var, bool val) = 0;
72
77 virtual std::shared_ptr<Expr> simplify() = 0;
78
83 virtual std::shared_ptr<Expr> fixNegations() = 0;
84
90 virtual std::shared_ptr<Expr> distribute() = 0;
91
96 virtual std::shared_ptr<Expr> getLeft() = 0;
97
102 virtual std::shared_ptr<Expr> getRight() = 0;
103
108 virtual std::unordered_set<std::string> literals() = 0;
109
116 virtual std::unordered_map<std::string, Polarity> literalPolarity(
117 std::string var) = 0;
118
123 virtual std::pair<std::string, bool> unitClause() = 0;
124
129 virtual std::vector<std::shared_ptr<Expr>> clauses() = 0;
130 };
131
136 class Var : public Expr {
137 std::string name;
138
139 public:
140 Var(std::string name) : name(name) { opcode = OpCode::VAR; }
141 std::string to_string() override { return name; }
142 std::pair<bool, std::string> freeVar() override { return {true, name}; }
143 std::shared_ptr<Expr> simplify() override { return shared_from_this(); }
144 bool evaluate() override { return false; }
145 bool unConst() override { return false; }
146 std::shared_ptr<Expr> guessVar(std::string var, bool val) override;
147
148 std::shared_ptr<Expr> fixNegations() override { return shared_from_this(); }
149 std::shared_ptr<Expr> distribute() override { return shared_from_this(); }
150 std::shared_ptr<Expr> getLeft() override { return std::shared_ptr<Expr>(); }
151 std::shared_ptr<Expr> getRight() override {
152 return std::shared_ptr<Expr>();
153 }
154
155 std::unordered_set<std::string> literals() override { return {name}; }
156 std::unordered_map<std::string, Polarity> literalPolarity(
157 std::string var) override {
158 std::unordered_map<std::string, Polarity> polarity_map;
159 if (name == var) {
160 polarity_map[var] = Polarity::Positive;
161 }
162 return polarity_map;
163 }
164
165 std::pair<std::string, bool> unitClause() override { return {name, true}; }
166 std::vector<std::shared_ptr<Expr>> clauses() override {
167 return {shared_from_this()};
168 }
169 };
170
175 class And : public Expr {
176 public:
182 And(std::shared_ptr<Expr> left, std::shared_ptr<Expr> right)
183 : left(left), right(right) {
184 opcode = OpCode::AND;
185 name = "And";
186 }
187
188 std::string to_string() override {
189 return "(" + left->to_string() + " && " + right->to_string() + ")";
190 }
191
192 bool evaluate() override { return left->evaluate() && right->evaluate(); }
193
194 std::pair<bool, std::string> freeVar() override {
195 std::pair<bool, std::string> leftVar = left->freeVar();
196 if (leftVar.first) {
197 return leftVar;
198 }
199 return right->freeVar();
200 }
201
202 bool unConst() override { return false; }
203
204 std::shared_ptr<Expr> fixNegations() override {
205 return std::make_shared<And>(left->fixNegations(),
206 right->fixNegations());
207 }
208
209 std::shared_ptr<Expr> distribute() override {
210 return std::make_shared<And>(left->distribute(), right->distribute());
211 }
212
213 std::shared_ptr<Expr> getLeft() override { return left; }
214 std::shared_ptr<Expr> getRight() override { return right; }
215
216 std::unordered_set<std::string> literals() override {
217 auto leftLiterals = left->literals();
218 auto rightLiterals = right->literals();
219 leftLiterals.insert(rightLiterals.begin(), rightLiterals.end());
220 return leftLiterals;
221 }
222
223 std::unordered_map<std::string, Polarity> literalPolarity(
224 std::string var) override {
225 std::unordered_map<std::string, Polarity> polarity_map;
226
227 std::unordered_map<std::string, Polarity> left_polarity =
228 left->literalPolarity(var);
229 std::unordered_map<std::string, Polarity> right_polarity =
230 right->literalPolarity(var);
231
232 for (auto &pair : left_polarity) {
233 polarity_map[pair.first] = pair.second;
234 }
235
236 for (auto &pair : right_polarity) {
237 if (polarity_map.find(pair.first) == polarity_map.end()) {
238 polarity_map[pair.first] = pair.second;
239 } else if (polarity_map[pair.first] != pair.second) {
240 polarity_map[pair.first] = Polarity::Mixed;
241 }
242 }
243
244 return polarity_map;
245 }
246
247 std::pair<std::string, bool> unitClause() override { return {"", false}; }
248
249 std::vector<std::shared_ptr<Expr>> clauses() override {
250 auto left_clause = left->clauses();
251 auto right_clause = right->clauses();
252 left_clause.insert(left_clause.end(), right_clause.begin(),
253 right_clause.end());
254 return left_clause;
255 }
256
257 std::shared_ptr<Expr> guessVar(std::string var, bool val) override;
258 std::shared_ptr<Expr> simplify() override;
259
260 private:
261 std::shared_ptr<Expr> left, right;
262 };
263
268 class Or : public Expr {
269 public:
275 Or(std::shared_ptr<Expr> left, std::shared_ptr<Expr> right)
276 : left(left), right(right) {
277 opcode = OpCode::OR;
278 name = "Or";
279 }
280
281 std::string to_string() override {
282 return "(" + left->to_string() + " || " + right->to_string() + ")";
283 }
284
285 bool evaluate() override { return left->evaluate() || right->evaluate(); }
286
287 std::pair<bool, std::string> freeVar() override {
288 std::pair<bool, std::string> leftVar = left->freeVar();
289 if (leftVar.first) {
290 return leftVar;
291 }
292 return right->freeVar();
293 }
294
295 bool unConst() override { return false; }
296
297 std::shared_ptr<Expr> fixNegations() override {
298 return std::make_shared<Or>(left->fixNegations(),
299 right->fixNegations());
300 }
301
302 std::shared_ptr<Expr> distribute() override {
303 if (right->opcode == AND) {
304 return std::make_shared<And>(
305 std::make_shared<Or>(left->distribute(),
306 right->getLeft()->distribute()),
307 std::make_shared<Or>(left->distribute(),
308 right->getRight()->distribute()));
309 } else if (left->opcode == AND) {
310 return std::make_shared<And>(
311 std::make_shared<Or>(right->distribute(),
312 left->getLeft()->distribute()),
313 std::make_shared<Or>(right->distribute(),
314 left->getRight()->distribute()));
315 }
316 return std::make_shared<Or>(left->distribute(), right->distribute());
317 }
318
319 std::shared_ptr<Expr> getLeft() override { return left; }
320
321 std::shared_ptr<Expr> getRight() override { return right; }
322
323 std::unordered_set<std::string> literals() override {
324 auto leftLiterals = left->literals();
325 auto rightLiterals = right->literals();
326 leftLiterals.insert(rightLiterals.begin(), rightLiterals.end());
327 return leftLiterals;
328 }
329
330 std::unordered_map<std::string, Polarity> literalPolarity(
331 std::string var) override {
332 std::unordered_map<std::string, Polarity> polarity_map;
333
334 std::unordered_map<std::string, Polarity> left_polarity =
335 left->literalPolarity(var);
336 std::unordered_map<std::string, Polarity> right_polarity =
337 right->literalPolarity(var);
338
339 for (auto &pair : left_polarity) {
340 polarity_map[pair.first] = pair.second;
341 }
342
343 for (auto &pair : right_polarity) {
344 if (polarity_map.find(pair.first) == polarity_map.end()) {
345 polarity_map[pair.first] = pair.second;
346 } else if (polarity_map[pair.first] != pair.second) {
347 polarity_map[pair.first] = Polarity::Mixed;
348 }
349 }
350
351 return polarity_map;
352 }
353
354 std::pair<std::string, bool> unitClause() override { return {"", false}; }
355
356 std::vector<std::shared_ptr<Expr>> clauses() override {
357 return {shared_from_this()};
358 }
359
360 std::shared_ptr<Expr> guessVar(std::string var, bool val) override;
361 std::shared_ptr<Expr> simplify() override;
362
363 private:
364 std::shared_ptr<Expr> left, right;
365 };
366
371 class Not : public Expr {
372 public:
377 Not(std::shared_ptr<Expr> expr) : expr(expr) {
378 opcode = OpCode::NOT;
379 name = "Not";
380 }
381
382 std::string to_string() override {
383 return "(!(" + expr->to_string() + "))";
384 }
385
386 bool evaluate() override { return !expr->evaluate(); }
387
388 std::pair<bool, std::string> freeVar() override { return expr->freeVar(); }
389
390 std::shared_ptr<Expr> distribute() override {
391 return std::make_shared<Not>(expr->distribute());
392 }
393
394 bool unConst() override { return false; }
395
396 std::shared_ptr<Expr> getLeft() override { return std::shared_ptr<Expr>(); }
397 std::shared_ptr<Expr> getRight() override {
398 return std::shared_ptr<Expr>();
399 }
400
401 std::unordered_set<std::string> literals() override {
402 return expr->literals();
403 }
404
405 std::unordered_map<std::string, Polarity> literalPolarity(
406 std::string var) override {
407 std::unordered_map<std::string, Polarity> polarity_map;
408 if (expr->opcode == OpCode::VAR && expr->name == var) {
409 polarity_map[expr->name] = Polarity::Negative;
410 }
411 return polarity_map;
412 }
413
414 std::pair<std::string, bool> unitClause() override {
415 if (expr->opcode == OpCode::VAR) {
416 return {expr->name, false};
417 }
418 return {"", false};
419 }
420
421 std::vector<std::shared_ptr<Expr>> clauses() override {
422 return {shared_from_this()};
423 }
424
425 std::shared_ptr<Expr> fixNegations() override;
426 std::shared_ptr<Expr> guessVar(std::string var, bool val) override;
427 std::shared_ptr<Expr> simplify() override;
428
429 private:
430 std::shared_ptr<Expr> expr;
431 };
432
437 class Const : public Expr {
438 public:
443 Const(bool value) : value(value) {
444 opcode = OpCode::CONST;
445 std::string name = "Const";
446 }
447
448 std::string to_string() override { return value ? "True" : "False"; }
449
450 bool evaluate() override { return value; }
451
452 std::pair<bool, std::string> freeVar() override { return {false, ""}; }
453
454 bool unConst() override { return value; }
455
456 std::shared_ptr<Expr> simplify() override { return shared_from_this(); };
457 std::shared_ptr<Expr> fixNegations() override { return shared_from_this(); }
458 std::shared_ptr<Expr> distribute() override { return shared_from_this(); }
459 std::shared_ptr<Expr> getLeft() override { return std::shared_ptr<Expr>(); }
460 std::shared_ptr<Expr> getRight() override {
461 return std::shared_ptr<Expr>();
462 }
463
464 std::unordered_set<std::string> literals() override { return {}; }
465
466 std::shared_ptr<Expr> guessVar(std::string var, bool val) override;
467
468 std::unordered_map<std::string, Polarity> literalPolarity(
469 std::string var) override {
470 std::unordered_map<std::string, Polarity> polarity_map;
471 return polarity_map;
472 }
473
474 std::pair<std::string, bool> unitClause() override { return {"", false}; }
475
476 std::vector<std::shared_ptr<Expr>> clauses() override {
477 return {shared_from_this()};
478 }
479
480 private:
481 bool value;
482 };
483
484 inline std::shared_ptr<Expr> Var::guessVar(std::string var, bool val) {
485 if (name == var) {
486 return std::make_shared<Const>(val);
487 } else {
488 return std::make_shared<Var>(name);
489 }
490 }
491
492 inline std::shared_ptr<Expr> And::guessVar(std::string var, bool val) {
493 return std::make_shared<And>(left->guessVar(var, val),
494 right->guessVar(var, val));
495 }
496
497 inline std::shared_ptr<Expr> Or::guessVar(std::string var, bool val) {
498 return std::make_shared<Or>(left->guessVar(var, val),
499 right->guessVar(var, val));
500 }
501
502 inline std::shared_ptr<Expr> Not::guessVar(std::string var, bool val) {
503 return std::make_shared<Not>(expr->guessVar(var, val));
504 }
505
506 inline std::shared_ptr<Expr> Const::guessVar(std::string var, bool val) {
507 return std::make_shared<Const>(value);
508 }
509
510 inline std::shared_ptr<Expr> And::simplify() {
511 auto simplifiedLeft = left->simplify();
512 auto simplifiedRight = right->simplify();
513
514 if (simplifiedLeft->to_string() == "True" &&
515 simplifiedRight->to_string() == "True") {
516 return std::make_shared<Const>(true);
517 } else if (simplifiedLeft->to_string() == "False" ||
518 simplifiedRight->to_string() == "False") {
519 return std::make_shared<Const>(false);
520 } else if (simplifiedLeft->to_string() == "True") {
521 return simplifiedRight;
522 } else if (simplifiedRight->to_string() == "True") {
523 return simplifiedLeft;
524 } else {
525 return std::make_shared<And>(simplifiedLeft, simplifiedRight);
526 }
527 }
528
529 inline std::shared_ptr<Expr> Or::simplify() {
530 auto simplifiedLeft = left->simplify();
531 auto simplifiedRight = right->simplify();
532
533 if (simplifiedLeft->to_string() == "False" &&
534 simplifiedRight->to_string() == "False") {
535 return std::make_shared<Const>(false);
536 } else if (simplifiedLeft->to_string() == "True" ||
537 simplifiedRight->to_string() == "True") {
538 return std::make_shared<Const>(true);
539 } else if (simplifiedLeft->to_string() == "False") {
540 return simplifiedRight;
541 } else if (simplifiedRight->to_string() == "False") {
542 return simplifiedLeft;
543 } else {
544 return std::make_shared<Or>(simplifiedLeft, simplifiedRight);
545 }
546 }
547
548 inline std::shared_ptr<Expr> Not::simplify() {
549 auto simplifiedExpr = expr->simplify();
550
551 if (simplifiedExpr->to_string() == "True") {
552 return std::make_shared<Const>(false);
553 } else if (simplifiedExpr->to_string() == "False") {
554 return std::make_shared<Const>(true);
555 } else {
556 return std::make_shared<Not>(simplifiedExpr);
557 }
558 }
559
560 inline std::shared_ptr<Expr> Not::fixNegations() {
561 if (expr->to_string() == "True") {
562 // !True = False
563 return std::make_shared<Const>(false);
564 } else if (expr->to_string() == "False") {
565 // !False = True
566 return std::make_shared<Const>(true);
567 } else if (expr->opcode == OpCode::VAR) {
568 return std::make_shared<Not>(expr->fixNegations());
569 } else if (expr->opcode == OpCode::NOT) {
570 // !!Var = Var
571 return expr->fixNegations();
572 } else if (expr->opcode == OpCode::AND) {
573 return std::make_shared<Or>(
574 std::make_shared<Not>(expr->getLeft())->fixNegations(),
575 std::make_shared<Not>(expr->getRight())->fixNegations());
576 } else if (expr->opcode == OpCode::OR) {
577 return std::make_shared<And>(
578 std::make_shared<Not>(expr->getLeft())->fixNegations(),
579 std::make_shared<Not>(expr->getRight())->fixNegations());
580 }
581 return std::make_shared<Not>(expr->fixNegations());
582 }
583
589 inline std::shared_ptr<Expr> cnf(std::shared_ptr<Expr> expr) {
590 std::shared_ptr<Expr> new_expr = expr->fixNegations()->distribute();
591 if (expr->to_string() == new_expr->to_string()) {
592 return expr;
593 } else {
594 return cnf(new_expr);
595 }
596 }
597
604 inline std::shared_ptr<Expr> literalElimination(
605 std::shared_ptr<Expr> expr,
606 std::unordered_map<std::string, bool> &assignments_map) {
607 std::unordered_set<std::string> literal_set = expr->literals();
608 std::unordered_map<std::string, Polarity> polarity_map;
609 std::vector<std::pair<std::string, bool>> assignments;
610
611 for (std::string var : literal_set) {
612 polarity_map = expr->literalPolarity(var);
613 if (polarity_map.find(var) != polarity_map.end()) {
614 if (polarity_map[var] == Polarity::Positive) {
615 assignments.push_back(std::make_pair(var, true));
616 } else if (polarity_map[var] == Polarity::Negative) {
617 assignments.push_back(std::make_pair(var, false));
618 }
619 }
620 }
621
622 for (auto &assignment : assignments) {
623 std::string var = assignment.first;
624 bool value = assignment.second;
625 expr = expr->guessVar(var, value);
626 if (assignments_map.find(var) == assignments_map.end()) {
627 assignments_map.emplace(var, value);
628 } else {
629 assignments_map[var] = value;
630 }
631 }
632
633 return expr;
634 }
635
641 inline std::vector<std::pair<std::string, bool>> allUnitClauses(
642 std::shared_ptr<Expr> expr) {
643 std::vector<std::pair<std::string, bool>> result;
644 std::vector<std::shared_ptr<Expr>> exprs = expr->clauses();
645 for (auto e : exprs) {
646 auto uc = e->unitClause();
647 if (uc.first != "") {
648 result.emplace_back(uc);
649 }
650 }
651 return result;
652 }
653
660 inline std::shared_ptr<Expr> unitPropagation(
661 std::shared_ptr<Expr> expr,
662 std::unordered_map<std::string, bool> &assignments_map) {
663 std::vector<std::pair<std::string, bool>> assignments =
664 allUnitClauses(expr);
665 for (auto &assignment : assignments) {
666 std::string var = assignment.first;
667 bool value = assignment.second;
668 expr = expr->guessVar(var, value);
669 if (assignments_map.find(var) == assignments_map.end()) {
670 assignments_map.emplace(var, value);
671 } else {
672 assignments_map[var] = value;
673 }
674 }
675
676 return expr;
677 }
678
685 inline bool satisfiableDPLL(
686 std::shared_ptr<Expr> expr,
687 std::unordered_map<std::string, bool> &assignments_map) {
688 // std::shared_ptr<Expr> expr2 = literalElimination(
689 // cnf(unitPropagation(expr, assignments_map)), assignments_map);
690 std::shared_ptr<Expr> expr2 = cnf(unitPropagation(expr, assignments_map));
691
692 std::pair<bool, std::string> freevar = expr2->freeVar();
693 if (!freevar.first) {
694 return expr2->simplify()->unConst();
695 } else {
696 std::string var = freevar.second;
697
698 auto trueGuess = expr2->guessVar(var, true)->simplify();
699 std::unordered_map<std::string, bool> true_assignments_map =
700 assignments_map;
701 if (true_assignments_map.find(var) == true_assignments_map.end()) {
702 true_assignments_map.emplace(var, true);
703 } else {
704 true_assignments_map[var] = true;
705 }
706 if (satisfiableDPLL(trueGuess, true_assignments_map)) {
707 assignments_map = true_assignments_map;
708 return true;
709 }
710
711 auto falseGuess = expr2->guessVar(var, false)->simplify();
712 std::unordered_map<std::string, bool> false_assignments_map =
713 assignments_map;
714 if (false_assignments_map.find(var) == false_assignments_map.end()) {
715 false_assignments_map.emplace(var, false);
716 } else {
717 false_assignments_map[var] = false;
718 }
719 if (satisfiableDPLL(falseGuess, false_assignments_map)) {
720 assignments_map = false_assignments_map;
721 return true;
722 }
723
724 return false;
725 }
726 }
727
735 inline std::shared_ptr<Expr> sym2expr(
736 gymbo::Sym *sym,
737 std::unordered_map<std::string, gymbo::Sym *> &unique_sym_map) {
738 switch (sym->symtype) {
739 case (gymbo::SymType::SAnd): {
740 return std::make_shared<And>(sym2expr(sym->left, unique_sym_map),
741 sym2expr(sym->right, unique_sym_map));
742 }
743 case (gymbo::SymType::SNot): {
744 return std::make_shared<Not>(sym2expr(sym->left, unique_sym_map));
745 }
746 case (gymbo::SymType::SOr): {
747 return std::make_shared<Or>(sym2expr(sym->left, unique_sym_map),
748 sym2expr(sym->right, unique_sym_map));
749 }
750 default: {
751 unique_sym_map.insert({sym->toString(true), sym});
752 return std::make_shared<Var>(sym->toString(true));
753 }
754 }
755 }
756
765 inline std::shared_ptr<Expr> pathconstraints2expr(
766 std::vector<gymbo::Sym> &constraints,
767 std::unordered_map<std::string, gymbo::Sym *> &unique_sym_map) {
768 if (constraints.size() == 0) {
769 return std::make_shared<Const>(true);
770 } else {
771 std::shared_ptr<Expr> res = sym2expr(&constraints[0], unique_sym_map);
772 for (int i = 1; i < constraints.size(); i++) {
773 res = std::make_shared<And>(
774 res, sym2expr(&constraints[i], unique_sym_map));
775 }
776 return res;
777 }
778 }
779 } // namespace gymbosat
gymbosat::And
Class representing the logical AND operation.
Definition: sat.h:175
gymbosat::And::freeVar
std::pair< bool, std::string > freeVar() override
Identify and return free variables in the logical expression.
Definition: sat.h:194
gymbosat::And::getRight
std::shared_ptr< Expr > getRight() override
Get the right child expression.
Definition: sat.h:214
gymbosat::And::evaluate
bool evaluate() override
Evaluate the logical expression.
Definition: sat.h:192
gymbosat::And::left
std::shared_ptr< Expr > left
Definition: sat.h:261
gymbosat::And::clauses
std::vector< std::shared_ptr< Expr > > clauses() override
Get a vector of clauses present in the logical expression.
Definition: sat.h:249
gymbosat::And::getLeft
std::shared_ptr< Expr > getLeft() override
Get the left child expression.
Definition: sat.h:213
gymbosat::And::literals
std::unordered_set< std::string > literals() override
Get the literals present in the logical expression.
Definition: sat.h:216
gymbosat::And::simplify
std::shared_ptr< Expr > simplify() override
Simplify the logical expression.
Definition: sat.h:510
gymbosat::And::unConst
bool unConst() override
Check if the logical expression can be simplified by removing constants.
Definition: sat.h:202
gymbosat::And::right
std::shared_ptr< Expr > right
Definition: sat.h:261
gymbosat::And::literalPolarity
std::unordered_map< std::string, Polarity > literalPolarity(std::string var) override
Get the polarities of literals with respect to a specific variable.
Definition: sat.h:223
gymbosat::And::distribute
std::shared_ptr< Expr > distribute() override
Distribute operations in the logical expression.
Definition: sat.h:209
gymbosat::And::And
And(std::shared_ptr< Expr > left, std::shared_ptr< Expr > right)
Constructor for the And class.
Definition: sat.h:182
gymbosat::And::guessVar
std::shared_ptr< Expr > guessVar(std::string var, bool val) override
Make a guess for a variable's value and return the resulting expression.
Definition: sat.h:492
gymbosat::And::fixNegations
std::shared_ptr< Expr > fixNegations() override
Fix negations in the logical expression.
Definition: sat.h:204
gymbosat::And::to_string
std::string to_string() override
Convert the logical expression to a string representation.
Definition: sat.h:188
gymbosat::And::unitClause
std::pair< std::string, bool > unitClause() override
Get a unit clause from the logical expression.
Definition: sat.h:247
gymbosat::Const
Class representing a boolean constant in a logical expression.
Definition: sat.h:437
gymbosat::Const::simplify
std::shared_ptr< Expr > simplify() override
Simplify the logical expression.
Definition: sat.h:456
gymbosat::Const::guessVar
std::shared_ptr< Expr > guessVar(std::string var, bool val) override
Make a guess for a variable's value and return the resulting expression.
Definition: sat.h:506
gymbosat::Const::getRight
std::shared_ptr< Expr > getRight() override
Get the right child expression.
Definition: sat.h:460
gymbosat::Const::unitClause
std::pair< std::string, bool > unitClause() override
Get a unit clause from the logical expression.
Definition: sat.h:474
gymbosat::Const::unConst
bool unConst() override
Check if the logical expression can be simplified by removing constants.
Definition: sat.h:454
gymbosat::Const::fixNegations
std::shared_ptr< Expr > fixNegations() override
Fix negations in the logical expression.
Definition: sat.h:457
gymbosat::Const::value
bool value
Definition: sat.h:481
gymbosat::Const::clauses
std::vector< std::shared_ptr< Expr > > clauses() override
Get a vector of clauses present in the logical expression.
Definition: sat.h:476
gymbosat::Const::freeVar
std::pair< bool, std::string > freeVar() override
Identify and return free variables in the logical expression.
Definition: sat.h:452
gymbosat::Const::Const
Const(bool value)
Constructor for the Const class.
Definition: sat.h:443
gymbosat::Const::distribute
std::shared_ptr< Expr > distribute() override
Distribute operations in the logical expression.
Definition: sat.h:458
gymbosat::Const::to_string
std::string to_string() override
Convert the logical expression to a string representation.
Definition: sat.h:448
gymbosat::Const::literals
std::unordered_set< std::string > literals() override
Get the literals present in the logical expression.
Definition: sat.h:464
gymbosat::Const::evaluate
bool evaluate() override
Evaluate the logical expression.
Definition: sat.h:450
gymbosat::Const::getLeft
std::shared_ptr< Expr > getLeft() override
Get the left child expression.
Definition: sat.h:459
gymbosat::Const::literalPolarity
std::unordered_map< std::string, Polarity > literalPolarity(std::string var) override
Get the polarities of literals with respect to a specific variable.
Definition: sat.h:468
gymbosat::Expr
Base class for representing logical expressions.
Definition: sat.h:28
gymbosat::Expr::getLeft
virtual std::shared_ptr< Expr > getLeft()=0
Get the left child expression.
gymbosat::Expr::fixNegations
virtual std::shared_ptr< Expr > fixNegations()=0
Fix negations in the logical expression.
gymbosat::Expr::clauses
virtual std::vector< std::shared_ptr< Expr > > clauses()=0
Get a vector of clauses present in the logical expression.
gymbosat::Expr::unConst
virtual bool unConst()=0
Check if the logical expression can be simplified by removing constants.
gymbosat::Expr::simplify
virtual std::shared_ptr< Expr > simplify()=0
Simplify the logical expression.
gymbosat::Expr::guessVar
virtual std::shared_ptr< Expr > guessVar(std::string var, bool val)=0
Make a guess for a variable's value and return the resulting expression.
gymbosat::Expr::distribute
virtual std::shared_ptr< Expr > distribute()=0
Distribute operations in the logical expression.
gymbosat::Expr::unitClause
virtual std::pair< std::string, bool > unitClause()=0
Get a unit clause from the logical expression.
gymbosat::Expr::to_string
virtual std::string to_string()=0
Convert the logical expression to a string representation.
gymbosat::Expr::freeVar
virtual std::pair< bool, std::string > freeVar()=0
Identify and return free variables in the logical expression.
gymbosat::Expr::literals
virtual std::unordered_set< std::string > literals()=0
Get the literals present in the logical expression.
gymbosat::Expr::opcode
OpCode opcode
Definition: sat.h:30
gymbosat::Expr::getRight
virtual std::shared_ptr< Expr > getRight()=0
Get the right child expression.
gymbosat::Expr::evaluate
virtual bool evaluate()=0
Evaluate the logical expression.
gymbosat::Expr::name
std::string name
Definition: sat.h:31
gymbosat::Expr::literalPolarity
virtual std::unordered_map< std::string, Polarity > literalPolarity(std::string var)=0
Get the polarities of literals with respect to a specific variable.
gymbosat::Expr::~Expr
virtual ~Expr()
Destructor for the Expr class.
Definition: sat.h:36
gymbosat::Not
Class representing the logical NOT operation.
Definition: sat.h:371
gymbosat::Not::freeVar
std::pair< bool, std::string > freeVar() override
Identify and return free variables in the logical expression.
Definition: sat.h:388
gymbosat::Not::Not
Not(std::shared_ptr< Expr > expr)
Constructor for the Not class.
Definition: sat.h:377
gymbosat::Not::getRight
std::shared_ptr< Expr > getRight() override
Get the right child expression.
Definition: sat.h:397
gymbosat::Not::unitClause
std::pair< std::string, bool > unitClause() override
Get a unit clause from the logical expression.
Definition: sat.h:414
gymbosat::Not::to_string
std::string to_string() override
Convert the logical expression to a string representation.
Definition: sat.h:382
gymbosat::Not::guessVar
std::shared_ptr< Expr > guessVar(std::string var, bool val) override
Make a guess for a variable's value and return the resulting expression.
Definition: sat.h:502
gymbosat::Not::distribute
std::shared_ptr< Expr > distribute() override
Distribute operations in the logical expression.
Definition: sat.h:390
gymbosat::Not::simplify
std::shared_ptr< Expr > simplify() override
Simplify the logical expression.
Definition: sat.h:548
gymbosat::Not::unConst
bool unConst() override
Check if the logical expression can be simplified by removing constants.
Definition: sat.h:394
gymbosat::Not::literals
std::unordered_set< std::string > literals() override
Get the literals present in the logical expression.
Definition: sat.h:401
gymbosat::Not::literalPolarity
std::unordered_map< std::string, Polarity > literalPolarity(std::string var) override
Get the polarities of literals with respect to a specific variable.
Definition: sat.h:405
gymbosat::Not::getLeft
std::shared_ptr< Expr > getLeft() override
Get the left child expression.
Definition: sat.h:396
gymbosat::Not::expr
std::shared_ptr< Expr > expr
Definition: sat.h:430
gymbosat::Not::clauses
std::vector< std::shared_ptr< Expr > > clauses() override
Get a vector of clauses present in the logical expression.
Definition: sat.h:421
gymbosat::Not::fixNegations
std::shared_ptr< Expr > fixNegations() override
Fix negations in the logical expression.
Definition: sat.h:560
gymbosat::Not::evaluate
bool evaluate() override
Evaluate the logical expression.
Definition: sat.h:386
gymbosat::Or
Class representing the logical OR operation.
Definition: sat.h:268
gymbosat::Or::distribute
std::shared_ptr< Expr > distribute() override
Distribute operations in the logical expression.
Definition: sat.h:302
gymbosat::Or::left
std::shared_ptr< Expr > left
Definition: sat.h:364
gymbosat::Or::unitClause
std::pair< std::string, bool > unitClause() override
Get a unit clause from the logical expression.
Definition: sat.h:354
gymbosat::Or::to_string
std::string to_string() override
Convert the logical expression to a string representation.
Definition: sat.h:281
gymbosat::Or::right
std::shared_ptr< Expr > right
Definition: sat.h:364
gymbosat::Or::clauses
std::vector< std::shared_ptr< Expr > > clauses() override
Get a vector of clauses present in the logical expression.
Definition: sat.h:356
gymbosat::Or::simplify
std::shared_ptr< Expr > simplify() override
Simplify the logical expression.
Definition: sat.h:529
gymbosat::Or::freeVar
std::pair< bool, std::string > freeVar() override
Identify and return free variables in the logical expression.
Definition: sat.h:287
gymbosat::Or::literalPolarity
std::unordered_map< std::string, Polarity > literalPolarity(std::string var) override
Get the polarities of literals with respect to a specific variable.
Definition: sat.h:330
gymbosat::Or::guessVar
std::shared_ptr< Expr > guessVar(std::string var, bool val) override
Make a guess for a variable's value and return the resulting expression.
Definition: sat.h:497
gymbosat::Or::unConst
bool unConst() override
Check if the logical expression can be simplified by removing constants.
Definition: sat.h:295
gymbosat::Or::Or
Or(std::shared_ptr< Expr > left, std::shared_ptr< Expr > right)
Constructor for the Or class.
Definition: sat.h:275
gymbosat::Or::evaluate
bool evaluate() override
Evaluate the logical expression.
Definition: sat.h:285
gymbosat::Or::fixNegations
std::shared_ptr< Expr > fixNegations() override
Fix negations in the logical expression.
Definition: sat.h:297
gymbosat::Or::getRight
std::shared_ptr< Expr > getRight() override
Get the right child expression.
Definition: sat.h:321
gymbosat::Or::getLeft
std::shared_ptr< Expr > getLeft() override
Get the left child expression.
Definition: sat.h:319
gymbosat::Or::literals
std::unordered_set< std::string > literals() override
Get the literals present in the logical expression.
Definition: sat.h:323
gymbosat::Var
Class representing a variable in a logical expression.
Definition: sat.h:136
gymbosat::Var::clauses
std::vector< std::shared_ptr< Expr > > clauses() override
Get a vector of clauses present in the logical expression.
Definition: sat.h:166
gymbosat::Var::Var
Var(std::string name)
Definition: sat.h:140
gymbosat::Var::guessVar
std::shared_ptr< Expr > guessVar(std::string var, bool val) override
Make a guess for a variable's value and return the resulting expression.
Definition: sat.h:484
gymbosat::Var::name
std::string name
Definition: sat.h:137
gymbosat::Var::literalPolarity
std::unordered_map< std::string, Polarity > literalPolarity(std::string var) override
Get the polarities of literals with respect to a specific variable.
Definition: sat.h:156
gymbosat::Var::getRight
std::shared_ptr< Expr > getRight() override
Get the right child expression.
Definition: sat.h:151
gymbosat::Var::unConst
bool unConst() override
Check if the logical expression can be simplified by removing constants.
Definition: sat.h:145
gymbosat::Var::literals
std::unordered_set< std::string > literals() override
Get the literals present in the logical expression.
Definition: sat.h:155
gymbosat::Var::distribute
std::shared_ptr< Expr > distribute() override
Distribute operations in the logical expression.
Definition: sat.h:149
gymbosat::Var::freeVar
std::pair< bool, std::string > freeVar() override
Identify and return free variables in the logical expression.
Definition: sat.h:142
gymbosat::Var::unitClause
std::pair< std::string, bool > unitClause() override
Get a unit clause from the logical expression.
Definition: sat.h:165
gymbosat::Var::to_string
std::string to_string() override
Convert the logical expression to a string representation.
Definition: sat.h:141
gymbosat::Var::getLeft
std::shared_ptr< Expr > getLeft() override
Get the left child expression.
Definition: sat.h:150
gymbosat::Var::simplify
std::shared_ptr< Expr > simplify() override
Simplify the logical expression.
Definition: sat.h:143
gymbosat::Var::fixNegations
std::shared_ptr< Expr > fixNegations() override
Fix negations in the logical expression.
Definition: sat.h:148
gymbosat::Var::evaluate
bool evaluate() override
Evaluate the logical expression.
Definition: sat.h:144
gymbo::SymType::SAnd
@ SAnd
gymbo::SymType::SOr
@ SOr
gymbo::SymType::SNot
@ SNot
gymbo::expr
Node * expr(Token *&token, char *user_input)
Parses an expression from a C-like language program.
Definition: parser.h:210
gymbosat
Definition: sat.h:12
gymbosat::sym2expr
std::shared_ptr< Expr > sym2expr(gymbo::Sym *sym, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map)
Convert a symbolic expression to a logical expression.
Definition: sat.h:735
gymbosat::satisfiableDPLL
bool satisfiableDPLL(std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
Check satisfiability of a logical expression using the DPLL algorithm.
Definition: sat.h:685
gymbosat::literalElimination
std::shared_ptr< Expr > literalElimination(std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
Eliminate literals in a logical expression based on assignments.
Definition: sat.h:604
gymbosat::allUnitClauses
std::vector< std::pair< std::string, bool > > allUnitClauses(std::shared_ptr< Expr > expr)
Extract all unit clauses from a logical expression.
Definition: sat.h:641
gymbosat::OpCode
OpCode
Enum representing different logical operation codes.
Definition: sat.h:17
gymbosat::VAR
@ VAR
Definition: sat.h:17
gymbosat::CONST
@ CONST
Definition: sat.h:17
gymbosat::NOT
@ NOT
Definition: sat.h:17
gymbosat::OR
@ OR
Definition: sat.h:17
gymbosat::AND
@ AND
Definition: sat.h:17
gymbosat::pathconstraints2expr
std::shared_ptr< Expr > pathconstraints2expr(std::vector< gymbo::Sym > &constraints, std::unordered_map< std::string, gymbo::Sym * > &unique_sym_map)
Convert a vector of symbolic path constraints to a logical expression.
Definition: sat.h:765
gymbosat::unitPropagation
std::shared_ptr< Expr > unitPropagation(std::shared_ptr< Expr > expr, std::unordered_map< std::string, bool > &assignments_map)
Perform unit propagation on a logical expression based on assignments.
Definition: sat.h:660
gymbosat::Polarity
Polarity
Enum representing different polarities in logical expressions.
Definition: sat.h:22
gymbosat::Positive
@ Positive
Definition: sat.h:22
gymbosat::Mixed
@ Mixed
Definition: sat.h:22
gymbosat::Negative
@ Negative
Definition: sat.h:22
gymbosat::cnf
std::shared_ptr< Expr > cnf(std::shared_ptr< Expr > expr)
Convert a logical expression to conjunctive normal form (CNF).
Definition: sat.h:589
gymbo::Sym
Struct representing a symbolic expression.
Definition: type.h:265
gymbo::Sym::right
Sym * right
Definition: type.h:268
gymbo::Sym::symtype
SymType symtype
Definition: type.h:266
gymbo::Sym::left
Sym * left
Definition: type.h:267
gymbo::Sym::toString
std::string toString(bool convert_to_num) const
Converts the symbolic expression to a string representation.
Definition: type.h:694
type.h
Implementatations of basic alias, types, and classes.