I ensured that I didn't change any code with this commit, and even tested on the cluster to be doubly sure:
http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=4655&reference_id=4646&p=0
--- /dev/null
+#!/usr/bin/perl -0777
+
+my $debug = 0;
+
+$_ = <>;
+my $comments = "";
+my $code = "";
+
+# ignore strings and comments appearing in preprocessor directives
+s/^#.*//mg;
+
+for(;;) {
+ s,^([^"/]+),,;
+ $code .= "$1\n";
+
+ if(m,^([^"]*)"",) {
+ s,^([^"]*)"",,s;
+ $code .= "$1\n";
+ next;
+ }
+ if(m,^([^"]*)"([^"]*)",) {
+ s,^([^"]*)"(([^\\"]*?([^\\"]|(\\.)))+)",,s;
+ print STDERR "quote: $2\n" if $debug;
+ $code .= "$1\n";
+ $comments .= "$2\n";
+ next;
+ }
+ if(m,/\*.*?\*/,) {
+ s,/\*(.*?)\*/,,s;
+ print STDERR "c-style comment: $1\n" if $debug;
+ $comments .= "$1\n";
+ print STDERR "REMAINDER:\n===========================\n$_\n=========================\n" if $debug;
+ next;
+ }
+ if(m,//,) {
+ s,//([^\n]*),,s;
+ print STDERR "c++-style comment: $1\n" if $debug;
+ $comments .= "$1\n";
+ print STDERR "REMAINDER:\n===========================\n$_\n=========================\n" if $debug;
+ next;
+ }
+ last;
+}
+
+$code .= "$_\n";
+$code =~ s,\W+,\n,g;
+$code =~ s,^,@,gm;
+print "$code\n";
+
+$comments =~ s,^,^,gm;
+print "$comments\n";
+
--- /dev/null
+#!/bin/bash
+
+dir="$(dirname "$0")"
+
+find src \( -name '*.cpp' -o -name '*.h' \) \! -path 'src/prop/minisat/*' \! -path 'src/prop/bvminisat/*' \! -path 'src/prop/cryptominisat/*' \! -path 'src/parser/*/generated/*' |
+ while read f; do
+ misspelled_words=`
+ $dir/extract-strings-and-comments $f |
+ ispell -a -W 3 2>/dev/null |
+ tail -n +2 |
+ while read s; do
+ case "$s" in
+ \**|\+*|-*) ;;
+ \&*|\#*|\?*) echo "$s" | awk '{print$2}';;
+# *) test -n "$s" && echo "UNKNOWN : $s";;
+ esac
+ done | sort -fu | sed 's,^, ,'`
+ if [ -n "$misspelled_words" ]; then
+ echo "$f"
+ echo "$misspelled_words"
+ fi
+ done
class Theory$camel : public Theory {
public:
- /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+ /** Constructs a new instance of Theory$camel w.r.t. the provided context.*/
Theory$camel(context::Context* c,
context::UserContext* u,
OutputChannel& out,
/********************* */
-/*! \file cdmap_forward.h
+/*! \file cdhashmap_forward.h
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
** public header context.
**
** For CDMap<> in particular, it's difficult to forward-declare it
- ** yourself, becase it has a default template argument.
+ ** yourself, because it has a default template argument.
**/
#include "cvc4_public.h"
/********************* */
-/*! \file cdset.h
+/*! \file cdhashset.h
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file cdset_forward.h
+/*! \file cdhashset_forward.h
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
** public header context.
**
** For CDSet<> in particular, it's difficult to forward-declare it
- ** yourself, becase it has a default template argument.
+ ** yourself, because it has a default template argument.
**/
#include "cvc4_public.h"
*
* Explanation:
* If ContextMemoryAllocator is used and d_list grows at a deeper context level
- * the reallocated will be reallocated in a context memory regaion that can be
- * detroyed on pop. To support this, a full copy of d_list would have to be made.
+ * the reallocated will be reallocated in a context memory region that can be
+ * destroyed on pop. To support this, a full copy of d_list would have to be made.
* As this is unacceptable for performance in other situations, we do not do
* this.
*/
-/**
- * This implements a CDMaybe.
- * This has either been set in the context or it has not.
- * T must have a default constructor and support assignment.
- */
+/********************* */
+/*! \file cdmaybe.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 A context-dependent "maybe" template type
+ **
+ ** This implements a CDMaybe.
+ ** This has either been set in the context or it has not.
+ ** Template parameter T must have a default constructor and support
+ ** assignment.
+ **/
#include "cvc4_private.h"
d_flag.set(true);
}
-}; /* class CDRaised */
+};/* class CDRaised */
template <class T>
class CDMaybe {
Assert(isSet());
return d_data.get().second;
}
-}; /* class CDMaybe<T> */
+};/* class CDMaybe<T> */
}/* CVC4::context namespace */
}/* CVC4 namespace */
/********************* */
-/*! \file justification_heuristic.h
+/*! \file justification_heuristic.cpp
** \verbatim
** Original author: kshitij
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): dejan
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/* Good luck, hope you can get what you want */
Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
- "invariant voilated");
+ "invariant violated");
/* What type of node is this */
Kind k = node.getKind();
class GiveUpException : public Exception {
public:
GiveUpException() :
- Exception("justification hueristic: giving up") {
+ Exception("justification heuristic: giving up") {
}
};/* class GiveUpException */
}
/**
- * Do all the hardwork.
+ * Do all the hard work.
* @param findFirst returns
*/
bool findSplitterRec(TNode node, SatValue value, SatLiteral* litDecision);
/********************* */
-/*! \file relevancy.h
+/*! \file relevancy.cpp
** \verbatim
** Original author: kshitij
** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2012 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/* Good luck, hope you can get what you want */
Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN,
- "invariant voilated");
+ "invariant violated");
/* What type of node is this */
Kind k = node.getKind();
if (d_exprStatisticsVars[type] == NULL) { \
stringstream statName; \
if (type == LAST_TYPE) { \
- statName << "expr::ExprManager::VARIABLE:Parametrized type"; \
+ statName << "expr::ExprManager::VARIABLE:Parameterized type"; \
} else { \
statName << "expr::ExprManager::VARIABLE:" << type; \
} \
Assert(getKind() == kind::UNDEFINED_KIND || d_nv->d_id == 0,
"can't redefine the Kind of a NodeBuilder");
Assert(d_nv->d_id == 0,
- "interal inconsistency with NodeBuilder: d_id != 0");
+ "internal inconsistency with NodeBuilder: d_id != 0");
AssertArgument(k != kind::UNDEFINED_KIND &&
k != kind::NULL_EXPR &&
k < kind::LAST_KIND,
/** Make a new (anonymous) sort of arity 0. */
inline TypeNode mkSort();
- /** Make a new sort with the given name and arity. */
+ /** Make a new sort with the given name of arity 0. */
inline TypeNode mkSort(const std::string& name);
- /** Make a new sort with the given name and arity. */
+ /** Make a new sort by parameterizing the given sort constructor. */
inline TypeNode mkSort(TypeNode constructor,
const std::vector<TypeNode>& children);
/********************* */
-/*! \file pickle.h
+/*! \file pickler.h
** \verbatim
- ** Original author: kshitij
- ** Major contributors: taking, mdeters
+ ** Original author: mdeters
+ ** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief Driver for (sequential) CVC4 executable
+ ** \brief Driver for (sequential) CVC4 executable (cvc4)
**
- ** Driver for (sequential) CVC4 executable.
+ ** Driver for (sequential) CVC4 executable (cvc4).
**/
#include <cstdlib>
+/********************* */
+/*! \file driver_portfolio.cpp
+ ** \verbatim
+ ** Original author: kshitij
+ ** Major contributors: taking, mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 Driver for portfolio CVC4 executable (pcvc4)
+ **
+ ** Driver for portfolio CVC4 executable (pcvc4).
+ **/
+
#include <cstdio>
#include <cstdlib>
#include <iostream>
}
} /* end of infinite while */
- Trace("interrupt") << "sharing thread interuppted, interrupting all smtEngines" << std::endl;
+ Trace("interrupt") << "sharing thread interrupted, interrupting all smtEngines" << std::endl;
for(int t = 0; t < numThreads; ++t) {
- Trace("interrupt") << "Interuppting thread #" << t << std::endl;
+ Trace("interrupt") << "Interrupting thread #" << t << std::endl;
try{
smts[t]->interrupt();
}catch(ModalException &e){
}
}
- Trace("sharing") << "sharing: Interuppted, exiting." << std::endl;
+ Trace("sharing") << "sharing: Interrupted, exiting." << std::endl;
}
} else {
// literal appears negative in the first clause
if( !clause1.count(~var) || !clause2.count(var)) {
- Debug("proof:sat") << "proof:resolve: Mising literal ";
+ Debug("proof:sat") << "proof:resolve: Missing literal ";
printLit(var);
Debug("proof:sat") << endl;
return false;
/**
* Transforms the node into CNF recursively.
* @param node the formula to transform
- * @param negated wheather the literal is negated
+ * @param negated whether the literal is negated
* @return the literal representing the root of the formula
*/
SatLiteral toCNF(TNode node, bool negated = false);
/********************* */
-/*! \file sat_module.h
+/*! \file sat_solver.h
** \verbatim
** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file sat_solver_factory.h
+/*! \file sat_solver_factory.cpp
** \verbatim
- ** Original author: lianah
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Original author: dejan
+ ** Major contributors: taking
+ ** Minor contributors (to current version): lianah
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file sat_solver_registry.h
+/*! \file sat_solver_registry.cpp
** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): barrett, cconway
+ ** Original author: dejan
+ ** Major contributors: none
+ ** 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)
+ ** Copyright (c) 2009-2012 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
namespace prop {
/**
- * Interface for SAT solver constructors. Solvers should declare an instantiatiation of the
+ * Interface for SAT solver constructors. Solvers should declare an instantiation of the
* SatSolverConstructor interface below.
*/
class SatSolverConstructorInterface {
/**
* Register a SAT solver with the registry. The Constructor type should be a subclass
- * of the SatSolverConstrutor.
+ * of the SatSolverConstructor.
*/
template <typename Constructor>
size_t registerSolver(const char* id) {
/********************* */
-/*! \file cnf_stream.h
+/*! \file sat_solver_types.h
** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters, dejan
- ** Minor contributors (to current version): barrett, cconway, kshitij
+ ** Original author: dejan
+ ** Major contributors: none
+ ** Minor contributors (to current version): kshitij
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file sat.cpp
+/*! \file theory_proxy.cpp
** \verbatim
** Original author: cconway
- ** Major contributors: dejan, taking, mdeters
- ** Minor contributors (to current version): kshitij
+ ** Major contributors: lianah, dejan, kshitij, mdeters
+ ** Minor contributors (to current version): barrett, taking
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
SatLiteral TheoryProxy::getNextDecisionRequest(bool &stopSearch) {
TNode n = d_theoryEngine->getNextDecisionRequest();
- if(not n.isNull())
+ if(not n.isNull()) {
return d_cnfStream->getLiteral(n);
-
+ }
+
// If theory doesn't give us a deicsion ask the decision engine. It
- // may return in undefSatLiteral in which case the sat solver figure
- // it out something
+ // may return in undefSatLiteral in which case the sat solver uses
+ // whatever default heuristic it has.
Assert(d_decisionEngine != NULL);
Assert(stopSearch != true);
SatLiteral ret = d_decisionEngine->getNext(stopSearch);
/********************* */
-/*! \file sat.h
+/*! \file theory_proxy.h
** \verbatim
** Original author: mdeters
- ** Major contributors: taking, cconway, dejan
- ** Minor contributors (to current version): barrett, kshitij
+ ** Major contributors: kshitij, lianah, dejan
+ ** Minor contributors (to current version): taking, cconway
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
* to determine which to dequeue first.
*
* - Variable Order Queue
- * This mode uses the variable order to determine which ArithVar is deuqued first.
+ * This mode uses the variable order to determine which ArithVar is dequeued first.
*
* The transitions between the modes of operation are:
* Collection => Difference Queue
/**
* Priority Queue of the basic variables that may be inconsistent.
* Variables are ordered according to which violates its bound the most.
- * This is a heuristic and makes no guarentees to terminate!
+ * This is a heuristic and makes no guarantees to terminate!
* This heuristic comes from Alberto Griggio's thesis.
*/
DifferenceArray d_diffQueue;
}
}
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
void miplibTrick(TNode var, std::set<Rational>& values, NodeBuilder<>& learned);
- /** These fields are designed to be accessable to ArithStaticLearner methods. */
+ /** These fields are designed to be accessible to ArithStaticLearner methods. */
class Statistics {
public:
IntStat d_iteMinMaxApplications;
return NodeManager::currentNM()->mkNode(kind::AND, out);
}
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
-
-
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__ARITH_UTILITIES_H */
virtual void operator()(Node n) = 0;
};
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#endif /* __CVC4__THEORY__ARITH__ARITHVAR_H */
+/********************* */
+/*! \file congruence_manager.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "theory/arith/congruence_manager.h"
#include "theory/arith/constraint.h"
-
+/********************* */
+/*! \file congruence_manager.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: dejan
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "cvc4_private.h"
*/
//void assertLiteral(bool eq, ArithVar s, TNode reason);
- /** This sends a shared term to the uninterpretted equality engine. */
+ /** This sends a shared term to the uninterpreted equality engine. */
//void addAssertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
void assertionToEqualityEngine(bool eq, ArithVar s, TNode reason);
~Statistics();
} d_statistics;
-};/* class CongruenceManager */
+};/* class ArithCongruenceManager */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
-
-
+/********************* */
+/*! \file constraint.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "cvc4_private.h"
#include "theory/arith/constraint.h"
}
}
-}/* arith namespace */
-}/* theory namespace */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
}/* CVC4 namespace */
*
* This is not context dependent, but may be set once.
*
- * This must be set if the constraint canbePropgated().
+ * This must be set if the constraint canBePropagated().
* This must be set if the constraint assertedToTheTheory().
* Otherwise, this may be null().
*/
/**
* True if the equality has been split.
- * Only meaningful if ContraintType == Equality.
+ * Only meaningful if ConstraintType == Equality.
*
* User Context Dependent.
* This is initially false.
/**
* Returns a explanation of the constraint that is appropriate for conflicts.
*
- * This is not appropraite for propagation!
+ * This is not appropriate for propagation!
*
* This is the minimum fringe of the implication tree s.t.
* every constraint is assertedToTheTheory() or hasEqualityEngineProof().
* This is the minimum fringe of the implication tree s.t.
* every constraint is assertedToTheTheory() or hasEqualityEngineProof().
*
- * This is not appropraite for propagation!
+ * This is not appropriate for propagation!
* Use explainForPropagation() instead.
*/
void explainForConflict(NodeBuilder<>& nb) const{
void propagate(const std::vector<Constraint>& b);
/**
* The only restriction is that this is not known be true.
- * This propgates if there is a node.
+ * This propagates if there is a node.
*/
void impliedBy(Constraint a);
void impliedBy(Constraint a, Constraint b);
* If no such constraint exists, NullConstraint is returned.
*
* t must be either UpperBound or LowerBound.
- * The returned value v is dominatated:
+ * The returned value v is dominated:
* If t is UpperBound, r <= v
* If t is LowerBound, r >= v
*/
/*TODO Currently linear in the size of the Queue
*It is not clear if am O(log n) strategy would be better.
- *Right before this in the algorithm is a substition which could potentially
+ *Right before this in the algorithm is a substitution which could potentially
*effect the key values of everything in the queue.
*/
void DioSolver::moveMinimumByAbsToQueueFront(){
SumPair DioSolver::purifyIndex(TrailIndex i){
- // TODO: "This uses the substition trail to reverse the substitions from the sum term. Using the proof term should be more efficient."
+ // TODO: "This uses the substitution trail to reverse the substitutions from the sum term. Using the proof term should be more efficient."
SumPair curr = d_trail[i].d_eq;
void debugPrintTrail(TrailIndex i) const;
public:
- /** These fields are designed to be accessable to TheoryArith methods. */
+ /** These fields are designed to be accessible to TheoryArith methods. */
class Statistics {
public:
/********************* */
-/*! \file simplex.cpp
+/*! \file linear_equality.cpp
** \verbatim
** Original author: taking
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
public:
/**
- * Initailizes a LinearEqualityModule with a partial model, a tableau,
+ * Initializes a LinearEqualityModule with a partial model, a tableau,
* and a callback function for when basic variables update their values.
*/
LinearEqualityModule(ArithPartialModel& pm, Tableau& t, ArithVarCallBack& f):
private:
- /** These fields are designed to be accessable to TheoryArith methods. */
+ /** These fields are designed to be accessible to TheoryArith methods. */
class Statistics {
public:
IntStat d_statPivots, d_statUpdates;
/********************* */
-/*! \file tableau.cpp
+/*! \file matrix.cpp
** \verbatim
** Original author: taking
** Major contributors: none
** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
typedef typename SuperT::const_iterator const_iterator;
RowVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
-};
+};/* class RowVector<T> */
template <class T>
class ColumnVector : public MatrixVector<T, false>
typedef typename SuperT::const_iterator const_iterator;
ColumnVector(MatrixEntryVector<T>* mev) : SuperT(mev){}
-};
+};/* class ColumnVector<T> */
template <class T>
class Matrix {
/* Changes the basic variable on the row for basicOld to basicNew. */
void rowPivot(ArithVar basicOld, ArithVar basicNew);
-};
+};/* class Tableau */
}/* CVC4::theory::arith namespace */
}/* CVC4::theory namespace */
*/
static Node computeQR(const Polynomial& p, const Integer& z);
- /** Returns the coefficient assiociated with the VarList in the polynomial. */
+ /** Returns the coefficient associated with the VarList in the polynomial. */
Constant getCoefficient(const VarList& vl) const;
uint32_t maxLength() const{
* is known to implicitly be equal to 0.
*
* SumPairs do not have unique representations due to the potential for p = 0.
- * This makes them inappropraite for normal forms.
+ * This makes them inappropriate for normal forms.
*/
class SumPair : public NodeWrapper {
private:
d_deltaIsSafe = true;
}
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
- /** These fields are designed to be accessable to TheoryArith methods. */
+ /** These fields are designed to be accessible to TheoryArith methods. */
class Statistics {
public:
IntStat d_statUpdateConflicts;
}
}
-}; /* namesapce arith */
-}; /* namespace theory */
-}; /* namespace CVC4 */
+}/* CVC4::theory::arith namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
/**
* Splits the disequalities in d_diseq that are violated using lemmas on demand.
* returns true if any lemmas were issued.
- * returns false if all disequalities are satisified in the current model.
+ * returns false if all disequalities are satisfied in the current model.
*/
bool splitDisequalities();
/** Tracks the bounds that were updated in the current round. */
DenseSet d_updatedBounds;
- /** Tracks the basic variables where propagatation might be possible. */
+ /** Tracks the basic variables where propagation might be possible. */
DenseSet d_candidateBasics;
bool hasAnyUpdates() { return !d_updatedBounds.empty(); }
bool assertionCases(Constraint c);
/**
- * Returns the basic variable with the shorted row containg a non-basic variable.
+ * Returns the basic variable with the shorted row containing a non-basic variable.
* If no such row exists, return ARITHVAR_SENTINEL.
*/
ArithVar findShortestBasicRow(ArithVar variable);
/** Debugging only routine. Prints the model. */
void debugPrintModel();
- /** These fields are designed to be accessable to TheoryArith methods. */
+ /** These fields are designed to be accessible to TheoryArith methods. */
class Statistics {
public:
IntStat d_statAssertUpperConflicts, d_statAssertLowerConflicts;
/********************* */
-/*! \file instantiator_arith_instantiator.cpp
+/*! \file theory_arith_instantiator.cpp
** \verbatim
** Original author: ajreynol
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file instantiator_arith_instantiator.h
+/*! \file theory_arith_instantiator.h
** \verbatim
** Original author: ajreynol
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
/**
* Propagate through the asserted circuit propagator. New information discovered by the propagator
- * are put in the subsitutions vector used in construction.
+ * are put in the substitutions vector used in construction.
*
* @return true iff conflict found
*/
}
void DefaultPlusBB (TNode node, Bits& res, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefaulPlusBB bitblasting " << node << "\n";
+ BVDebug("bitvector-bb") << "theory::bv::DefaultPlusBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_PLUS &&
res.size() == 0);
void DefaultSubBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefautSubBB bitblasting " << node << "\n";
+ BVDebug("bitvector-bb") << "theory::bv::DefaultSubBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_SUB &&
node.getNumChildren() == 2 &&
bits.size() == 0);
}
void DefaultNegBB (TNode node, Bits& bits, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefautNegBB bitblasting " << node << "\n";
+ BVDebug("bitvector-bb") << "theory::bv::DefaultNegBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_NEG);
Bits a;
}
void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefautUdivBB bitblasting " << node << "\n";
+ BVDebug("bitvector-bb") << "theory::bv::DefaultUdivBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_UDIV && q.size() == 0);
Bits a, b;
}
void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) {
- BVDebug("bitvector-bb") << "theory::bv::DefautUremBB bitblasting " << node << "\n";
+ BVDebug("bitvector-bb") << "theory::bv::DefaultUremBB bitblasting " << node << "\n";
Assert(node.getKind() == kind::BITVECTOR_UREM && rem.size() == 0);
Bits a, b;
/********************* */
-/*! \file bv_subtheory_eq_bitblast.cpp
+/*! \file bv_subtheory_bitblast.cpp
** \verbatim
- ** Original author: lianah
- ** Major contributors: dejan
+ ** Original author: dejan
+ ** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file bv_subtheory_eq_bitblast.h
+/*! \file bv_subtheory_bitblast.h
** \verbatim
- ** Original author: lianah
- ** Major contributors: dejan
+ ** Original author: dejan
+ ** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file theory_bv_rewrite_rules_core.h
+/*! \file theory_bv_rewrite_rules_constant_evaluation.h
** \verbatim
** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version):
+ ** Major contributors: barrett
+ ** 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)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file theory_bv_rewrite_rules_core.h
+/*! \file theory_bv_rewrite_rules_operator_elimination.h
** \verbatim
** Original author: lianah
- ** Major contributors: none
- ** Minor contributors (to current version):
+ ** Major contributors: barrett
+ ** 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)
+ ** Copyright (c) 2009-2012 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
template<>
Node RewriteRule<SgtEliminate>::apply(TNode node) {
- BVDebug("bv-rewrite") << "RgewriteRule<UgtEliminate>(" << node << ")" << std::endl;
+ BVDebug("bv-rewrite") << "RewriteRule<SgtEliminate>(" << node << ")" << std::endl;
TNode a = node[0];
TNode b = node[1];
Node result = utils::mkNode(kind::BITVECTOR_SLT, b, a);
/********************* */
-/*! \file instantiator_datatypes_instantiator.h
+/*! \file theory_datatypes_instantiator.h
** \verbatim
** Original author: ajreynol
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
virtual void reset( Node eqc, QuantifiersEngine* qe ) = 0;
/** get the next match. must call reset( eqc ) before this function. */
virtual bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) = 0;
- /** return true if whatever Node is subsituted for the variables the
+ /** return true if whatever Node is substituted for the variables the
given Node can't match the pattern */
virtual bool nonunifiable( TNode t, const std::vector<Node> & vars) = 0;
/** add instantiations directly */
bool getMatchArithmetic( Node t, InstMatch& m, QuantifiersEngine* qe );
public:
/** get the match against ground term or formula t.
- d_match_mattern and t should have the same shape.
+ d_match_pattern and t should have the same shape.
only valid for use where !d_match_pattern.isNull().
*/
bool getMatch( Node t, InstMatch& m, QuantifiersEngine* qe );
void reset( Node eqc, QuantifiersEngine* qe );
/** get the next match. must call reset( eqc ) before this function. */
bool getNextMatch( InstMatch& m, QuantifiersEngine* qe );
- /** return true if whatever Node is subsituted for the variables the
+ /** return true if whatever Node is substituted for the variables the
given Node can't match the pattern */
bool nonunifiable( TNode t, const std::vector<Node> & vars);
/** add instantiations */
std::vector< IndexedTrie >& unique_var_tries,
int uvtIndex, InstMatchTrie* tr = NULL, int trieIndex = 0 );
private:
- /** var contains (variable indicies) for each pattern node */
+ /** var contains (variable indices) for each pattern node */
std::map< Node, std::vector< int > > d_var_contains;
- /** variable indicies contained to pattern nodes */
+ /** variable indices contained to pattern nodes */
std::map< int, std::vector< Node > > d_var_to_node;
/** quantifier to use */
Node d_f;
void reset( Node eqc, QuantifiersEngine* qe );
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
- /** return true if whatever Node is subsituted for the variables the
+ /** return true if whatever Node is substituted for the variables the
given Node can't match the pattern */
bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
/** add instantiations */
void reset( Node eqc, QuantifiersEngine* qe ) {}
/** get the next match. must call reset( eqc ) before this function. (not implemented) */
bool getNextMatch( InstMatch& m, QuantifiersEngine* qe ) { return false; }
- /** return true if whatever Node is subsituted for the variables the
+ /** return true if whatever Node is substituted for the variables the
given Node can't match the pattern */
bool nonunifiable( TNode t, const std::vector<Node> & vars) { return true; }
/** add instantiations */
/********************* */
-/*! \file inst_match.h
+/*! \file inst_match_impl.h
** \verbatim
- ** Original author: ajreynol
+ ** Original author: bobot
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking, mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
void assertNode( Node assertion );
/** identify */
std::string identify() const { return std::string("InstantiatorDefault"); }
-};/* class Instantiatior */
+};/* class InstantiatorDefault */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
/********************* */
-/*! \file instantiation_engine.h
+/*! \file model_engine.h
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
** 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)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file theory_quantifiers_rewriter.cpp
+/*! \file quantifiers_rewriter.cpp
** \verbatim
** Original author: ajreynol
- ** Major contributors: none
+ ** Major contributors: mdeters
** 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)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file instantiator_quantifiers_instantiator.h
+/*! \file theory_quantifiers_instantiator.h
** \verbatim
** Original author: ajreynol
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
static RewriteResponse callPostRewrite(theory::TheoryId theoryId, TNode node);
/**
- * Calls the equality-rewruter for the given theory.
+ * Calls the equality-rewriter for the given theory.
*/
static Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
-/********************* */
-/*! \file rewrite_engine.cpp
+/********************* */
+/*! \file theory_rewriterules.cpp
** \verbatim
- ** Original author: ajreynolds
+ ** Original author: ajreynol
** Major contributors: bobot
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011
- ** The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
-/********************* */
-/*! \file rewrite_engine.h
+/********************* */
+/*! \file theory_rewriterules.h
** \verbatim
** Original author: ajreynol
** Major contributors: bobot
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011
- ** The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
*/
void propagateRule(const RuleInst * r, TCache cache);
- /** Auxillary functions */
+ /** Auxiliary functions */
private:
/** A guard is verify, notify the Guarded */
void notification(GList * const lpropa, bool b);
-/********************* */
-/*! \file rewrite_engine.cpp
+/********************* */
+/*! \file theory_rewriterules_params.h
** \verbatim
** Original author: bobot
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
static const bool useCurrentModel = false;
/**
- Simulate rewritting by tagging rewritten terms.
+ Simulate rewriting by tagging rewritten terms.
*/
static const bool simulateRewritting = false;
/********************* */
-/*! \file rewriterules.h
+/*! \file theory_rewriterules_preprocess.h
** \verbatim
** Original author: bobot
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
+/********************* */
+/*! \file theory_rewriterules_rewriter.h
+ ** \verbatim
+ ** Original author: bobot
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "cvc4_private.h"
#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_REWRITER_H
-/********************* */
-/*! \file rewrite_engine.cpp
+/********************* */
+/*! \file theory_rewriterules_rules.cpp
** \verbatim
- ** Original author: ajreynolds
- ** Major contributors: bobot
- ** Minor contributors (to current version): none
+ ** Original author: bobot
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011
- ** The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
};
break;
default:
- Unreachable("RewriteRules can be of only threee kinds");
+ Unreachable("RewriteRules can be of only three kinds");
};
/* Add the other guards */
TNode g = r[1];
-/********************* */
-/*! \file rewrite_engine.h
+/********************* */
+/*! \file theory_rewriterules_rules.h
** \verbatim
- ** Original author: ajreynol
- ** Major contributors: bobot
+ ** Original author: bobot
+ ** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
+/********************* */
+/*! \file theory_rewriterules_type_rules.h
+ ** \verbatim
+ ** Original author: bobot
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "cvc4_private.h"
#ifndef __CVC4__THEORY__REWRITERULES__THEORY_REWRITERULES_TYPE_RULES_H
/********************* */
-/*! \file node_visitor.h
+/*! \file shared_terms_database.h
** \verbatim
** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: mdeters
+ ** 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)
+ ** Copyright (c) 2009-2012 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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
**/
#pragma once
/********************* */
-/*! \file term_registration_visitor.h
+/*! \file term_registration_visitor.cpp
** \verbatim
** Original author: dejan
- ** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): taking, barrett
** This file is part of the CVC4 prototype.
** Copyright (c) 2009-2012 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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
**/
#include "theory/term_registration_visitor.h"
/********************* */
-/*! \file node_visitor.h
+/*! \file term_registration_visitor.h
** \verbatim
** Original author: dejan
- ** Major contributors:
- ** Minor contributors (to current version):
+ ** Major contributors: none
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
**/
#include "cvc4_private.h"
SharedTermsDatabase& d_sharedTerms;
/**
- * Cache from proprocessing of atoms.
+ * Cache from preprocessing of atoms.
*/
typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap;
TNodeVisitedMap d_visited;
Node TheoryEngine::getExplanation(TNode node) {
- Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current proagation index = " << d_propagationMapTimestamp << std::endl;
+ Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << "): current propagation index = " << d_propagationMapTimestamp << std::endl;
bool polarity = node.getKind() != kind::NOT;
TNode atom = polarity ? node : node[0];
explanation = theoryOf(toExplain.theory)->explain(toExplain.node);
}
Debug("theory::explain") << "TheoryEngine::explain(): got explanation " << explanation << " got from " << toExplain.theory << std::endl;
- Assert(explanation != toExplain.node, "wansn't sent to you, so why are you explaining it trivially");
+ Assert(explanation != toExplain.node, "wasn't sent to you, so why are you explaining it trivially");
// Mark the explanation
NodeTheoryPair newExplain(explanation, toExplain.theory, toExplain.timestamp);
explanationVector.push_back(newExplain);
void preprocessStart();
/**
- * Runs theory specific preprocesssing on the non-Boolean parts of
+ * Runs theory specific preprocessing on the non-Boolean parts of
* the formula. This is only called on input assertions, after ITEs
* have been removed.
*/
/********************* */
-/*! \file registrar.h
+/*! \file theory_registrar.h
** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
+ ** Original author: lianah
+ ** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
#include "cvc4_public.h"
#ifndef __CVC4__THEORY__THEORY_TEST_UTILS_H
-#define __CVC4__THEORY__ITHEORY_TEST_UTILS_H
+#define __CVC4__THEORY__THEORY_TEST_UTILS_H
#include "util/Assert.h"
#include "expr/node.h"
/********************* */
-/*! \file theory.h
+/*! \file theoryof_mode.h
** \verbatim
** Original author: mdeters
** Major contributors: dejan
** Minor contributors (to current version): taking, barrett
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009, 2010, 2011, 2012 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 Base of the theory interface.
+ ** \brief Option selection for theoryOf() operation
**
- ** Base of the theory interface.
+ ** Option selection for theoryOf() operation.
**/
#pragma once
THEORY_OF_TYPE_BASED,
/** Variables are uninterpreted, constants are with the type, equalities prefer parametric */
THEORY_OF_TERM_BASED
-};
+};/* enum TheoryOfMode */
-}
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
/********************* */
-/*! \file equality_engine_impl.h
+/*! \file equality_engine.cpp
** \verbatim
** Original author: dejan
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): taking, mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
// This is the class trigger set
const TriggerTermSet& triggerSet = getTriggerTermSet(triggerSetRef);
- // Go throught the disequalities and notify
+ // Go through the disequalities and notify
TaggedEqualitiesSet::const_iterator it = disequalitiesToNotify.begin();
TaggedEqualitiesSet::const_iterator it_end = disequalitiesToNotify.end();
for (; !d_done && it != it_end; ++ it) {
/**
- * Class for keeping an incremental congurence closure over a set of terms. It provides
+ * Class for keeping an incremental congruence closure over a set of terms. It provides
* notifications via an EqualityEngineNotify object.
*/
class EqualityEngine : public context::ContextNotifyObj {
/** Number of application lookups, for backtracking. */
context::CDO<DefaultSizeType> d_applicationLookupsCount;
- /** Map from ids to the nodes (these need to be nodes as we pick-up the opreators) */
+ /** Map from ids to the nodes (these need to be nodes as we pick up the operators) */
std::vector<Node> d_nodes;
/** A context-dependents count of nodes */
/**
* All the equality edges (twice as many as the number of asserted equalities. If an equality
- * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index
+ * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hence, having the index
* of one of the edges you can reconstruct the original equality.
*/
std::vector<EqualityEdge> d_equalityEdges;
std::vector<TriggerId> d_nodeTriggers;
/**
- * Map from ids to wheather they are constants (constants are always
+ * Map from ids to whether they are constants (constants are always
* representatives of their class.
*/
std::vector<bool> d_isConstant;
}
/**
- * Map from ids to wheather they are Boolean.
+ * Map from ids to whether they are Boolean.
*/
std::vector<bool> d_isBoolean;
bool hasPropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId) const;
/**
- * Stores a propagated disequality for explanation purpooses and remembers the reasons. The
+ * Stores a propagated disequality for explanation purposes and remembers the reasons. The
* reasons should be pushed on the reasons vector.
*/
void storePropagatedDisequality(TheoryId tag, EqualityNodeId lhsId, EqualityNodeId rhsId);
/**
* Adds a predicate p with given polarity. The predicate asserted
- * should be in the coungruence closure kinds (otherwise it's
+ * should be in the congruence closure kinds (otherwise it's
* useless.
*
* @param p the (non-negated) predicate
size_t getSize(TNode t);
/**
- * Returns true if the engine is in a consistents state.
+ * Returns true if the engine is in a consistent state.
*/
bool consistent() const { return !d_done; }
};
/**
- * We mantaint uselist where a node appears in, and this is the node
+ * We maintain uselist where a node appears in, and this is the node
* of such a list.
*/
class UseListNode {
* Main class for representing nodes in the equivalence class. The
* nodes are a circular list, with the representative carrying the
* size. Each individual node carries with itself the uselist of
- * functino applications it appears in and the list of asserted
+ * function applications it appears in and the list of asserted
* disequalities it belongs to. In order to get these lists one must
* traverse the entire class and pick up all the individual lists.
*/
/********************* */
-/*! \file theory_uf_candidate generator.h
+/*! \file theory_uf_candidate_generator.h
** \verbatim
** Original author: ajreynol
** Major contributors: none
- ** Minor contributors (to current version): none
+ ** Minor contributors (to current version): mdeters
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 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
}
Assert( children.size()>1 );
Node lem = NodeManager::currentNM()->mkNode( OR, children );
- Debug( "uf-ss-lemma" ) << "*** Diambiguate lemma : " << lem << std::endl;
- //Notice() << "*** Diambiguate lemma : " << lem << std::endl;
+ Debug( "uf-ss-lemma" ) << "*** Disambiguate lemma : " << lem << std::endl;
+ //Notice() << "*** Disambiguate lemma : " << lem << std::endl;
out->lemma( lem );
d_term_amb[ eq ] = false;
lemmaAdded = true;
/** statistics class */
Statistics d_statistics;
- /** is relavant type */
+ /** is relevant type */
static bool isRelevantType( TypeNode t );
- /** involves relavant type */
+ /** involves relevant type */
static bool involvesRelevantType( Node n );
};/* class StrongSolverTheoryUf */
}
break;
- // Array store - if both store and value are uncosntrained, so is resulting store
+ // Array store - if both store and value are unconstrained, so is resulting store
case kind::STORE:
if (((parent[0] == current &&
d_unconstrained.find(parent[2]) != d_unconstrained.end()) ||
new(head)ListNode<T> (d, head->next);
//head->data = d;
head->empty = false;
- //Assert(tail == head); FIXME: do I need this because this list might be empty but appende to another one
+ //Assert(tail == head); FIXME: do I need this because this list might be empty but append to another one
uninitialized = false;
} else {
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief A multiprecision rational constant.
+ ** \brief A multi-precision rational constant.
**
- ** A multiprecision rational constant.
- ** This stores the rational as a pair of multiprecision integers,
+ ** A multi-precision rational constant.
+ ** This stores the rational as a pair of multi-precision integers,
** one for the numerator and one for the denominator.
** The number is always stored so that the gcd of the numerator and denominator
** is 1. (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consquence is that that the numerator and denominator may be
+ ** literature.) A consequence is that that the numerator and denominator may be
** different than the values used to construct the Rational.
**/
** This is an abstraction of a Map from an unsigned integer to elements of type T.
** This class is designed to provide constant time insertion, deletion, element_of,
** and fast iteration. This is done by storing backing vectors of size greater than
- ** the maximum key. This datastructure is appropraite for heavy use datastructures
+ ** the maximum key. This datastructure is appropriate for heavy use datastructures
** where the Keys are a dense set of integers.
**
** T must support T(), and operator=().
+/********************* */
+/*! \file index.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "cvc4_private.h"
#pragma once
/* Discussion: Why is Index a uint32_t instead of size_t (or uint_fast32_t)?
*
- * size_t is a more appropraite choice than uint32_t as the choice is dictated by
+ * size_t is a more appropriate choice than uint32_t as the choice is dictated by
* uniqueness in arrays and vectors. These correspond to size_t.
- * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticably
+ * However, the using size_t with a sizeof == 8 on 64 bit platforms is noticeably
* slower. (Limited testing suggests a ~1/16 of running time.)
* (Interestingly, uint_fast32_t also has a sizeof == 8 on x86_64. Filthy Liars!)
*/
-}; /* namespace CVC4 */
+}/* CVC4 namespace */
*/
unsigned isPow2() const {
if (d_value <= 0) return 0;
- // check that the number of ones in the binary represenation is 1
+ // check that the number of ones in the binary representation is 1
if (mpz_popcount(d_value.get_mpz_t()) == 1) {
// return the index of the first one plus 1
return mpz_scan1(d_value.get_mpz_t(), 0) + 1;
+/********************* */
+/*! \file lemma_input_channel.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009-2012 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 "cvc4_public.h"
#ifndef __CVC4__LEMMA_INPUT_CHANNEL_H
** Major contributors: dejan
** 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, 2010, 2011, 2012 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 A simple visitor for nodes.
+ ** \brief A simple visitor for nodes
**
- ** The theory engine.
+ ** A simple visitor for nodes.
**/
#pragma once
namespace CVC4 {
/**
- * Traverses the nodes topologically and call the visitor when all the children have been visited.
+ * Traverses the nodes reverse-topologically (children before parents),
+ * calling the visitor in order.
*/
template<typename Visitor>
class NodeVisitor {
/** For re-entry checking */
static CVC4_THREADLOCAL(bool) s_inRun;
+ /**
+ * Guard against NodeVisitor<> being re-entrant.
+ */
class GuardReentry {
bool& d_guard;
public:
Assert(d_guard);
d_guard = false;
}
- };
+ };/* class NodeVisitor<>::GuardReentry */
public:
// Notify of a start
visitor.start(node);
- // Do a topological sort of the subexpressions
+ // Do a reverse-topological sort of the subexpressions
std::vector<stack_element> toVisit;
toVisit.push_back(stack_element(node, node));
while (!toVisit.empty()) {
return visitor.done(node);
}
-};
+};/* class NodeVisitor<> */
template <typename Visitor>
CVC4_THREADLOCAL(bool) NodeVisitor<Visitor>::s_inRun = false;
-}
-
+}/* CVC4 namespace */
--print-winner enable printing the winning thread (pcvc4 only)\n\
--trace | -t trace something (e.g. -t pushpop), can repeat\n\
--debug | -d debug something (e.g. -d arith), can repeat\n\
- --show-debug-tags show all avalable tags for debugging\n\
- --show-trace-tags show all avalable tags for tracing\n\
+ --show-debug-tags show all available tags for debugging\n\
+ --show-trace-tags show all available tags for tracing\n\
--show-sat-solvers show all available SAT solvers\n\
--default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
--default-dag-thresh=N dagify common subexprs appearing > N times\n\
--lazy-definition-expansion expand define-funs/LAMBDAs lazily\n\
--simplification=MODE choose simplification mode, see --simplification=help\n\
--decision=MODE choose decision mode, see --decision=help\n\
- --decision-budget=N impose a budget for relevancy hueristic which increases linearly with\n\
+ --decision-budget=N impose a budget for relevancy heuristic which increases linearly with\n\
each decision. N between 0 and 1000. (default: 1000, no budget)\n\
--no-static-learning turn off static learning (e.g. diamond-breaking)\n\
--ite-simp turn on ite simplification (Kim (and Somenzi) et al., SAT 2009)\n\
--threadN=string configures thread N (0..#threads-1)\n\
--filter-lemma-length=N don't share lemmas strictly longer than N\n\
--bitblast-eager eagerly bitblast the bitvectors to the main SAT solver\n\
- --bitblast-share-lemmas share lemmas from the bitblsting solver with the main solver\n\
+ --bitblast-share-lemmas share lemmas from the bitblasting solver with the main solver\n\
--bitblast-eager-fullcheck check the bitblasting eagerly\n\
--refine-conflicts refine theory conflict clauses\n\
";
Decision modes currently supported by the --decision option:\n\
\n\
internal (default)\n\
-+ Use the internal decision hueristics of the SAT solver\n\
++ Use the internal decision heuristics of the SAT solver\n\
\n\
justification\n\
+ An ATGP-inspired justification heuristic\n\
+ Output correctness queries for all theory explanations\n\
\n\
Dump modes can be combined with multiple uses of --dump. Generally you want\n\
-one from the assertions category (either asertions, learned, or clauses), and\n\
+one from the assertions category (either assertions, learned, or clauses), and\n\
perhaps one or more stateful or non-stateful modes for checking correctness\n\
and completeness of decision procedure implementations. Stateful modes dump\n\
the contextual assertions made by the core solver (all decisions and\n\
";
static const string pivotRulesHelp = "\
-This decides on the rule used by simplex during hueristic rounds\n\
+This decides on the rule used by simplex during heuristic rounds\n\
for deciding the next basic variable to select.\n\
Pivot rules available:\n\
+min\n\
optarg + "'. Must be between 0 and 1000.");
}
if(i == 0) {
- Warning() << "Decision budget is 0. Consider using internal decision hueristic and "
+ Warning() << "Decision budget is 0. Consider using internal decision heuristic and "
<< std::endl << " removing this option." << std::endl;
}
ArithPropagationMode arithPropagationMode;
/**
- * The maximum number of difference pivots to do per invokation of simplex.
+ * The maximum number of difference pivots to do per invocation of simplex.
* If this is negative, the number of pivots done is the number of variables.
* If this is not set by the user, different logics are free to chose different
* defaults.
bool arithHeuristicPivotsSetByUser;
/**
- * The maximum number of variable order pivots to do per invokation of simplex.
+ * The maximum number of variable order pivots to do per invocation of simplex.
* If this is negative, the number of pivots done is unlimited.
* If this is not set by the user, different logics are free to chose different
* defaults.
#endif /* CVC4_STATISTICS_ON */
}/* StatisticsRegistry::registerStat() */
-void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException)
-{
+void StatisticsRegistry::registerStat_(Stat* s) throw(AssertionException) {
#ifdef CVC4_STATISTICS_ON
AlwaysAssert(d_registeredStats.find(s) == d_registeredStats.end());
d_registeredStats.insert(s);
/********************* */
-/*! \file cvc3_main.cpp
+/*! \file cvc3_george.cpp
** \verbatim
** Original author: mdeters
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
/********************* */
-/*! \file cvc3_main.cpp
+/*! \file cvc3_george.h
** \verbatim
** Original author: mdeters
** Major contributors: none
** 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)
+ ** Copyright (c) 2009-2012 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
d_cmm->pop();
}
- // Try poping out of scope
+ // Try popping out of scope
d_cmm->pop();
}
projects / cvc5.git / commitdiff