From 3361081acd11178d0eb580ce91279a2ecaa7aa65 Mon Sep 17 00:00:00 2001 From: lianah Date: Tue, 8 Oct 2013 16:50:28 -0400 Subject: fixed uf proof with holes bugs --- src/prop/minisat/minisat.cpp | 7 +++++++ src/prop/minisat/minisat.h | 2 +- src/prop/sat_solver_types.h | 4 ++++ 3 files changed, 12 insertions(+), 1 deletion(-) (limited to 'src/prop') diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 960f2ad62..98e43aaf0 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -103,6 +103,13 @@ void MinisatSatSolver::toSatClause(Minisat::vec& clause, Assert((unsigned)clause.size() == sat_clause.size()); } +void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, + SatClause& sat_clause) { + for (int i = 0; i < clause.size(); ++i) { + sat_clause.push_back(toSatLiteral(clause[i])); + } + Assert((unsigned)clause.size() == sat_clause.size()); +} void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index ec49b5f71..27258b3c2 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -51,7 +51,7 @@ public: static void toMinisatClause(SatClause& clause, Minisat::vec& minisat_clause); static void toSatClause (Minisat::vec& clause, SatClause& sat_clause); - + static void toSatClause (const Minisat::Clause& clause, SatClause& sat_clause); void initialize(context::Context* context, TheoryProxy* theoryProxy); void addClause(SatClause& clause, bool removable); diff --git a/src/prop/sat_solver_types.h b/src/prop/sat_solver_types.h index ab2bcda47..8fee0d11e 100644 --- a/src/prop/sat_solver_types.h +++ b/src/prop/sat_solver_types.h @@ -135,6 +135,10 @@ public: return (size_t)d_value; } + uint64_t toInt() const { + return d_value; + } + /** * Returns true if the literal is undefined. */ -- cgit v1.2.3