blob: b4df32f0f769b0126fb21a76a23c9822866cbf03 (
plain)
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
|
/********************* -*- C++ -*- */
/** prop_engine.cpp
** Original author: mdeters
** Major contributors: none
** Minor contributors (to current version): dejan
** 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 "prop/cnf_stream.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_restartMayBeNeeded(false){
d_sat = new Solver();
d_cnfStream = new CVC4::prop::TseitinCnfStream(this);
}
PropEngine::~PropEngine(){
delete d_cnfStream;
delete d_sat;
}
void PropEngine::assertClause(vec<Lit> & c){
/*we can also here add a context dependent queue of assertions
*for restarting the sat solver
*/
//TODO assert that each lit has been mapped to an atom or requested
d_sat->addClause(c);
}
void PropEngine::registerAtom(const Node & n, Lit l){
d_atom2lit.insert(make_pair(n,l));
d_lit2atom.insert(make_pair(l,n));
}
Lit PropEngine::requestFreshLit(){
Var v = d_sat->newVar();
Lit l(v,false);
return l;
}
void PropEngine::assertFormula(const Node& node) {
d_cnfStream->convertAndAssert(node);
d_assertionList.push_back(node);
}
void PropEngine::restart(){
delete d_sat;
d_sat = new Solver();
d_cnfStream->flushCache();
d_atom2lit.clear();
d_lit2atom.clear();
for(vector<Node>::iterator iter = d_assertionList.begin();
iter != d_assertionList.end(); ++iter){
d_cnfStream->convertAndAssert(*iter);
}
}
void PropEngine::solve() {
if(d_restartMayBeNeeded)
restart();
d_sat->verbosity = 1;
bool result = d_sat->solve();
if(!result){
d_restartMayBeNeeded = true;
}
Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
}
}/* CVC4 namespace */
|