count=0
for attachment in $(\
- webcat "http://church.cims.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \
+ webcat "http://cvc4.cs.nyu.edu/bugs/show_bug.cgi?id=$bugid" 2>/dev/null \
| grep ' href="attachment.cgi?id=[0-9][0-9]*' \
| sed 's,.* href="attachment.cgi?id=\([0-9][0-9]*\).*,\1,' \
| sort -nu); do
let count++
printf "%-30s " "Downloading attachment $attachment..."
- webget "http://church.cims.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid"
+ webget "http://cvc4.cs.nyu.edu/bugs/attachment.cgi?id=$attachment" "test/regress/regress0/bug$bugid"
done
and constants
* to write code in theory_$dir_rewriter.h to implement a normal form
for your theory's terms
+* for any new types that you have introduced, add "mk*Type()" functions to
+ the NodeManager and ExprManager in src/expr/node_manager.{h,cpp} and
+ src/expr/expr_manager_template.{h,cpp}. You may also want "is*()" testers
+ in src/expr/type_node.h and a corresponding Type derived class in
+ src/expr/type.h.
* to write parser rules in src/parser/cvc/Cvc.g to support the CVC input
language, src/parser/smt/Smt.g to support the (deprecated) SMT-LIBv1
language, and src/parser/smt2/Smt2.g to support SMT-LIBv2
version @VERSION@.
.SH BUGS
A Bugzilla for the CVC4 project is maintained at
-.BR http://church.cims.nyu.edu/bugzilla3/ .
+.BR http://cvc4.cs.nyu.edu/bugzilla3/ .
.SH AUTHORS
.B CVC4
is developed by a team of researchers at New York University
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://church.cims.nyu.edu/wiki/ .
+.BR http://cvc4.cs.nyu.edu/wiki/ .
version @VERSION@.
.SH BUGS
A Bugzilla for the CVC4 project is maintained at
-.BR http://church.cims.nyu.edu/bugzilla3/ .
+.BR http://cvc4.cs.nyu.edu/bugzilla3/ .
.SH AUTHORS
.B CVC4
is developed by a team of researchers at New York University
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://church.cims.nyu.edu/wiki/ .
+.BR http://cvc4.cs.nyu.edu/wiki/ .
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://church.cims.nyu.edu/wiki/ .
+.BR http://cvc4.cs.nyu.edu/wiki/ .
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://church.cims.nyu.edu/wiki/ .
+.BR http://cvc4.cs.nyu.edu/wiki/ .
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://church.cims.nyu.edu/wiki/ .
+.BR http://cvc4.cs.nyu.edu/wiki/ .
version @VERSION@.
.SH BUGS
A Bugzilla for the CVC4 project is maintained at
-.BR http://church.cims.nyu.edu/bugzilla3/ .
+.BR http://cvc4.cs.nyu.edu/bugzilla3/ .
.SH AUTHORS
.B CVC4
is developed by a team of researchers at New York University
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
-.BR http://church.cims.nyu.edu/wiki/ .
+.BR http://cvc4.cs.nyu.edu/wiki/ .
}/* CVC4::kind namespace */
-#line 348 "${template}"
+#line 349 "${template}"
namespace theory {
* If this is \top, i.e. there is no inhabited type that contains both,
* a TypeNode such that isNull() is true is returned.
*
- * For more information see: http://church.cims.nyu.edu/wiki/Cvc4_Type_Lattice
+ * For more information see: http://cvc4.cs.nyu.edu/wiki/Cvc4_Type_Lattice
*/
static TypeNode leastCommonTypeNode(TypeNode t0, TypeNode t1);
ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
term[expr, expr2]
{ cmd = new AssertCommand(expr); }
- | /* checksat */
+ | /* check-sat */
CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
( term[expr, expr2]
{ if(PARSER_STATE->strictModeEnabled()) {
(kind == CVC4::kind::AND || kind == CVC4::kind::OR) &&
args.size() == 1) {
/* Unary AND/OR can be replaced with the argument.
- It just so happens expr should already by the only argument. */
+ * It just so happens expr should already be the only argument. */
assert( expr == args[0] );
} else if( CVC4::kind::isAssociative(kind) &&
args.size() > EXPR_MANAGER->maxArity(kind) ) {
}
*/
PARSER_STATE->includeFile(name /* , inclArgs */ );
- // The command of the included file will be produced at the new parseCommand call
+ // The command of the included file will be produced at the next parseCommand() call
cmd = new EmptyCommand("include::" + name);
}
| EOF
Debug("parser") << "Can't open " << fileName << std::endl;
return false;
}
- // Samething than the predefined PUSHSTREAM(in);
+ // Same thing as the predefined PUSHSTREAM(in);
lexer->pushCharStream(lexer,in);
// restart it
//lexer->rec->state->tokenStartCharIndex = -10;
// Test in the directory of the actual parsed file
std::string currentDirFileName;
if(inputName != "<stdin>") {
- // TODO: Use dirname ot Boost::filesystem?
+ // TODO: Use dirname or Boost::filesystem?
size_t pos = inputName.rfind('/');
if(pos != std::string::npos) {
currentDirFileName = std::string(inputName, 0, pos + 1);
inline Command* Tptp::makeCommand(FormulaRole fr, Expr& expr, bool cnf) {
// For SZS ontology compliance.
- // If we're in cnf() though, conjectures don't result in "Theorem" or
+ // if we're in cnf() though, conjectures don't result in "Theorem" or
// "CounterSatisfiable".
if(!cnf && (fr == FR_NEGATED_CONJECTURE || fr == FR_CONJECTURE)) {
d_hasConjecture = true;
/** Get the language that this Input is reading. */
InputLanguage getLanguage() const throw() {
- return language::input::LANG_SMTLIB_V2;
+ return language::input::LANG_TPTP;
}
protected:
int i, j;
Lit prev = lit_Undef;
for (i = 0, j = 0; i < explanation.size(); ++ i) {
- // This clause is valid theory propagation, so it's level is the level of the top literal
+ // This clause is valid theory propagation, so its level is the level of the top literal
explLevel = std::max(explLevel, intro_level(var(explanation[i])));
Assert(value(explanation[i]) != l_Undef);
assert(assigns[var(ps[0])] != l_False);
uncheckedEnqueue(ps[0], cr);
PROOF( if (ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], true); } )
- return ok = (propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef);
+ return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef);
} else return ok;
}
}
// Propagate on the clauses
confl = propagateBool();
// If no conflict, do the theory check
- if (confl == CRef_Undef && type != CHECK_WITHOUTH_THEORY) {
+ if (confl == CRef_Undef && type != CHECK_WITHOUT_THEORY) {
// Do the theory check
if (type == CHECK_FINAL_FAKE) {
theoryCheck(CVC4::theory::Theory::EFFORT_FULL);
for (i = j = 0; i < cs.size(); i++){
Clause& c = ca[cs[i]];
if (c.level() > level) {
- assert(!locked(c));
- removeClause(cs[i]);
+ assert(!locked(c));
+ removeClause(cs[i]);
} else {
cs[j++] = cs[i];
}
{
assert(decisionLevel() == 0);
- if (!ok || propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef)
+ if (!ok || propagate(CHECK_WITHOUT_THEORY) != CRef_Undef)
return ok = false;
if (nAssigns() == simpDB_assigns || (simpDB_props > 0))
if (next == lit_Undef) {
// We need to do a full theory check to confirm
- Debug("minisat::search") << "Doing a full theoy check..."
+ Debug("minisat::search") << "Doing a full theory check..."
<< std::endl;
check_type = CHECK_FINAL;
continue;
Debug("minisat") << "== unassigning " << trail.last() << std::endl;
Var x = var(trail.last());
if (user_level(x) > assertionLevel) {
- assigns [x] = l_Undef;
+ assigns[x] = l_Undef;
vardata[x] = VarData(CRef_Undef, -1, -1, intro_level(x), -1);
if(phase_saving >= 1 && (polarity[x] & 0x2) == 0)
polarity[x] = sign(trail.last());
// The head should be at the trail top
qhead = trail.size();
- // Remove the clause
+ // Remove the clauses
removeClausesAboveLevel(clauses_persistent, assertionLevel);
removeClausesAboveLevel(clauses_removable, assertionLevel);
int level;
// User level when the literal was added to the trail
int user_level;
- // Use level at which this literal was introduced
+ // User level at which this literal was introduced
int intro_level;
// The index in the trail
int trail_index;
enum TheoryCheckType {
// Quick check, but don't perform theory reasoning
- CHECK_WITHOUTH_THEORY,
+ CHECK_WITHOUT_THEORY,
// Check and perform theory reasoning
CHECK_WITH_THEORY,
// The SAT abstraction of the problem is satisfiable, perform a full theory check
/** The SatSolver used */
Minisat::SimpSolver* d_minisat;
-
/** The SatSolver uses this to communicate with the theories */
TheoryProxy* d_theoryProxy;
- /** Context we will be using to synchronzie the sat solver */
+ /** Context we will be using to synchronize the sat solver */
context::Context* d_context;
public:
- MinisatSatSolver ();
+ MinisatSatSolver();
~MinisatSatSolver();
static SatVariable toSatVariable(Minisat::Var var);
const T& operator [] (int index) const { return data[index]; }
T& operator [] (int index) { return data[index]; }
- // Duplicatation (preferred instead):
+ // Duplication (preferred instead):
void copyTo(vec<T>& copy) const { copy.clear(); copy.growTo(sz); for (int i = 0; i < sz; i++) copy[i] = data[i]; }
void moveTo(vec<T>& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; }
};
if(options::minisatUseElim() &&
options::minisatUseElim.wasSetByUser() &&
enableIncremental) {
- WarningOnce() << "Incremental mode incompatible with --minisat-elimination" << std::endl;
+ WarningOnce() << "Incremental mode incompatible with --minisat-elim" << std::endl;
}
vec<Lit> dummy(1,lit_Undef);
updateElimHeap(var(l));
}
- return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUTH_THEORY) == CRef_Undef : true;
+ return c.size() == 1 ? enqueue(c[0]) && propagate(CHECK_WITHOUT_THEORY) == CRef_Undef : true;
}
uncheckedEnqueue(~c[i]);
}
- bool result = propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef;
+ bool result = propagate(CHECK_WITHOUT_THEORY) != CRef_Undef;
cancelUntil(0);
return result;
}
else
l = c[i];
- if (propagate(CHECK_WITHOUTH_THEORY) != CRef_Undef){
+ if (propagate(CHECK_WITHOUT_THEORY) != CRef_Undef){
cancelUntil(0);
asymm_lits++;
if (!strengthenClause(cr, l))
option satRestartInc --restart-int-inc=F double :default 3.0 :predicate greater_equal(0.0)
sets the restart interval increase factor for the sat solver (F=3.0 by default)
-option sat_refine_conflicts --refine-conflicts bool
- refine theory conflict clauses
+option sat_refine_conflicts --refine-conflicts bool :default false
+ refine theory conflict clauses (default false)
option minisatUseElim --minisat-elimination bool :default true :read-write
use Minisat elimination
common-option perCallMillisecondLimit tlimit-per --tlimit-per=MS "unsigned long"
enable time limiting per query (give milliseconds)
common-option cumulativeResourceLimit rlimit --rlimit=N "unsigned long"
- enable resource limiting
+ enable resource limiting (currently, roughly the number of SAT conflicts)
common-option perCallResourceLimit rlimit-per --rlimit-per=N "unsigned long"
enable resource limiting per query
return;
}
- if (options::bitvectorEagerBitblast()) {
+ if(options::bitvectorEagerBitblast()) {
// Eager solver should use the internal decision strategy
options::decisionMode.set(DECISION_STRATEGY_INTERNAL);
}
// otherwise expand it
NodeManager* nm = d_smt.d_nodeManager;
- // FIXME: this theory specific code should be factored out of the SmtEngine, somehow
+ // FIXME: this theory-specific code should be factored out of the
+ // SmtEngine, somehow
switch(k) {
case kind::BITVECTOR_SDIV:
case kind::BITVECTOR_SREM:
- case kind::BITVECTOR_SMOD: {
+ case kind::BITVECTOR_SMOD:
node = bv::TheoryBVRewriter::eliminateBVSDiv(node);
break;
- }
case kind::BITVECTOR_UDIV:
- case kind::BITVECTOR_UREM: {
+ case kind::BITVECTOR_UREM:
node = expandBVDivByZero(node);
break;
- }
case kind::DIVISION: {
// partial function: division
Rewriter::rewrite(Node(builder));
}
// For some reason this is needed for some benchmarks, such as
- // http://church.cims.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
+ // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
// Figure it out later
removeITEs();
// Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
/**
* Set a resource limit for SmtEngine operations. This is like a time
* limit, but it's deterministic so that reproducible results can be
- * obtained. However, please note that it may not be deterministic
- * between different versions of CVC4, or even the same version on
- * different platforms.
+ * obtained. Currently, it's based on the number of conflicts.
+ * However, please note that the definition may change between different
+ * versions of CVC4 (as may the number of conflicts required, anyway),
+ * and it might even be different between instances of the same version
+ * of CVC4 on different platforms.
*
* A cumulative and non-cumulative (per-call) resource limit can be
* set at the same time. A call to setResourceLimit() with
/**
* If glpk is enabled, return a subclass that can do something.
- * If glpk is disabled, return a sublass that does nothing.
+ * If glpk is disabled, return a subclass that does nothing.
*/
static ApproximateSimplex* mkApproximateSimplexSolver(const ArithVariables& vars);
ApproximateSimplex();
virtual ApproxResult solveMIP() = 0;
virtual Solution extractMIP() const = 0;
- /** UTILIES FOR DEALING WITH ESTIMATES */
+ /** UTILITIES FOR DEALING WITH ESTIMATES */
static const double SMALL_FIXED_DELTA;
static const double TOLERENCE;
+/********************* */
+/*! \file bound_counts.h
+ ** \verbatim
+ ** Original author: Tim King
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
using namespace std;
namespace CVC4 {
-namespace theory{
+namespace theory {
namespace arith {
bool Variable::isDivMember(Node n){
turns on the preprocessing step of attempting to infer bounds on miplib problems
/turns off the preprocessing step of attempting to infer bounds on miplib problems
-option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs unsigned :default 1
+option arithMLTrickSubstitutions miplib-trick-subs --miplib-trick-subs=N unsigned :default 1
do substitution for miplib 'tmp' vars if defined in <= N eliminated vars
option doCutAllBounded --cut-all-bounded bool :default false :read-write
maximum cuts in a given context before signalling a restart
option revertArithModels --revert-arith-models-on-unsat bool :default false
- Revert the arithmetic model to a known safe model on unsat if one is cached
+ revert the arithmetic model to a known safe model on unsat if one is cached
option havePenalties --fc-penalties bool :default false :read-write
turns on degenerate pivot penalties
-/ turns off degenerate pivot penalties
+/turns off degenerate pivot penalties
option useFC --use-fcsimplex bool :default false :read-write
use focusing and converging simplex (FMCAD 2013 submission)
use sum of infeasibility simplex (FMCAD 2013 submission)
option restrictedPivots --restrict-pivots bool :default true :read-write
- have a pivot cap for simplex at effort levels below fullEffort.
+ have a pivot cap for simplex at effort levels below fullEffort
option collectPivots --collect-pivot-stats bool :default false :read-write
collect the pivot history
option fancyFinal --fancy-final bool :default false :read-write
- Tuning how final check works for really hard problems.
+ tuning how final check works for really hard problems
option exportDioDecompositions --dio-decomps bool :default false :read-write
- Let skolem variables for integer divisibility constraints leak from the dio solver.
+ let skolem variables for integer divisibility constraints leak from the dio solver
option newProp --new-prop bool :default false :read-write
- Use the new row propagation system
+ use the new row propagation system
option arithPropAsLemmaLength --arith-prop-clauses uint16_t :default 8 :read-write
- Rows shorter than this are propagated as clauses
+ rows shorter than this are propagated as clauses
option soiQuickExplain --soi-qe bool :default false :read-write
- Use quick explain to minimize the sum of infeasibility conflicts.
+ use quick explain to minimize the sum of infeasibility conflicts
option rewriteDivk rewrite-divk --rewrite-divk bool :default false
rewrite division and mod when by a constant into linear terms
}
/**
- * Determines the appropraite WitnessImprovement for the update.
+ * Determines the appropriate WitnessImprovement for the update.
* useBlands breaks ties for degenerate pivots.
*
* This is safe if:
}
-// neeed a better name, this is not technically a ground term
+// need a better name, this is not technically a ground term
inline bool isBVGroundTerm(TNode node) {
if (node.getNumChildren() == 0) {
return node.isConst();
+/********************* */
+/*! \file idl_assertion.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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/idl/idl_assertion.h"
using namespace CVC4;
+/********************* */
+/*! \file idl_assertion.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
+ **/
+
#pragma once
#include "theory/idl/idl_model.h"
+/********************* */
+/*! \file idl_assertion_db.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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/idl/idl_assertion_db.h"
using namespace CVC4;
+/********************* */
+/*! \file idl_assertion_db.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
+ **/
+
#pragma once
#include "theory/idl/idl_assertion.h"
+/********************* */
+/*! \file idl_model.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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/idl/idl_model.h"
using namespace CVC4;
+/********************* */
+/*! \file idl_model.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
+ **/
+
#pragma once
#include "expr/node.h"
+/********************* */
+/*! \file theory_idl.cpp
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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/idl/theory_idl.h"
#include "theory/idl/options.h"
#include "theory/rewriter.h"
+/********************* */
+/*! \file theory_idl.h
+ ** \verbatim
+ ** Original author: Dejan Jovanovic
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2013 New York University and The University of Iowa
+ ** 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
+ **/
+
#pragma once
#include "cvc4_private.h"
}
hash_map<Node, bool, NodeHashFunction>::iterator it;
- it = d_containsTermITECache.find(e);
+ it = d_containsTermITECache.find(e);
if (it != d_containsTermITECache.end()) {
return (*it).second;
}
}
hash_map<Node, bool, NodeHashFunction>::iterator it;
- it = d_leavesConstCache.find(e);
+ it = d_leavesConstCache.find(e);
if (it != d_leavesConstCache.end()) {
return (*it).second;
}
#include "util/ite_removal.h"
namespace CVC4 {
+namespace theory {
class ITESimplifier {
Node d_true;
};
-}
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
#endif
/** Demands that the search restart from sat search level 0.
* Using this leads to non-termination issues.
- * It is appropraite for prototyping for theories.
+ * It is appropriate for prototyping for theories.
*/
virtual void demandRestart() throw(TypeCheckingExceptionPrivate, AssertionException) {}
//get relevant domain
RelevantDomain * getRelevantDomain() { return d_rel_dom; }
//get the builder
- QModelBuilder * getModelBuilder() { return d_builder; }
+ QModelBuilder* getModelBuilder() { return d_builder; }
public:
void check( Theory::Effort e );
void registerQuantifier( Node f );
// Variables
if (node.isVar()) {
if (theoryOf(node.getType()) != theory::THEORY_BOOL) {
- // We treat the varibables as uninterpreted
+ // We treat the variables as uninterpreted
return s_uninterpretedSortOwner;
} else {
// Except for the Boolean ones, which we just ignore anyhow
virtual EqualityStatus getEqualityStatus(TNode a, TNode b) { return EQUALITY_UNKNOWN; }
/**
- * Return the model value of the give shared term (or null if not avalilable.
+ * Return the model value of the give shared term (or null if not available).
*/
virtual Node getModelValue(TNode var) { return Node::null(); }
}
}
if (multipleTheories) {
- // Collect the shared terms if there are multipe theories
+ // Collect the shared terms if there are multiple theories
NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
}
}
d_iteRemover.run(additionalLemmas, iteSkolemMap);
additionalLemmas[0] = theory::Rewriter::rewrite(additionalLemmas[0]);
- if(Trace.isOn("lemma-ites")) {
+ if(Debug.isOn("lemma-ites")) {
Debug("lemma-ites") << "removed ITEs from lemma: " << node << endl;
Debug("lemma-ites") << " + now have the following "
<< additionalLemmas.size() << " lemma(s):" << endl;
Debug("theory::explain") << "TheoryEngine::explain(): processing [" << toExplain.timestamp << "] " << toExplain.node << " sent from " << toExplain.theory << endl;
- // If a treu constant or a negation of a false constant we can ignore it
+ // If a true constant or a negation of a false constant we can ignore it
if (toExplain.node.isConst() && toExplain.node.getConst<bool>()) {
++ i;
continue;
void dumpAssertions(const char* tag);
/** For preprocessing pass simplifying ITEs */
- ITESimplifier d_iteSimplifier;
+ theory::ITESimplifier d_iteSimplifier;
/** For preprocessing pass simplifying unconstrained expressions */
UnconstrainedSimplifier d_unconstrainedSimp;
/**
* Adds a predicate p with given polarity. The predicate asserted
* should be in the congruence closure kinds (otherwise it's
- * useless.
+ * useless).
*
* @param p the (non-negated) predicate
* @param polarity true if asserting the predicate, false if
void getUseListTerms(TNode t, std::set<TNode>& output);
/**
- * Get an explanation of the equality t1 = t2 begin true of false.
+ * Get an explanation of the equality t1 = t2 being true or false.
* Returns the reasons (added when asserting) that imply it
* in the assertions vector.
*/
%ignore CVC4::operator<<(std::ostream&, enum Result::UnknownExplanation);
%ignore CVC4::operator==(enum Result::Sat, const Result&);
-%ignore CVC4::operator==(enum Result::Validity, const Result&);
%ignore CVC4::operator!=(enum Result::Sat, const Result&);
+
+%ignore CVC4::operator==(enum Result::Validity, const Result&);
%ignore CVC4::operator!=(enum Result::Validity, const Result&);
%include "util/result.h"
* like in this example, which takes the place of the declaration of a
* statistics field "d_checkTimer":
*
- * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::morgan::checkTime");
+ * KEEP_STATISTIC(TimerStat, d_checkTimer, "theory::uf::checkTime");
*
* If any args need to be passed to the constructor, you can specify
* them after the string.
projects / cvc5.git / commitdiff