.PHONY: test
test: check
+.PHONY: doc
+doc: doc-builds
+
submission:
if [ ! -e configure ]; then ./autogen.sh; fi
./configure competition --disable-shared --enable-static-binary
.PHONY: TAGS tags
+.PHONY: doc-builds doc-prereq
+doc-builds: doc-prereq
+ (cd $(CURRENT_BUILD) && $(MAKE) doxygen-doc)
+doc-prereq:
+ (cd $(CURRENT_BUILD) && for dir in `find . -name Makefile | xargs grep -l BUILT_SOURCES`; do (cd `dirname "$$dir"`; (cat Makefile; echo 'doc-prereq: $$(BUILT_SOURCES)') | make -f- doc-prereq); done)
+
# any other target than the default doesn't do the extra stuff above
%:
(cd $(CURRENT_BUILD) && $(MAKE) $@)
DX_PDF_FEATURE(OFF)
DX_PS_FEATURE(OFF)
-DX_DOT_FEATURE(OFF)
+DX_DOT_FEATURE(ON)
DX_INIT_DOXYGEN($PACKAGE_NAME, config/doxygen.cfg, $srcdir/doc)
AC_ARG_VAR(CXXTEST, [path to CxxTest installation])
* Get a particular attribute on a particular node.
*
* @param nv the node about which to inquire
- *
- * @param const AttrKind& the attribute kind to get
- *
+ * @param attr the attribute kind to get
* @return the attribute value, if set, or a default-constructed
* AttrKind::value_type if not.
*/
template <class AttrKind>
typename AttrKind::value_type getAttribute(NodeValue* nv,
- const AttrKind&) const;
+ const AttrKind& attr) const;
/**
* Determine if a particular attribute exists for a particular node.
*
* @param nv the node about which to inquire
- *
- * @param const AttrKind& the attribute kind to inquire about
- *
+ * @param attr the attribute kind to inquire about
* @return true if the given node has the given attribute
*/
template <class AttrKind>
bool hasAttribute(NodeValue* nv,
- const AttrKind&) const;
+ const AttrKind& attr) const;
/**
* Determine if a particular attribute exists for a particular node,
* and get it if it does.
*
* @param nv the node about which to inquire
- *
- * @param const AttrKind& the attribute kind to inquire about
- *
+ * @param attr the attribute kind to inquire about
* @param ret a pointer to a return value, set in case the node has
* the attribute
- *
* @return true if the given node has the given attribute
*/
template <class AttrKind>
bool getAttribute(NodeValue* nv,
- const AttrKind&,
+ const AttrKind& attr,
typename AttrKind::value_type& ret) const;
/**
* Set a particular attribute on a particular node.
*
* @param nv the node for which to set the attribute
- *
- * @param const AttrKind& the attribute kind to set
- *
- * @param ret a pointer to a return value, set in case the node has
+ * @param attr the attribute kind to set
+ * @param value a pointer to a return value, set in case the node has
* the attribute
- *
* @return true if the given node has the given attribute
*/
template <class AttrKind>
void setAttribute(NodeValue* nv,
- const AttrKind&,
+ const AttrKind& attr,
const typename AttrKind::value_type& value);
/**
}
void DeclarationScope::bindType(const std::string& name,
- const vector<Type>& params,
+ const std::vector<Type>& params,
Type t) throw() {
if(Debug.isOn("sort")) {
Debug("sort") << "bindType(" << name << ", [";
}
Type DeclarationScope::lookupType(const std::string& name,
- const vector<Type>& params) const throw(AssertionException) {
+ const std::vector<Type>& params) const throw(AssertionException) {
pair<vector<Type>, Type> p = (*d_typeMap->find(name)).second;
Assert(p.first.size() == params.size(),
"type constructor arity is wrong: "
/**
* Bind an expression to a name in the current scope level. If
- * <code>name</code> is already bound in the current level, then the
- * binding is replaced. If <code>name</code> is bound in a previous
- * level, then the binding is "covered" by this one until the
- * current scope is popped.
+ * <code>name</code> is already bound to an expression in the current
+ * level, then the binding is replaced. If <code>name</code> is bound
+ * in a previous level, then the binding is "covered" by this one
+ * until the current scope is popped.
*
* @param name an identifier
* @param obj the expression to bind to <code>name</code>
void bind(const std::string& name, Expr obj) throw();
/**
- * Bind a type to a name in the current scope. If <code>name</code>
- * is already bound to a type in the current level, then the binding
- * is replaced. If <code>name</code> is bound in a previous level,
- * then the binding is "covered" by this one until the current scope
- * is popped.
+ * Bind a function body to a name in the current scope. If
+ * <code>name</code> is already bound to an expression in the current
+ * level, then the binding is replaced. If <code>name</code> is bound
+ * in a previous level, then the binding is "covered" by this one
+ * until the current scope is popped. Same as bind() but registers
+ * this as a function (so that isBoundDefinedFunction() returns true).
*
* @param name an identifier
- * @param t the type to bind to <code>name</code>
+ * @param obj the expression to bind to <code>name</code>
*/
void bindDefinedFunction(const std::string& name, Expr obj) throw();
* one until the current scope is popped.
*
* @param name an identifier
+ * @param params the parameters to the type
* @param t the type to bind to <code>name</code>
*/
void bindType(const std::string& name,
// compiler directs the user to the template file instead of the
// generated one. We don't want the user to modify the generated one,
// since it'll get overwritten on a later build.
-#line 30 "${template}"
+#line 31 "${template}"
using namespace std;
using namespace CVC4::context;
* type checking is not requested, getType() will do the minimum
* amount of checking required to return a valid result.
*
- * @param n the Expr for which we want a type
+ * @param e the Expr for which we want a type
* @param check whether we should check the type as we compute it
* (default: false)
*/
/**
* Make a unary expression of a given kind (NOT, BVNOT, ...).
+ * @param kind the kind of expression
* @param child1 kind the kind of expression
* @return the expression
*/
* suitably-sized chunks, taking advantage of the associativity of
* <code>kind</code>. For example, if kind <code>FOO</code> has max arity
* 2, then calling <code>mkAssociative(FOO,a,b,c)</code> will return
- * <code>(FOO (FOO a b) c)</code> or code>(FOO a (FOO b c))</code>.
+ * <code>(FOO (FOO a b) c)</code> or <code>(FOO a (FOO b c))</code>.
* The order of the arguments will be preserved in a left-to-right
* traversal of the resulting tree.
*/
/**
* Outputs the string representation of the expression to the stream.
- * @param out the output stream
- */
- void toStream(std::ostream& out, int depth = -1, bool types = false,
- OutputLanguage lang = language::output::LANG_AST) const;
+ *
+ * @param out the stream to serialize this expression to
+ * @param toDepth the depth to which to print this expression, or -1
+ * to print it fully
+ * @param types set to true to ascribe types to the output
+ * expressions (might break language compliance, but good for
+ * debugging expressions)
+ * @param language the language in which to output
+ */
+ void toStream(std::ostream& out, int toDepth = -1, bool types = false,
+ OutputLanguage language = language::output::LANG_AST) const;
/**
* Check if this is a null expression.
namespace CVC4 {
TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
- string message) :
+ std::string message) :
Exception(message),
d_node(new Node(node)) {
}
* PLUSes don't exist---begin(PLUS) will give an iterator over the
* children if the node's a PLUS node, otherwise give an iterator
* over the node itself, as if it were a unary PLUS.
- * @param the kind to match
+ * @param kind the kind to match
* @return the kinded_iterator iterating over this Node (if its kind
* is not the passed kind) or its children
*/
* don't exist---begin(PLUS) will give an iterator over the children
* if the node's a PLUS node, otherwise give an iterator over the
* node itself, as if it were a unary PLUS.
- * @param the kind to match
+ * @param kind the kind to match
* @return the kinded_iterator pointing off-the-end of this Node (if
* its kind is not the passed kind) or off-the-end of its children
*/
* PLUSes don't exist---begin(PLUS) will give an iterator over the
* children if the node's a PLUS node, otherwise give an iterator
* over the node itself, as if it were a unary PLUS.
- * @param the kind to match
+ * @param kind the kind to match
* @return the kinded_iterator iterating over this Node (if its kind
* is not the passed kind) or its children
*/
* don't exist---begin(PLUS) will give an iterator over the children
* if the node's a PLUS node, otherwise give an iterator over the
* node itself, as if it were a unary PLUS.
- * @param the kind to match
+ * @param kind the kind to match
* @return the kinded_iterator pointing off-the-end of this Node (if
* its kind is not the passed kind) or off-the-end of its children
*/
/**
* Converst this node into a string representation and sends it to the
* given stream
+ *
* @param out the stream to serialize this node to
+ * @param toDepth the depth to which to print this expression, or -1 to
+ * print it fully
+ * @param types set to true to ascribe types to the output expressions
+ * (might break language compliance, but good for debugging expressions)
+ * @param language the language in which to output
*/
inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
OutputLanguage language = language::output::LANG_AST) const {
/**
* Very basic pretty printer for Node.
- * @param o output stream to print to.
+ * @param out output stream to print to.
* @param indent number of spaces to indent the formula by.
*/
inline void printAst(std::ostream& out, int indent = 0) const;
/**
* Serializes a given node to the given stream.
* @param out the output stream to use
- * @param node the node to output to the stream
- * @return the changed stream.
+ * @param n the node to output to the stream
+ * @return the stream
*/
inline std::ostream& operator<<(std::ostream& out, TNode n) {
n.toStream(out,
*replacement.d_typeNode));
}
-Type Type::substitute(const vector<Type>& types,
- const vector<Type>& replacements) const {
+Type Type::substitute(const std::vector<Type>& types,
+ const std::vector<Type>& replacements) const {
NodeManagerScope nms(d_nodeManager);
vector<TypeNode> typesNodes, replacementsNodes;
replacementsNodes.end()));
}
-void Type::toStream(ostream& out) const {
+void Type::toStream(std::ostream& out) const {
NodeManagerScope nms(d_nodeManager);
out << *d_typeNode;
return;
return d_typeNode->getAttribute(expr::SortArityAttr());
}
-SortType SortConstructorType::instantiate(const vector<Type>& params) const {
+SortType SortConstructorType::instantiate(const std::vector<Type>& params) const {
NodeManagerScope nms(d_nodeManager);
vector<TypeNode> paramsNodes;
for(vector<Type>::const_iterator i = params.begin(),
* Assignment operator for nodes, copies the relevant information from node
* to this node.
*
- * @param node the node to copy
+ * @param typeNode the node to copy
* @return reference to this node
*/
TypeNode& operator=(const TypeNode& typeNode);
* We compare by expression ids so, keeping things deterministic and having
* that subexpressions have to be smaller than the enclosing expressions.
*
- * @param node the node to compare to
+ * @param typeNode the node to compare to
* @return true if this expression is smaller
*/
inline bool operator<(const TypeNode& typeNode) const {
* given stream
*
* @param out the stream to serialize this node to
+ * @param toDepth the depth to which to print this expression, or -1 to
+ * print it fully
+ * @param types set to true to ascribe types to the output expressions
+ * (might break language compliance, but good for debugging expressions)
+ * @param language the language in which to output
*/
inline void toStream(std::ostream& out, int toDepth = -1, bool types = false,
OutputLanguage language = language::output::LANG_AST) const {
/**
* Very basic pretty printer for Node.
*
- * @param o output stream to print to.
+ * @param out output stream to print to.
* @param indent number of spaces to indent the formula by.
*/
void printAst(std::ostream& out, int indent = 0) const;
* Indents the given stream a given amount of spaces.
*
* @param out the stream to indent
- * @param indent the numer of spaces
+ * @param indent the number of spaces
*/
static void indent(std::ostream& out, int indent) {
for(int i = 0; i < indent; i++) {
* Serializes a given node to the given stream.
*
* @param out the output stream to use
- * @param node the node to output to the stream
- * @return the changed stream.
+ * @param n the node to output to the stream
+ * @return the stream
*/
inline std::ostream& operator<<(std::ostream& out, const TypeNode& n) {
n.toStream(out,
/** Create a file input.
*
- * @param filename the path of the file to read
+ * @param name the path of the file to read
* @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
* input will use the standard ANTLR3 I/O implementation.
*/
*/
CvcInput(AntlrInputStream& inputStream);
- /** Create a string input.
- *
- * @param exprManager the manager to use when building expressions from the input
- * @param input the string to read
- * @param name the "filename" to use when reporting errors
- */
-/*
- CvcInput(ExprManager* exprManager, const std::string& input,
- const std::string& name);
-*/
-
- /* Destructor. Frees the lexer and the parser. */
+ /** Destructor. Frees the lexer and the parser. */
~CvcInput();
protected:
Expr getSymbol(const std::string& var_name, SymbolType type);
protected:
- /** Create a parser state. NOTE: The parser takes "ownership" of the given
+ /**
+ * Create a parser state. NOTE: The parser takes "ownership" of the given
* input and will delete it on destruction.
*
* @param exprManager the expression manager to use when creating expressions
* @param input the parser input
+ * @param strictMode whether to incorporate strict(er) compliance checks
*/
Parser(ExprManager* exprManager, Input* input, bool strictMode = false);
/**
* Returns a function, given a name.
*
- * @param var_name the name of the variable
+ * @param name the name of the variable
* @return the variable expression
*/
Expr getFunction(const std::string& name);
/**
* Returns a sort, given a name.
+ * @param sort_name the name to look up
*/
Type getSort(const std::string& sort_name);
* @param kind the built-in operator to check
* @param numArgs the number of actual arguments
* @throws ParserException if the parser mode is strict and the
- * operator <code>kind</kind> has not been enabled
+ * operator <code>kind</code> has not been enabled
*/
void checkOperator(Kind kind, unsigned int numArgs) throw (ParserException);
addOperator(kind::GEQ);
}
-/**
- * Add theory symbols to the parser state.
- *
- * @param parser the CVC4 Parser object
- * @param theory the theory to open (e.g., Core, Ints)
- */
void Smt::addTheory(Theory theory) {
switch(theory) {
case THEORY_ARRAYS:
addOperator(kind::APPLY_UF);
}
-/**
- * Sets the logic for the current benchmark. Declares any logic and theory symbols.
- *
- * @param parser the CVC4 Parser object
- * @param name the name of the logic (e.g., QF_UF, AUFLIA)
- */
void Smt::setLogic(const std::string& name) {
d_logicSet = true;
d_logic = toLogic(name);
case QF_NIA:
addTheory(THEORY_INTS);
break;
-
+
case QF_LRA:
case QF_RDL:
addTheory(THEORY_REALS);
/**
* Add theory symbols to the parser state.
*
- * @param parser the CVC4 Parser object
* @param theory the theory to open (e.g., Core, Ints)
*/
void addTheory(Theory theory);
/**
* Sets the logic for the current benchmark. Declares any logic and theory symbols.
*
- * @param parser the CVC4 Parser object
* @param name the name of the logic (e.g., QF_UF, AUFLIA)
*/
void setLogic(const std::string& name);
*/
SmtInput(AntlrInputStream& inputStream);
- /**
- * Create a string input.
- *
- * @param exprManager the manager to use when building expressions from the input
- * @param input the string to read
- * @param name the "filename" to use when reporting errors
- */
-// SmtInput(ExprManager* exprManager, const std::string& input, const std::string& name);
-
/** Destructor. Frees the lexer and the parser. */
~SmtInput();
addOperator(kind::GEQ);
}
-/**
- * Add theory symbols to the parser state.
- *
- * @param parser the CVC4 Parser object
- * @param theory the theory to open (e.g., Core, Ints)
- */
void Smt2::addTheory(Theory theory) {
switch(theory) {
case THEORY_CORE:
return d_logicSet;
}
-/**
- * Sets the logic for the current benchmark. Declares any logic and
- * theory symbols.
- *
- * @param parser the CVC4 Parser object
- * @param name the name of the logic (e.g., QF_UF, AUFLIA)
- */
void Smt2::setLogic(const std::string& name) {
d_logicSet = true;
d_logic = Smt::toLogic(name);
/**
* Add theory symbols to the parser state.
*
- * @param parser the CVC4 Parser object
* @param theory the theory to open (e.g., Core, Ints)
*/
void addTheory(Theory theory);
* Sets the logic for the current benchmark. Declares any logic and
* theory symbols.
*
- * @param parser the CVC4 Parser object
* @param name the name of the logic (e.g., QF_UF, AUFLIA)
*/
void setLogic(const std::string& name);
*/
Smt2Input(AntlrInputStream& inputStream);
- /**
- * Create a string input.
- *
- * @param exprManager the manager to use when building expressions
- * from the input
- * @param input the string to read
- * @param name the "filename" to use when reporting errors
- */
-// Smt2Input(ExprManager* exprManager, const std::string& input, const std::string& name);
-
/** Destructor. Frees the lexer and the parser. */
virtual ~Smt2Input();
return d_translationCache.find(n) != d_translationCache.end();
}
-SatLiteral CnfStream::lookupInCache(TNode n) const {
- Assert(isCached(n), "Node is not in CNF translation cache");
- return d_translationCache.find(n)->second;
+SatLiteral CnfStream::lookupInCache(TNode node) const {
+ Assert(isCached(node), "Node is not in CNF translation cache");
+ return d_translationCache.find(node)->second;
}
void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
#include "cvc4_private.h"
-#ifndef __CVC4__CNF_STREAM_H
-#define __CVC4__CNF_STREAM_H
+#ifndef __CVC4__PROP__CNF_STREAM_H
+#define __CVC4__PROP__CNF_STREAM_H
#include "expr/node.h"
#include "prop/sat.h"
namespace CVC4 {
namespace prop {
+
class PropEngine;
/**
/**
* Asserts the given clause to the sat solver.
+ * @param node the node giving rise to this clause
* @param clause the clasue to assert
*/
void assertClause(TNode node, SatClause& clause);
/**
* Asserts the unit clause to the sat solver.
+ * @param node the node giving rise to this clause
* @param a the unit literal of the clause
*/
void assertClause(TNode node, SatLiteral a);
/**
* Asserts the binary clause to the sat solver.
+ * @param node the node giving rise to this clause
* @param a the first literal in the clause
* @param b the second literal in the clause
*/
/**
* Asserts the ternary clause to the sat solver.
+ * @param node the node giving rise to this clause
* @param a the first literal in the clause
* @param b the second literal in the clause
* @param c the thirs literal in the clause
void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
/**
- * Returns true if the node has been cashed in the translation cache.
+ * Returns true if the node has been cached in the translation cache.
* @param node the node
* @return true if the node has been cached
*/
bool isCached(TNode node) const;
/**
- * Returns the cashed literal corresponding to the given node.
+ * Returns the cached literal corresponding to the given node.
* @param node the node to lookup
* @return returns the corresponding literal
*/
- SatLiteral lookupInCache(TNode n) const;
+ SatLiteral lookupInCache(TNode node) const;
/**
* Caches the pair of the node and the literal corresponding to the
* translation.
- * @param node node
- * @param lit
+ * @param node the node
+ * @param lit the literal
*/
void cacheTranslation(TNode node, SatLiteral lit);
/**
- * Acquires a new variable from the SAT solver to represent the node and
- * inserts the necessary data it into the mapping tables.
+ * Acquires a new variable from the SAT solver to represent the node
+ * and inserts the necessary data it into the mapping tables.
* @param node a formula
- * @param theoryLiteral is this literal a theory literal (i.e. theory to be
- * informed when set to true/false
+ * @param theoryLiteral whether this literal a theory literal (and
+ * therefore the theory is to be informed when set to true/false)
* @return the literal corresponding to the formula
*/
SatLiteral newLiteral(TNode node, bool theoryLiteral = false);
public:
/**
- * Constructs a CnfStream that sends constructs an equi-satisfiable set of clauses
- * and sends them to the given sat solver.
+ * Constructs a CnfStream that sends constructs an equi-satisfiable
+ * set of clauses and sends them to the given sat solver.
* @param satSolver the sat solver to use
*/
CnfStream(SatInputInterface* satSolver);
/**
* Converts and asserts a formula.
* @param node node to convert and assert
- * @param whether the sat solver can choose to remove the clauses
+ * @param lemma whether the sat solver can choose to remove the clauses
* @param negated wheather we are asserting the node negated
*/
virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0;
const NodeCache& getNodeCache() const {
return d_nodeCache;
}
+
};/* class CnfStream */
+
/**
* TseitinCnfStream is based on the following recursive algorithm
* http://people.inf.ethz.ch/daniekro/classes/251-0247-00/f2007/readings/Tseitin70.pdf
*/
SatLiteral toCNF(TNode node, bool negated = false);
-}; /* class TseitinCnfStream */
+};/* class TseitinCnfStream */
+
-}/* prop namespace */
+}/* CVC4::prop namespace */
}/* CVC4 namespace */
-#endif /* __CVC4__CNF_STREAM_H */
+#endif /* __CVC4__PROP__CNF_STREAM_H */
delete d_decisionEngine;
}
-void SmtEngine::setInfo(const string& key, const SExpr& value)
+void SmtEngine::setInfo(const std::string& key, const SExpr& value)
throw(BadOptionException) {
Debug("smt") << "SMT setInfo(" << key << ", " << value << ")" << endl;
if(key == ":name" ||
throw BadOptionException();
}
-SExpr SmtEngine::getInfo(const string& key) const
+SExpr SmtEngine::getInfo(const std::string& key) const
throw(BadOptionException) {
Debug("smt") << "SMT getInfo(" << key << ")" << endl;
if(key == ":all-statistics") {
}
}
-void SmtEngine::setOption(const string& key, const SExpr& value)
+void SmtEngine::setOption(const std::string& key, const SExpr& value)
throw(BadOptionException) {
Debug("smt") << "SMT setOption(" << key << ", " << value << ")" << endl;
if(key == ":print-success") {
}
}
-SExpr SmtEngine::getOption(const string& key) const
+SExpr SmtEngine::getOption(const std::string& key) const
throw(BadOptionException) {
Debug("smt") << "SMT getOption(" << key << ")" << endl;
if(key == ":print-success") {
}
void SmtEngine::defineFunction(Expr func,
- const vector<Expr>& formals,
+ const std::vector<Expr>& formals,
Expr formula) {
Debug("smt") << "SMT defineFunction(" << func << ")" << endl;
NodeManagerScope nms(d_nodeManager);
return Monomial::mkMonomial(newConstant, newVL);
}
-vector<Monomial> Monomial::sumLikeTerms(const vector<Monomial> & monos) {
+vector<Monomial> Monomial::sumLikeTerms(const std::vector<Monomial> & monos) {
Assert(isSorted(monos));
Debug("blah") << "start sumLikeTerms" << std::endl;
Debug("normal-form") << getNode() << std::endl;
}
-void Monomial::printList(const vector<Monomial>& list) {
+void Monomial::printList(const std::vector<Monomial>& list) {
for(vector<Monomial>::const_iterator i = list.begin(), end = list.end(); i != end; ++i) {
const Monomial& m =*i;
m.print();
return true;
}
-void RowVector::zip(const vector< ArithVar >& variables,
- const vector< Rational >& coefficients,
+void RowVector::zip(const std::vector< ArithVar >& variables,
+ const std::vector< Rational >& coefficients,
VarCoeffArray& output){
Assert(coefficients.size() == variables.size() );
}
}
-RowVector::RowVector(const vector< ArithVar >& variables,
- const vector< Rational >& coefficients,
+RowVector::RowVector(const std::vector< ArithVar >& variables,
+ const std::vector< Rational >& coefficients,
std::vector<uint32_t>& counts):
d_rowCount(counts)
{
}
ReducedRowVector::ReducedRowVector(ArithVar basic,
- const vector<ArithVar>& variables,
- const vector<Rational>& coefficients,
+ const
std::vector<ArithVar>& variables,
+ const std::vector<Rational>& coefficients,
std::vector<uint32_t>& count):
RowVector(variables, coefficients, count), d_basic(basic){
}
-void SharedTermManager::collectExplanations(SharedData* pData, set<Node>& s) const {
+void SharedTermManager::collectExplanations(SharedData* pData, std::set<Node>& s) const {
Theory* expTh = pData->getExplainingTheory();
if(expTh == NULL) {
// This equality is directly from SAT, no need to ask a theory for an explanation
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief .
+ ** \brief A decision engine for CVC4
**
+ ** A decision engine for CVC4.
**/
#include "util/decision_engine.h"
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief A decision engine for CVC4.
+ ** \brief A decision engine for CVC4
**
** A decision engine for CVC4.
**/
return optionsDescription;
}
-void Options::printUsage(const string msg, std::ostream& out) {
+void Options::printUsage(const std::string msg, std::ostream& out) {
out << msg << optionsDescription << endl << flush;
// printf(usage + options.getDescription(), options.binary_name.c_str());
// printf(usage, binary_name.c_str());
}
}
-void DebugC::printf(string tag, const char* fmt, ...) {
+void DebugC::printf(std::string tag, const char* fmt, ...) {
if(d_tags.find(tag) != d_tags.end()) {
// chop off output after 1024 bytes
char buf[1024];
}
}
-void TraceC::printf(string tag, const char* fmt, ...) {
+void TraceC::printf(std::string tag, const char* fmt, ...) {
if(d_tags.find(tag) != d_tags.end()) {
// chop off output after 1024 bytes
char buf[1024];
/* Computes a rational given a decimal string. The rational
* version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
*/
-Rational Rational::fromDecimal(const string& dec) {
+Rational Rational::fromDecimal(const std::string& dec) {
// Find the decimal point, if there is one
string::size_type i( dec.find(".") );
if( i != string::npos ) {
/* Computes a rational given a decimal string. The rational
* version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
*/
-Rational Rational::fromDecimal(const string& dec) {
+Rational Rational::fromDecimal(const std::string& dec) {
// Find the decimal point, if there is one
string::size_type i( dec.find(".") );
if( i != string::npos ) {
namespace CVC4 {
-Result::Result(const string& instr) :
+Result::Result(const std::string& instr) :
d_sat(SAT_UNKNOWN),
d_validity(VALIDITY_UNKNOWN),
d_which(TYPE_NONE),
projects / cvc5.git / commitdiff