From 06e088262574a9f3e1638d89b93a25ae83514820 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 29 Aug 2012 20:36:35 +0000 Subject: [PATCH] * Numerous documentation fixes (fix doxygen warnings, add missing documentation, etc.). * Remove sat_module.cpp, which was no longer used (was previously refactored?) --- README | 6 +- config/doxygen.cfg | 9 +- src/bindings/compat/c/c_interface.h | 8 +- src/bindings/compat/c/c_interface_defs.h | 10 +- src/bindings/compat/java/formula_value.h | 6 +- src/decision/justification_heuristic.cpp | 4 +- src/expr/expr_manager_template.cpp | 2 +- src/expr/expr_manager_template.h | 4 +- src/expr/expr_template.cpp | 2 +- src/expr/expr_template.h | 5 +- src/expr/kind_template.h | 2 +- src/expr/metakind_template.h | 2 +- src/expr/symbol_table.h | 2 + src/expr/type_checker_template.cpp | 2 +- src/expr/type_properties_template.h | 2 +- src/options/base_options_template.cpp | 2 +- src/options/base_options_template.h | 2 +- src/options/options_holder_template.h | 2 +- src/options/options_template.cpp | 2 +- src/parser/input.h | 17 +- src/prop/sat_module.cpp | 478 -------------------- src/prop/sat_solver.h | 41 +- src/smt/smt_options_template.cpp | 2 +- src/theory/bv/bitblast_strategies.cpp | 2 +- src/theory/bv/bitblast_strategies.h | 4 +- src/theory/bv/bitblaster.cpp | 2 +- src/theory/instantiator_tables_template.cpp | 2 +- src/theory/rewriter_tables_template.h | 2 +- src/theory/theory_traits_template.h | 5 +- src/theory/type_enumerator_template.cpp | 3 +- src/theory/uf/equality_engine.h | 22 +- src/util/cardinality.h | 2 +- src/util/integer.h.in | 2 +- src/util/rational.h.in | 2 +- src/util/tls.h.in | 2 +- 35 files changed, 98 insertions(+), 564 deletions(-) delete mode 100644 src/prop/sat_module.cpp diff --git a/README b/README index ed8edd53a..37c285639 100644 --- a/README +++ b/README @@ -5,7 +5,7 @@ This is a prerelease version of CVC4. To build, you'll need reasonably new automake, autoconf, and libtool installed (see below). Execute, - ./autogen.sh + ./autogen.sh ./configure make @@ -80,10 +80,10 @@ includes a diff of all changes made to cudd makefiles. *** Build dependencies The following tools and libraries are required to build CVC4 from -scratch. +scratch. Automake v1.11 -Autoconf v2.61 +Autoconf v2.61 Libtool v2.2 ANTLR3 v3.2 diff --git a/config/doxygen.cfg b/config/doxygen.cfg index 71d434959..f4713b616 100644 --- a/config/doxygen.cfg +++ b/config/doxygen.cfg @@ -568,7 +568,12 @@ WARN_LOGFILE = # directories like "/usr/src/myproject". Separate the files or directories # with spaces. -INPUT = $(CVC4_DOXYGEN_INPUT) +INPUT = $(SRCDIR)/AUTHORS \ + $(SRCDIR)/COPYING \ + $(SRCDIR)/NEWS \ + $(SRCDIR)/README \ + $(SRCDIR)/ChangeLog \ + $(CVC4_DOXYGEN_INPUT) # This tag can be used to specify the character encoding of the source files # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is @@ -1242,7 +1247,7 @@ SEARCH_INCLUDES = YES # contain include files that are not input files but should be processed by # the preprocessor. -INCLUDE_PATH = . +INCLUDE_PATH = . include $(SRCDIR)/src $(SRCDIR)/src/include # You can use the INCLUDE_FILE_PATTERNS tag to specify one or more wildcard # patterns (like *.h and *.hpp) to filter out the header-files in the diff --git a/src/bindings/compat/c/c_interface.h b/src/bindings/compat/c/c_interface.h index 14fea7478..379097c27 100644 --- a/src/bindings/compat/c/c_interface.h +++ b/src/bindings/compat/c/c_interface.h @@ -12,7 +12,7 @@ * License to use, copy, modify, sell and/or distribute this software * and its documentation for any purpose is hereby granted without * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. + * COPYING file provided with this distribution. * *
* @@ -66,6 +66,8 @@ Type vc_subRangeType(VC vc, int lowerEnd, int upperEnd); //! Creates a subtype defined by the given predicate /*! + * \param vc the validity checker + * * \param pred is a predicate taking one argument of type T and returning * Boolean. The resulting type is a subtype of T whose elements x are those * satisfying the predicate pred(x). @@ -298,6 +300,7 @@ Expr vc_ratExprFromStr(VC vc, char* n, char* d, int base); //! Create a rational from a single string. /*! + \param vc the validity checker \param n can be a string containing an integer, a pair of integers "nnn/ddd", or a number in the fixed or floating point format. \param base is the base in which to interpret the string. @@ -442,7 +445,8 @@ Expr vc_datatypeTestExpr(VC vc, char* constructor, Expr arg); // Quantifiers //! Create a bound variable. -/*! \param name +/*! \param vc the validity checker + * \param name * \param uid is a fresh unique string to distinguish this variable * from other bound variables with the same name * \param type diff --git a/src/bindings/compat/c/c_interface_defs.h b/src/bindings/compat/c/c_interface_defs.h index ee6c09e13..f30e9b797 100644 --- a/src/bindings/compat/c/c_interface_defs.h +++ b/src/bindings/compat/c/c_interface_defs.h @@ -1,9 +1,9 @@ /*****************************************************************************/ /*! * \file c_interface_defs.h - * + * * Author: Clark Barrett - * + * * Created: Thu Jun 5 13:16:26 2003 * *
@@ -11,10 +11,10 @@ * License to use, copy, modify, sell and/or distribute this software * and its documentation for any purpose is hereby granted without * royalty, subject to the terms and conditions defined in the \ref - * LICENSE file provided with this distribution. - * + * COPYING file provided with this distribution. + * *
- * + * */ /*****************************************************************************/ diff --git a/src/bindings/compat/java/formula_value.h b/src/bindings/compat/java/formula_value.h index 79f31f404..efcd32eea 100644 --- a/src/bindings/compat/java/formula_value.h +++ b/src/bindings/compat/java/formula_value.h @@ -1,6 +1,6 @@ /*****************************************************************************/ /*! - *\file formulavalue.h + *\file formula_value.h *\brief enumerated type for value of formulas * * Author: Alexander Fuchs @@ -13,7 +13,7 @@ * and its documentation for any purpose is hereby granted without * royalty, subject to the terms and conditions defined in the \ref * LICENSE file provided with this distribution. - * + * *
*/ /*****************************************************************************/ @@ -31,7 +31,7 @@ namespace CVC3 { typedef enum FormulaValue { TRUE_VAL, FALSE_VAL, - UNKNOWN_VAL + UNKNOWN_VAL } FormulaValue; } diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 67000b1ba..77f4cd56c 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -21,8 +21,8 @@ **/ /*****************************************************************************/ /*! - *\file search_sat.cpp - *\brief Implementation of Search engine with generic external sat solver + * file search_sat.cpp + * brief Implementation of Search engine with generic external sat solver * * Author: Clark Barrett * diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 5e7aebbec..804d3af9a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file expr_manager_template.cpp +/*! \file expr_manager.cpp ** \verbatim ** Original author: dejan ** Major contributors: cconway, mdeters diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 158f17c14..8e0f23c6a 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file expr_manager_template.h +/*! \file expr_manager.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters @@ -210,7 +210,7 @@ public: * * @param kind the kind of expression to build * @param child1 the first subexpression - * @param children the remaining subexpressions + * @param otherChildren the remaining subexpressions * @return the n-ary expression */ Expr mkExpr(Kind kind, Expr child1, const std::vector& otherChildren); diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp index 365dc050f..a6f9f2cf6 100644 --- a/src/expr/expr_template.cpp +++ b/src/expr/expr_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file expr_template.cpp +/*! \file expr.cpp ** \verbatim ** Original author: dejan ** Major contributors: mdeters diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 395bdff3a..c50e85ac2 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file expr_template.h +/*! \file expr.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters @@ -403,6 +403,7 @@ public: * @param types set to true to ascribe types to the output * expressions (might break language compliance, but good for * debugging expressions) + * @param dag the dagification threshold to use (0 == off) * @param language the language in which to output */ void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, @@ -960,7 +961,7 @@ public: ${getConst_instantiations} -#line 964 "${template}" +#line 965 "${template}" namespace expr { diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 1acbed978..fc7d838a1 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file kind_template.h +/*! \file kind.h ** \verbatim ** Original author: mdeters ** Major contributors: dejan diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index a954a7f70..dbaba664c 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file metakind_template.h +/*! \file metakind.h ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h index ee04b17fd..3f24d10f8 100644 --- a/src/expr/symbol_table.h +++ b/src/expr/symbol_table.h @@ -118,6 +118,8 @@ public: * @param name an identifier * @param params the parameters to the type * @param t the type to bind to name + * @param levelZero true to bind it globally (default is to bind it + * locally within the current scope) */ void bindType(const std::string& name, const std::vector& params, diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 9359a6ab8..d559477f1 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file type_checker_template.cpp +/*! \file type_checker.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 1e983e86c..ee7a93144 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file type_properties_template.h +/*! \file type_properties.h ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/options/base_options_template.cpp b/src/options/base_options_template.cpp index 97d747652..e3d62936b 100644 --- a/src/options/base_options_template.cpp +++ b/src/options/base_options_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file base_options_template.cpp +/*! \file base_options.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/options/base_options_template.h b/src/options/base_options_template.h index 211cb866a..97c19930e 100644 --- a/src/options/base_options_template.h +++ b/src/options/base_options_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file base_options_template.h +/*! \file base_options.h ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/options/options_holder_template.h b/src/options/options_holder_template.h index 5b2c9a35d..2d37475f0 100644 --- a/src/options/options_holder_template.h +++ b/src/options/options_holder_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file options_holder_template.h +/*! \file options_holder.h ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index 97a588414..560efdfe3 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file options_template.cpp +/*! \file options.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/parser/input.h b/src/parser/input.h index 1b8c97713..d47ca4d12 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -68,7 +68,7 @@ protected: public: /** Destructor. */ - virtual ~InputStream() { + virtual ~InputStream() { if( d_fileIsTemporary ) { remove(d_name.c_str()); } @@ -108,8 +108,8 @@ public: * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(InputLanguage lang, - const std::string& filename, + static Input* newFileInput(InputLanguage lang, + const std::string& filename, bool useMmap = false) throw (InputStreamException, AssertionException); @@ -118,9 +118,12 @@ public: * @param lang the input language * @param input the input stream * @param name the name of the stream, for use in error messages + * @param lineBuffered whether this Input should be line-buffered + * (false, the default, means that the entire Input might be read + * before being lexed and parsed) */ - static Input* newStreamInput(InputLanguage lang, - std::istream& input, + static Input* newStreamInput(InputLanguage lang, + std::istream& input, const std::string& name, bool lineBuffered = false) throw (InputStreamException, AssertionException); @@ -131,8 +134,8 @@ public: * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(InputLanguage lang, - const std::string& input, + static Input* newStringInput(InputLanguage lang, + const std::string& input, const std::string& name) throw (InputStreamException, AssertionException); diff --git a/src/prop/sat_module.cpp b/src/prop/sat_module.cpp deleted file mode 100644 index ca41eac2f..000000000 --- a/src/prop/sat_module.cpp +++ /dev/null @@ -1,478 +0,0 @@ -/********************* */ -/*! \file sat.cpp - ** \verbatim - ** Original author: cconway - ** Major contributors: dejan, taking, mdeters, lianah - ** Minor contributors (to current version): none - ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 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.\endverbatim - ** - ** \brief [[ Add one-line brief description here ]] - ** - ** [[ Add lengthier description here ]] - ** \todo document this file - **/ - -#include "prop/prop_engine.h" -#include "prop/sat_module.h" -#include "context/context.h" -#include "theory/theory_engine.h" -#include "expr/expr_stream.h" -#include "prop/sat.h" - -// DPLLT Minisat -#include "prop/minisat/simp/SimpSolver.h" - -// BV Minisat -#include "prop/bvminisat/simp/SimpSolver.h" - - -using namespace std; - -namespace CVC4 { -namespace prop { - -string SatLiteral::toString() { - ostringstream os; - os << (isNegated()? "~" : "") << getSatVariable() << " "; - return os.str(); -} - -MinisatSatSolver::MinisatSatSolver() : - d_minisat(new BVMinisat::SimpSolver()) -{ - d_statistics.init(d_minisat); -} - -MinisatSatSolver::~MinisatSatSolver() { - delete d_minisat; -} - -void MinisatSatSolver::addClause(SatClause& clause, bool removable) { - Debug("sat::minisat") << "Add clause " << clause <<"\n"; - BVMinisat::vec minisat_clause; - toMinisatClause(clause, minisat_clause); - // for(unsigned i = 0; i < minisat_clause.size(); ++i) { - // d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true); - // } - d_minisat->addClause(minisat_clause); -} - -SatVariable MinisatSatSolver::newVar(bool freeze){ - return d_minisat->newVar(true, true, freeze); -} - -void MinisatSatSolver::markUnremovable(SatLiteral lit){ - d_minisat->setFrozen(BVMinisat::var(toMinisatLit(lit)), true); -} - -void MinisatSatSolver::interrupt(){ - d_minisat->interrupt(); -} - -SatLiteralValue MinisatSatSolver::solve(){ - return toSatLiteralValue(d_minisat->solve()); -} - -SatLiteralValue MinisatSatSolver::solve(long unsigned int& resource){ - Trace("limit") << "MinisatSatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; - if(resource == 0) { - d_minisat->budgetOff(); - } else { - d_minisat->setConfBudget(resource); - } - BVMinisat::vec empty; - unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); - d_minisat->clearInterrupt(); - resource = d_minisat->conflicts - conflictsBefore; - Trace("limit") << " & assumptions){ - Debug("sat::minisat") << "Solve with assumptions "; - context::CDList::const_iterator it = assumptions.begin(); - BVMinisat::vec assump; - for(; it!= assumptions.end(); ++it) { - SatLiteral lit = *it; - Debug("sat::minisat") << lit <<" "; - assump.push(toMinisatLit(lit)); - } - Debug("sat::minisat") <<"\n"; - - SatLiteralValue result = toSatLiteralValue(d_minisat->solve(assump)); - return result; -} - - -void MinisatSatSolver::getUnsatCore(SatClause& unsatCore) { - // TODO add assertion to check the call was after an unsat call - for (int i = 0; i < d_minisat->conflict.size(); ++i) { - unsatCore.push_back(toSatLiteral(d_minisat->conflict[i])); - } -} - -SatLiteralValue MinisatSatSolver::value(SatLiteral l){ - Unimplemented(); - return SatValUnknown; -} - -SatLiteralValue MinisatSatSolver::modelValue(SatLiteral l){ - Unimplemented(); - return SatValUnknown; -} - -void MinisatSatSolver::unregisterVar(SatLiteral lit) { - // this should only be called when user context is implemented - // in the BVSatSolver - Unreachable(); -} - -void MinisatSatSolver::renewVar(SatLiteral lit, int level) { - // this should only be called when user context is implemented - // in the BVSatSolver - - Unreachable(); -} - -int MinisatSatSolver::getAssertionLevel() const { - // we have no user context implemented so far - return 0; -} - -// converting from internal Minisat representation - -SatVariable MinisatSatSolver::toSatVariable(BVMinisat::Var var) { - if (var == var_Undef) { - return undefSatVariable; - } - return SatVariable(var); -} - -BVMinisat::Lit MinisatSatSolver::toMinisatLit(SatLiteral lit) { - if (lit == undefSatLiteral) { - return BVMinisat::lit_Undef; - } - return BVMinisat::mkLit(lit.getSatVariable(), lit.isNegated()); -} - -SatLiteral MinisatSatSolver::toSatLiteral(BVMinisat::Lit lit) { - if (lit == BVMinisat::lit_Undef) { - return undefSatLiteral; - } - - return SatLiteral(SatVariable(BVMinisat::var(lit)), - BVMinisat::sign(lit)); -} - -SatLiteralValue MinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; -} - -SatLiteralValue MinisatSatSolver::toSatLiteralValue(BVMinisat::lbool res) { - if(res == (BVMinisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (BVMinisat::lbool((uint8_t)2))) return SatValUnknown; - Assert(res == (BVMinisat::lbool((uint8_t)1))); - return SatValFalse; -} - -void MinisatSatSolver::toMinisatClause(SatClause& clause, - BVMinisat::vec& minisat_clause) { - for (unsigned i = 0; i < clause.size(); ++i) { - minisat_clause.push(toMinisatLit(clause[i])); - } - Assert(clause.size() == (unsigned)minisat_clause.size()); -} - -void MinisatSatSolver::toSatClause(BVMinisat::vec& 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()); -} - - -// Satistics for MinisatSatSolver - -MinisatSatSolver::Statistics::Statistics() : - d_statStarts("theory::bv::bvminisat::starts"), - d_statDecisions("theory::bv::bvminisat::decisions"), - d_statRndDecisions("theory::bv::bvminisat::rnd_decisions"), - d_statPropagations("theory::bv::bvminisat::propagations"), - d_statConflicts("theory::bv::bvminisat::conflicts"), - d_statClausesLiterals("theory::bv::bvminisat::clauses_literals"), - d_statLearntsLiterals("theory::bv::bvminisat::learnts_literals"), - d_statMaxLiterals("theory::bv::bvminisat::max_literals"), - d_statTotLiterals("theory::bv::bvminisat::tot_literals"), - d_statEliminatedVars("theory::bv::bvminisat::eliminated_vars") -{ - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); - StatisticsRegistry::registerStat(&d_statEliminatedVars); -} - -MinisatSatSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); - StatisticsRegistry::unregisterStat(&d_statEliminatedVars); -} - -void MinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){ - d_statStarts.setData(minisat->starts); - d_statDecisions.setData(minisat->decisions); - d_statRndDecisions.setData(minisat->rnd_decisions); - d_statPropagations.setData(minisat->propagations); - d_statConflicts.setData(minisat->conflicts); - d_statClausesLiterals.setData(minisat->clauses_literals); - d_statLearntsLiterals.setData(minisat->learnts_literals); - d_statMaxLiterals.setData(minisat->max_literals); - d_statTotLiterals.setData(minisat->tot_literals); - d_statEliminatedVars.setData(minisat->eliminated_vars); -} - - - -//// DPllMinisatSatSolver - -DPLLMinisatSatSolver::DPLLMinisatSatSolver() : - d_minisat(NULL), - d_theoryProxy(NULL), - d_context(NULL) -{} - -DPLLMinisatSatSolver::~DPLLMinisatSatSolver() { - delete d_minisat; -} - -SatVariable DPLLMinisatSatSolver::toSatVariable(Minisat::Var var) { - if (var == var_Undef) { - return undefSatVariable; - } - return SatVariable(var); -} - -Minisat::Lit DPLLMinisatSatSolver::toMinisatLit(SatLiteral lit) { - if (lit == undefSatLiteral) { - return Minisat::lit_Undef; - } - return Minisat::mkLit(lit.getSatVariable(), lit.isNegated()); -} - -SatLiteral DPLLMinisatSatSolver::toSatLiteral(Minisat::Lit lit) { - if (lit == Minisat::lit_Undef) { - return undefSatLiteral; - } - - return SatLiteral(SatVariable(Minisat::var(lit)), - Minisat::sign(lit)); -} - -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(bool res) { - if(res) return SatValTrue; - else return SatValFalse; -} - -SatLiteralValue DPLLMinisatSatSolver::toSatLiteralValue(Minisat::lbool res) { - if(res == (Minisat::lbool((uint8_t)0))) return SatValTrue; - if(res == (Minisat::lbool((uint8_t)2))) return SatValUnknown; - Assert(res == (Minisat::lbool((uint8_t)1))); - return SatValFalse; -} - - -void DPLLMinisatSatSolver::toMinisatClause(SatClause& clause, - Minisat::vec& minisat_clause) { - for (unsigned i = 0; i < clause.size(); ++i) { - minisat_clause.push(toMinisatLit(clause[i])); - } - Assert(clause.size() == (unsigned)minisat_clause.size()); -} - -void DPLLMinisatSatSolver::toSatClause(Minisat::vec& 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 DPLLMinisatSatSolver::initialize(context::Context* context, TheoryProxy* theoryProxy) -{ - - d_context = context; - - // Create the solver - d_minisat = new Minisat::SimpSolver(theoryProxy, d_context, - options::incrementalSolving()); - // Setup the verbosity - d_minisat->verbosity = (options::verbosity() > 0) ? 1 : -1; - - // Setup the random decision parameters - d_minisat->random_var_freq = options::satRandomFreq(); - d_minisat->random_seed = 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 DPLLMinisatSatSolver::addClause(SatClause& clause, bool removable) { - Minisat::vec minisat_clause; - toMinisatClause(clause, minisat_clause); - d_minisat->addClause(minisat_clause, removable); -} - -SatVariable DPLLMinisatSatSolver::newVar(bool theoryAtom) { - return d_minisat->newVar(true, true, theoryAtom); -} - - -SatLiteralValue DPLLMinisatSatSolver::solve(unsigned long& resource) { - Trace("limit") << "SatSolver::solve(): have limit of " << resource << " conflicts" << std::endl; - if(resource == 0) { - d_minisat->budgetOff(); - } else { - d_minisat->setConfBudget(resource); - } - Minisat::vec empty; - unsigned long conflictsBefore = d_minisat->conflicts; - SatLiteralValue result = toSatLiteralValue(d_minisat->solveLimited(empty)); - d_minisat->clearInterrupt(); - resource = d_minisat->conflicts - conflictsBefore; - Trace("limit") << "SatSolver::solve(): it took " << resource << " conflicts" << std::endl; - return result; -} - -SatLiteralValue DPLLMinisatSatSolver::solve() { - d_minisat->budgetOff(); - return toSatLiteralValue(d_minisat->solve()); -} - - -void DPLLMinisatSatSolver::interrupt() { - d_minisat->interrupt(); -} - -SatLiteralValue DPLLMinisatSatSolver::value(SatLiteral l) { - return toSatLiteralValue(d_minisat->value(toMinisatLit(l))); -} - -SatLiteralValue DPLLMinisatSatSolver::modelValue(SatLiteral l){ - return toSatLiteralValue(d_minisat->modelValue(toMinisatLit(l))); -} - -bool DPLLMinisatSatSolver::properExplanation(SatLiteral lit, SatLiteral expl) const { - return true; -} - -/** Incremental interface */ - -int DPLLMinisatSatSolver::getAssertionLevel() const { - return d_minisat->getAssertionLevel(); -} - -void DPLLMinisatSatSolver::push() { - d_minisat->push(); -} - -void DPLLMinisatSatSolver::pop(){ - d_minisat->pop(); -} - -void DPLLMinisatSatSolver::unregisterVar(SatLiteral lit) { - d_minisat->unregisterVar(toMinisatLit(lit)); -} - -void DPLLMinisatSatSolver::renewVar(SatLiteral lit, int level) { - d_minisat->renewVar(toMinisatLit(lit), level); -} - -/// Statistics for DPLLMinisatSatSolver - -DPLLMinisatSatSolver::Statistics::Statistics() : - d_statStarts("sat::starts"), - d_statDecisions("sat::decisions"), - d_statRndDecisions("sat::rnd_decisions"), - d_statPropagations("sat::propagations"), - d_statConflicts("sat::conflicts"), - d_statClausesLiterals("sat::clauses_literals"), - d_statLearntsLiterals("sat::learnts_literals"), - d_statMaxLiterals("sat::max_literals"), - d_statTotLiterals("sat::tot_literals") -{ - StatisticsRegistry::registerStat(&d_statStarts); - StatisticsRegistry::registerStat(&d_statDecisions); - StatisticsRegistry::registerStat(&d_statRndDecisions); - StatisticsRegistry::registerStat(&d_statPropagations); - StatisticsRegistry::registerStat(&d_statConflicts); - StatisticsRegistry::registerStat(&d_statClausesLiterals); - StatisticsRegistry::registerStat(&d_statLearntsLiterals); - StatisticsRegistry::registerStat(&d_statMaxLiterals); - StatisticsRegistry::registerStat(&d_statTotLiterals); -} -DPLLMinisatSatSolver::Statistics::~Statistics() { - StatisticsRegistry::unregisterStat(&d_statStarts); - StatisticsRegistry::unregisterStat(&d_statDecisions); - StatisticsRegistry::unregisterStat(&d_statRndDecisions); - StatisticsRegistry::unregisterStat(&d_statPropagations); - StatisticsRegistry::unregisterStat(&d_statConflicts); - StatisticsRegistry::unregisterStat(&d_statClausesLiterals); - StatisticsRegistry::unregisterStat(&d_statLearntsLiterals); - StatisticsRegistry::unregisterStat(&d_statMaxLiterals); - StatisticsRegistry::unregisterStat(&d_statTotLiterals); -} -void DPLLMinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){ - d_statStarts.setData(d_minisat->starts); - d_statDecisions.setData(d_minisat->decisions); - d_statRndDecisions.setData(d_minisat->rnd_decisions); - d_statPropagations.setData(d_minisat->propagations); - d_statConflicts.setData(d_minisat->conflicts); - d_statClausesLiterals.setData(d_minisat->clauses_literals); - d_statLearntsLiterals.setData(d_minisat->learnts_literals); - d_statMaxLiterals.setData(d_minisat->max_literals); - d_statTotLiterals.setData(d_minisat->tot_literals); -} - - -/* - - SatSolverFactory - - */ - -MinisatSatSolver* SatSolverFactory::createMinisat() { - return new MinisatSatSolver(); -} - -DPLLMinisatSatSolver* SatSolverFactory::createDPLLMinisat(){ - return new DPLLMinisatSatSolver(); -} - - -}/* CVC4::prop namespace */ -}/* CVC4 namespace */ diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h index d2e967393..567f897a1 100644 --- a/src/prop/sat_solver.h +++ b/src/prop/sat_solver.h @@ -18,8 +18,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__PROP__SAT_MODULE_H -#define __CVC4__PROP__SAT_MODULE_H +#ifndef __CVC4__PROP__SAT_SOLVER_H +#define __CVC4__PROP__SAT_SOLVER_H #include #include @@ -30,21 +30,21 @@ namespace CVC4 { namespace prop { -class TheoryProxy; +class TheoryProxy; class SatSolver { -public: +public: /** Virtual destructor */ virtual ~SatSolver() { } - + /** Assert a clause in the solver. */ virtual void addClause(SatClause& clause, bool removable) = 0; /** Create a new boolean variable in the solver. */ virtual SatVariable newVar(bool theoryAtom = false) = 0; - + /** Create a new (or return an existing) boolean variable representing the constant true */ virtual SatVariable trueVar() = 0; @@ -56,7 +56,7 @@ public: /** Check the satisfiability of the added clauses */ virtual SatValue solve(long unsigned int&) = 0; - + /** Interrupt the solver */ virtual void interrupt() = 0; @@ -67,12 +67,12 @@ public: virtual SatValue modelValue(SatLiteral l) = 0; virtual void unregisterVar(SatLiteral lit) = 0; - + virtual void renewVar(SatLiteral lit, int level = -1) = 0; virtual unsigned getAssertionLevel() const = 0; -}; +};/* class SatSolver */ class BVSatSolverInterface: public SatSolver { @@ -94,30 +94,31 @@ public: * Notify about a learnt clause. */ virtual void notify(SatClause& clause) = 0; - }; + };/* class BVSatSolverInterface::Notify */ + + virtual void setNotify(Notify* notify) = 0; - virtual void setNotify(Notify* notify) = 0; - virtual void markUnremovable(SatLiteral lit) = 0; - virtual void getUnsatCore(SatClause& unsatCore) = 0; + virtual void getUnsatCore(SatClause& unsatCore) = 0; - virtual void addMarkerLiteral(SatLiteral lit) = 0; + virtual void addMarkerLiteral(SatLiteral lit) = 0; virtual SatValue propagate() = 0; virtual void explain(SatLiteral lit, std::vector& explanation) = 0; - virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; + virtual SatValue assertAssumption(SatLiteral lit, bool propagate = false) = 0; virtual void popAssumption() = 0; -}; + +};/* class BVSatSolverInterface */ class DPLLSatSolverInterface: public SatSolver { public: - virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; - + virtual void initialize(context::Context* context, prop::TheoryProxy* theoryProxy) = 0; + virtual void push() = 0; virtual void pop() = 0; @@ -130,9 +131,9 @@ public: virtual bool isDecision(SatVariable decn) const = 0; -}; +};/* class DPLLSatSolverInterface */ -}/* prop namespace */ +}/* CVC4::prop namespace */ inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) { out << lit.toString(); diff --git a/src/smt/smt_options_template.cpp b/src/smt/smt_options_template.cpp index 1af029f17..deec881e4 100644 --- a/src/smt/smt_options_template.cpp +++ b/src/smt/smt_options_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file smt_options_template.cpp +/*! \file smt_options.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index 8cfdab5af..80b689b8c 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -100,7 +100,7 @@ void inline makeZero(Bits& bits, unsigned width) { * * @param a first term to be added * @param b second term to be added - * @param sum the sum + * @param res the result * @param carry the carry-in bit * * @return the carry-out diff --git a/src/theory/bv/bitblast_strategies.h b/src/theory/bv/bitblast_strategies.h index 826b61d4f..5b53678dd 100644 --- a/src/theory/bv/bitblast_strategies.h +++ b/src/theory/bv/bitblast_strategies.h @@ -41,7 +41,6 @@ typedef std::vector Bits; * Default Atom Bitblasting strategies: * * @param node the atom to be bitblasted - * @param markerLit the marker literal corresponding to the atom * @param bb the bitblaster */ @@ -68,9 +67,8 @@ Node SleBB(TNode node, Bitblaster* bb); * Default Term Bitblasting strategies * * @param node the term to be bitblasted + * @param bits [output parameter] bits representing the new term * @param bb the bitblaster in which the clauses are added - * - * @return the bits representing the new term */ void UndefinedTermBBStrategy(TNode node, Bits& bits, Bitblaster* bb); diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp index c86f14398..eb5f3e155 100644 --- a/src/theory/bv/bitblaster.cpp +++ b/src/theory/bv/bitblaster.cpp @@ -170,7 +170,7 @@ void Bitblaster::explain(TNode atom, std::vector& explanation) { /** * Asserts the clauses corresponding to the atom to the Sat Solver * by turning on the marker literal (i.e. setting it to false) - * @param node the atom to be aserted + * @param node the atom to be asserted * */ diff --git a/src/theory/instantiator_tables_template.cpp b/src/theory/instantiator_tables_template.cpp index 7a78c3aae..7234993fa 100644 --- a/src/theory/instantiator_tables_template.cpp +++ b/src/theory/instantiator_tables_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file instantiator_tables_template.cpp +/*! \file instantiator_tables.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 9ab98168e..6533e9335 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file rewriter_tables_template.h +/*! \file rewriter_tables.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index bbf13b425..4522af568 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_traits_template.h +/*! \file theory_traits.h ** \verbatim ** Original author: dejan ** Major contributors: mdeters @@ -27,7 +27,6 @@ ${theory_includes} namespace CVC4 { - namespace theory { template @@ -37,5 +36,5 @@ ${theory_traits} ${theory_for_each_macro} -}/* theory namespace */ +}/* CVC4::theory namespace */ }/* CVC4 namespace */ diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index 426bf52a0..0619a900f 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file type_enumerator_template.cpp +/*! \file type_enumerator.cpp ** \verbatim ** Original author: mdeters ** Major contributors: none @@ -58,4 +58,3 @@ ${mk_type_enumerator_cases} }/* CVC4::theory namespace */ }/* CVC4 namespace */ - diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h index 7f216d634..1e3b276a4 100644 --- a/src/theory/uf/equality_engine.h +++ b/src/theory/uf/equality_engine.h @@ -58,7 +58,7 @@ public: /** * Notifies about a trigger equality that became true or false. * - * @param eq the equality that became true or false + * @param equality the equality that became true or false * @param value the value of the equality */ virtual bool eqNotifyTriggerEquality(TNode equality, bool value) = 0; @@ -680,13 +680,13 @@ public: /** * Adds a predicate p with given polarity. The predicate asserted - * should be in the congruence closure kinds (otherwise it's + * should be in the congruence closure kinds (otherwise it's * useless. * * @param p the (non-negated) predicate - * @param polarity true if asserting the predicate, false if + * @param polarity true if asserting the predicate, false if * asserting the negated predicate - * @param the reason to keep for building explanations + * @param reason the reason to keep for building explanations */ void assertPredicate(TNode p, bool polarity, TNode reason); @@ -694,9 +694,9 @@ public: * Adds an equality eq with the given polarity to the database. * * @param eq the (non-negated) equality - * @param polarity true if asserting the equality, false if + * @param polarity true if asserting the equality, false if * asserting the negated equality - * @param the reason to keep for building explanations + * @param reason the reason to keep for building explanations */ void assertEquality(TNode eq, bool polarity, TNode reason); @@ -706,20 +706,20 @@ public: TNode getRepresentative(TNode t) const; /** - * Add all the terms where the given term appears as a first child + * Add all the terms where the given term appears as a first child * (directly or implicitly). */ void getUseListTerms(TNode t, std::set& output); /** - * Get an explanation of the equality t1 = t2 begin true of false. + * Get an explanation of the equality t1 = t2 begin true of false. * Returns the reasons (added when asserting) that imply it * in the assertions vector. */ void explainEquality(TNode t1, TNode t2, bool polarity, std::vector& assertions) const; /** - * Get an explanation of the predicate being true or false. + * Get an explanation of the predicate being true or false. * Returns the reasons (added when asserting) that imply imply it * in the assertions vector. */ @@ -733,12 +733,12 @@ public: * it's own notification. * * @param t the trigger term - * @param tag tag for this trigger (do NOT use THEORY_LAST) + * @param theoryTag tag for this trigger (do NOT use THEORY_LAST) */ void addTriggerTerm(TNode t, TheoryId theoryTag); /** - * Returns true if t is a trigger term or in the same equivalence + * Returns true if t is a trigger term or in the same equivalence * class as some other trigger term. */ bool isTriggerTerm(TNode t, TheoryId theoryTag) const; diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 30bdea78d..81a291006 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -165,7 +165,7 @@ public: /** * Returns true iff this cardinality is finite and large (i.e., * at the ceiling of representable finite cardinalities). - . */ + */ bool isLargeFinite() const throw() { return d_card >= s_largeFiniteCard; } diff --git a/src/util/integer.h.in b/src/util/integer.h.in index b2973081d..1fdaf0215 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -1,5 +1,5 @@ /********************* */ -/*! \file integer.h.in +/*! \file integer.h ** \verbatim ** Original author: taking ** Major contributors: none diff --git a/src/util/rational.h.in b/src/util/rational.h.in index 17c1e31fc..f97559377 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -1,5 +1,5 @@ /********************* */ -/*! \file rational.h.in +/*! \file rational.h ** \verbatim ** Original author: taking ** Major contributors: none diff --git a/src/util/tls.h.in b/src/util/tls.h.in index df53cae36..cd89be9d0 100644 --- a/src/util/tls.h.in +++ b/src/util/tls.h.in @@ -1,5 +1,5 @@ /********************* */ -/*! \file tls.h.in +/*! \file tls.h ** \verbatim ** Original author: mdeters ** Major contributors: none -- 2.30.2