1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
|
/********************* -*- C++ -*- */
/** prop_engine.h
** This file is part of the CVC4 prototype.
** Copyright (c) 2009 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
** information.
**
**/
#include "prop/prop_engine.h"
#include "theory/theory_engine.h"
#include "util/decision_engine.h"
#include "prop/minisat/mtl/Vec.h"
#include "prop/minisat/simp/SimpSolver.h"
#include "prop/minisat/core/SolverTypes.h"
#include "util/Assert.h"
#include "util/output.h"
#include <utility>
#include <map>
using namespace CVC4::prop::minisat;
using namespace std;
namespace CVC4 {
PropEngine::PropEngine(DecisionEngine& de, TheoryEngine& te) :
d_de(de), d_te(te), d_sat() {
}
void PropEngine::addVars(Expr e) {
Debug("prop") << "adding vars to " << e << endl;
for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
Debug("prop") << "expr " << *i << endl;
if(i->getKind() == VARIABLE) {
if(d_vars.find(*i) == d_vars.end()) {
Var v = d_sat.newVar();
Debug("prop") << "adding var " << *i << " <--> " << v << endl;
d_vars.insert(make_pair(*i, v));
d_varsReverse.insert(make_pair(v, *i));
} else Debug("prop") << "using var " << *i << " <--> " << d_vars[*i] << endl;
} else addVars(*i);
}
}
static void doAtom(SimpSolver* minisat, map<Expr, Var>* vars, Expr e, vec<Lit>* c) {
if(e.getKind() == VARIABLE) {
map<Expr, Var>::iterator v = vars->find(e);
Assert(v != vars->end());
c->push(Lit(v->second, false));
return;
}
if(e.getKind() == NOT) {
Assert(e.numChildren() == 1);
Expr child = *e.begin();
Assert(child.getKind() == VARIABLE);
map<Expr, Var>::iterator v = vars->find(child);
Assert(v != vars->end());
c->push(Lit(v->second, true));
return;
}
Unhandled();
}
static void doClause(SimpSolver* minisat, map<Expr, Var>* vars, map<Var, Expr>* varsReverse, Expr e) {
vec<Lit> c;
Debug("prop") << " " << e << endl;
if(e.getKind() == VARIABLE || e.getKind() == NOT) {
doAtom(minisat, vars, e, &c);
} else {
Assert(e.getKind() == OR);
for(Expr::iterator i = e.begin(); i != e.end(); ++i) {
Debug("prop") << " " << *i << endl;
doAtom(minisat, vars, *i, &c);
}
}
Notice() << "added clause of length " << c.size() << endl;
for(int i = 0; i < c.size(); ++i)
Notice() << " " << (sign(c[i]) ? "-" : "") << var(c[i]);
Notice() << " [[";
for(int i = 0; i < c.size(); ++i)
Notice() << " " << (sign(c[i]) ? "-" : "") << (*varsReverse)[var(c[i])];
Notice() << " ]] " << endl;
minisat->addClause(c);
}
void PropEngine::solve(Expr e) {
Debug("prop") << "SOLVING " << e << endl;
addVars(e);
if(e.getKind() == AND) {
Debug("prop") << "AND" << endl;
for(Expr::iterator i = e.begin(); i != e.end(); ++i)
doClause(&d_sat, &d_vars, &d_varsReverse, *i);
} else doClause(&d_sat, &d_vars, &d_varsReverse, e);
d_sat.verbosity = 1;
bool result = d_sat.solve();
Notice() << "result is " << (result ? "sat" : "unsat") << endl;
if(result) {
Notice() << "model:" << endl;
for(int i = 0; i < d_sat.model.size(); ++i)
Notice() << " " << toInt(d_sat.model[i]);
Notice() << endl;
for(int i = 0; i < d_sat.model.size(); ++i)
Notice() << " " << d_varsReverse[i] << " is "
<< (d_sat.model[i] == l_False ? "FALSE" :
(d_sat.model[i] == l_Undef ? "UNDEF" :
"TRUE")) << endl;
} else {
Notice() << "conflict:" << endl;
for(int i = 0; i < d_sat.conflict.size(); ++i)
Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << var(d_sat.conflict[i]);
Notice() << " [[";
for(int i = 0; i < d_sat.conflict.size(); ++i)
Notice() << " " << (sign(d_sat.conflict[i]) ? "-" : "") << d_varsReverse[var(d_sat.conflict[i])];
Notice() << " ]] " << endl;
}
}
}/* CVC4 namespace */
|
