From 01e3d838982658349f429063834379b7cda43dbc Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 11 Mar 2014 15:07:38 -0400 Subject: [PATCH] Fix some Win32 and SMT-LIB compliance bugs discovered by David Cok. --- src/prop/minisat/minisat.cpp | 25 ++++++++++++++++++------- src/prop/minisat/minisat.h | 15 ++++++++------- src/prop/options | 2 +- src/smt/options | 2 +- src/smt/smt_options_template.cpp | 8 ++++++-- 5 files changed, 34 insertions(+), 18 deletions(-) diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp index 98e43aaf0..c4fe58fd7 100644 --- a/src/prop/minisat/minisat.cpp +++ b/src/prop/minisat/minisat.cpp @@ -5,7 +5,7 @@ ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2014 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 @@ -13,7 +13,7 @@ ** ** \brief SAT Solver. ** - ** Implementation of the minisat for cvc4. + ** Implementation of the minisat interface for cvc4. **/ #include "prop/minisat/minisat.h" @@ -111,8 +111,7 @@ void MinisatSatSolver::toSatClause(const Minisat::Clause& clause, Assert((unsigned)clause.size() == sat_clause.size()); } -void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) -{ +void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) { d_context = context; @@ -125,20 +124,30 @@ void MinisatSatSolver::initialize(context::Context* context, TheoryProxy* theory d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, options::incrementalSolving() || options::decisionMode() != decision::DECISION_STRATEGY_INTERNAL ); + + d_statistics.init(d_minisat); +} + +// Like initialize() above, but called just before each search when in +// incremental mode +void MinisatSatSolver::setupOptions() { + // Copy options from CVC4 options structure into minisat, as appropriate + // Set up the verbosity d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; // Set up the random decision parameters d_minisat->random_var_freq = options::satRandomFreq(); - d_minisat->random_seed = options::satRandomSeed(); + // If 0, we use whatever we like (here, the Minisat default seed) + if(options::satRandomSeed() != 0) { + d_minisat->random_seed = double(options::satRandomSeed()); + } // Give access to all possible options in the sat solver d_minisat->var_decay = options::satVarDecay(); d_minisat->clause_decay = options::satClauseDecay(); d_minisat->restart_first = options::satRestartFirst(); d_minisat->restart_inc = options::satRestartInc(); - - d_statistics.init(d_minisat); } void MinisatSatSolver::addClause(SatClause& clause, bool removable) { @@ -153,6 +162,7 @@ SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool c SatValue MinisatSatSolver::solve(unsigned long& resource) { Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; + setupOptions(); if(resource == 0) { d_minisat->budgetOff(); } else { @@ -168,6 +178,7 @@ SatValue MinisatSatSolver::solve(unsigned long& resource) { } SatValue MinisatSatSolver::solve() { + setupOptions(); d_minisat->budgetOff(); return toSatLiteralValue(d_minisat->solve()); } diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h index 27258b3c2..201879eb0 100644 --- a/src/prop/minisat/minisat.h +++ b/src/prop/minisat/minisat.h @@ -5,7 +5,7 @@ ** Major contributors: ** Minor contributors (to current version): ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2014 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 @@ -13,7 +13,7 @@ ** ** \brief SAT Solver. ** - ** Implementation of the minisat for cvc4. + ** Implementation of the minisat interface for cvc4. **/ #pragma once @@ -36,6 +36,8 @@ class MinisatSatSolver : public DPLLSatSolverInterface { /** Context we will be using to synchronize the sat solver */ context::Context* d_context; + void setupOptions(); + public: MinisatSatSolver(); @@ -96,11 +98,10 @@ public: Statistics(); ~Statistics(); void init(Minisat::SimpSolver* d_minisat); - }; + };/* class MinisatSatSolver::Statistics */ Statistics d_statistics; -}; - -} // prop namespace -} // cvc4 namespace +};/* class MinisatSatSolver */ +}/* CVC4::prop namespace */ +}/* CVC4 namespace */ diff --git a/src/prop/options b/src/prop/options index b300c3fb6..cf241479c 100644 --- a/src/prop/options +++ b/src/prop/options @@ -10,7 +10,7 @@ option - --show-sat-solvers void :handler CVC4::prop::showSatSolvers :handler-in option satRandomFreq random-frequency --random-freq=P double :default 0.0 :predicate greater_equal(0.0) less_equal(1.0) sets the frequency of random decisions in the sat solver (P=0.0 by default) -option satRandomSeed random-seed --random-seed=S double :default 91648253 :read-write +option satRandomSeed random-seed --random-seed=S uint32_t :default sets the random seed for the sat solver option satVarDecay double :default 0.95 :predicate less_equal(1.0) greater_equal(0.0) diff --git a/src/smt/options b/src/smt/options index 05a138f60..458f42d6a 100644 --- a/src/smt/options +++ b/src/smt/options @@ -36,7 +36,7 @@ option produceAssignments produce-assignments --produce-assignments bool :defaul # This could go in src/main/options, but by SMT-LIBv2 spec, "interactive" # is a mode in which the assertion list must be kept. So it belongs here. -common-option interactive interactive-mode --interactive bool :read-write +common-option interactive interactive-mode --interactive bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h" :read-write force interactive mode option doITESimp --ite-simp bool :read-write diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index 4edd91a8d..987d2e3c7 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -62,11 +62,15 @@ void SmtEngine::setOption(const std::string& key, const CVC4::SExpr& value) throw OptionException("command-verbosity value must be a tuple (command-name, integer)"); } + if(!value.isAtom()) { + throw OptionException("bad value for :" + key); + } + string optionarg = value.getValue(); ${smt_setoption_handlers} -#line 70 "${template}" +#line 74 "${template}" throw UnrecognizedOptionException(key); } @@ -126,7 +130,7 @@ CVC4::SExpr SmtEngine::getOption(const std::string& key) const ${smt_getoption_handlers} -#line 130 "${template}" +#line 134 "${template}" throw UnrecognizedOptionException(key); } -- 2.30.2