blob: 875d0cd165cdb0a58a4c3ebceff48e7873fbae67 (
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
|
/********************* -*- 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_cnfStream = new CVC4::prop::TseitinCnfStream(this);
}
PropEngine::~PropEngine(){
delete d_cnfStream;
}
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);
}
void PropEngine::solve() {
//TODO: may need to restart if a previous query returned false
d_sat.verbosity = 1;
bool result = d_sat.solve();
Notice() << "result is " << (result ? "sat/invalid" : "unsat/valid") << endl;
}
}/* CVC4 namespace */
|
