diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/decision/justification_heuristic.cpp | 2 | ||||
-rw-r--r-- | src/decision/options_handlers.h | 2 | ||||
-rw-r--r-- | src/expr/attribute.cpp | 2 | ||||
-rw-r--r-- | src/expr/attribute_unique_id.h | 2 | ||||
-rw-r--r-- | src/expr/command.cpp | 2 | ||||
-rw-r--r-- | src/expr/command.h | 4 | ||||
-rw-r--r-- | src/expr/expr_template.h | 4 | ||||
-rw-r--r-- | src/expr/node.h | 2 | ||||
-rw-r--r-- | src/expr/node_value.cpp | 7 | ||||
-rw-r--r-- | src/expr/node_value.h | 2 | ||||
-rw-r--r-- | src/expr/type_node.h | 9 | ||||
-rw-r--r-- | src/main/portfolio.cpp | 2 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 6 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 2 | ||||
-rw-r--r-- | src/printer/printer.h | 16 | ||||
-rw-r--r-- | src/theory/arith/options_handlers.h | 2 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_utils.h | 1 | ||||
-rw-r--r-- | src/theory/idl/idl_assertion_db.h | 2 | ||||
-rw-r--r-- | src/theory/idl/idl_model.h | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 8 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 12 | ||||
-rw-r--r-- | src/theory/theory_engine.h | 2 | ||||
-rw-r--r-- | src/util/backtrackable.h | 2 | ||||
-rw-r--r-- | src/util/bool.h | 10 |
25 files changed, 56 insertions, 53 deletions
diff --git a/src/decision/justification_heuristic.cpp b/src/decision/justification_heuristic.cpp index 78de1a74e..54d2dee97 100644 --- a/src/decision/justification_heuristic.cpp +++ b/src/decision/justification_heuristic.cpp @@ -106,7 +106,7 @@ CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, D if(litDecision != undefSatLiteral) { setPrvsIndex(i); - Trace("decision") << "jh: spliting on " << litDecision << std::endl; + Trace("decision") << "jh: splitting on " << litDecision << std::endl; return litDecision; } } diff --git a/src/decision/options_handlers.h b/src/decision/options_handlers.h index f538ba947..a8931aecb 100644 --- a/src/decision/options_handlers.h +++ b/src/decision/options_handlers.h @@ -29,7 +29,7 @@ static const std::string decisionModeHelp = "\ 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\ diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp index 86768500b..cde261463 100644 --- a/src/expr/attribute.cpp +++ b/src/expr/attribute.cpp @@ -128,7 +128,7 @@ void AttributeManager::deleteAttributes(const AttrIdVec& atids){ case AttrTableCDNode: case AttrTableCDString: case AttrTableCDPointer: - Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behaviour is desired."); + Unimplemented("CDAttributes cannot be deleted. Contact Tim/Morgan if this behavior is desired."); break; case LastAttrTable: default: diff --git a/src/expr/attribute_unique_id.h b/src/expr/attribute_unique_id.h index 08b31a4c0..3a52d7a89 100644 --- a/src/expr/attribute_unique_id.h +++ b/src/expr/attribute_unique_id.h @@ -46,7 +46,7 @@ enum AttrTableId { }; /** - * This uniquely indentifies attributes across tables. + * This uniquely identifies attributes across tables. */ class AttributeUniqueId { AttrTableId d_tableId; diff --git a/src/expr/command.cpp b/src/expr/command.cpp index 0b664ceb4..9341c9828 100644 --- a/src/expr/command.cpp +++ b/src/expr/command.cpp @@ -467,7 +467,7 @@ Command* CommandSequence::exportTo(ExprManager* exprManager, ExprManagerMapColle Command* cmd_to_export = *i; Command* cmd = cmd_to_export->exportTo(exprManager, variableMap); seq->addCommand(cmd); - Debug("export") << "[export] so far coverted: " << seq << endl; + Debug("export") << "[export] so far converted: " << seq << endl; } seq->d_index = d_index; return seq; diff --git a/src/expr/command.h b/src/expr/command.h index a3d58e5dd..0d173faf6 100644 --- a/src/expr/command.h +++ b/src/expr/command.h @@ -156,7 +156,7 @@ protected: public: virtual ~CommandStatus() throw() {} void toStream(std::ostream& out, - OutputLanguage language = language::output::LANG_AST) const throw(); + OutputLanguage language = language::output::LANG_AUTO) const throw(); virtual CommandStatus& clone() const = 0; };/* class CommandStatus */ @@ -211,7 +211,7 @@ public: virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw(); virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AST) const throw(); + OutputLanguage language = language::output::LANG_AUTO) const throw(); std::string toString() const throw(); diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h index 0c7acce9c..828b1923c 100644 --- a/src/expr/expr_template.h +++ b/src/expr/expr_template.h @@ -459,7 +459,7 @@ public: * @param language the language in which to output */ void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AST) const; + OutputLanguage language = language::output::LANG_AUTO) const; /** * Check if this is a null expression. @@ -861,7 +861,7 @@ class CVC4_PUBLIC ExprSetLanguage { * setlanguage() applied to them and where the current Options * information isn't available. */ - static const int s_defaultOutputLanguage = language::output::LANG_AST; + static const int s_defaultOutputLanguage = language::output::LANG_AUTO; /** * When this manipulator is used, the setting is stored here. diff --git a/src/expr/node.h b/src/expr/node.h index a6914aedb..e7c51f0e2 100644 --- a/src/expr/node.h +++ b/src/expr/node.h @@ -815,7 +815,7 @@ public: * @param language the language in which to output */ inline void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage language = language::output::LANG_AST) const { + OutputLanguage language = language::output::LANG_AUTO) const { assertTNodeNotExpired(); d_nv->toStream(out, toDepth, types, dag, language); } diff --git a/src/expr/node_value.cpp b/src/expr/node_value.cpp index ed7a8add3..d5b08bc18 100644 --- a/src/expr/node_value.cpp +++ b/src/expr/node_value.cpp @@ -37,11 +37,8 @@ NodeValue NodeValue::s_null(0); string NodeValue::toString() const { stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage(); - toStream(ss, -1, false, false, - outlang == language::output::LANG_AUTO ? - language::output::LANG_AST : - outlang); + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + toStream(ss, -1, false, false, outlang); return ss.str(); } diff --git a/src/expr/node_value.h b/src/expr/node_value.h index 5c73b39b5..85abca524 100644 --- a/src/expr/node_value.h +++ b/src/expr/node_value.h @@ -268,7 +268,7 @@ public: std::string toString() const; void toStream(std::ostream& out, int toDepth = -1, bool types = false, size_t dag = 1, - OutputLanguage = language::output::LANG_AST) const; + OutputLanguage = language::output::LANG_AUTO) const; static inline unsigned kindToDKind(Kind k) { return ((unsigned) k) & kindMask; diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1dd0ffed1..c823190bf 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -374,11 +374,8 @@ public: */ inline std::string toString() const { std::stringstream ss; - OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AST : options::outputLanguage(); - d_nv->toStream(ss, -1, false, 0, - outlang == language::output::LANG_AUTO ? - language::output::LANG_AST : - outlang); + OutputLanguage outlang = (this == &s_null) ? language::output::LANG_AUTO : options::outputLanguage(); + d_nv->toStream(ss, -1, false, 0, outlang); return ss.str(); } @@ -389,7 +386,7 @@ public: * @param out the stream to serialize this node to * @param language the language in which to output */ - inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AST) const { + inline void toStream(std::ostream& out, OutputLanguage language = language::output::LANG_AUTO) const { d_nv->toStream(out, -1, false, 0, language); } diff --git a/src/main/portfolio.cpp b/src/main/portfolio.cpp index 56a05795a..21c1b60a3 100644 --- a/src/main/portfolio.cpp +++ b/src/main/portfolio.cpp @@ -38,7 +38,7 @@ int global_winner; template<typename S> void runThread(int thread_id, boost::function<S()> threadFn, S& returnValue) { - /* Uncommment line to delay first thread, useful to unearth errors/debug */ + /* Uncomment line to delay first thread, useful to unearth errors/debug */ // if(thread_id == 0) { sleep(1); } returnValue = threadFn(); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index e2e52b158..13850aba6 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -336,8 +336,10 @@ command returns [CVC4::Command* cmd = NULL] } | /* value query */ GET_VALUE_TOK { PARSER_STATE->checkThatLogicIsSet(); } - LPAREN_TOK termList[terms,expr] RPAREN_TOK - { $cmd = new GetValueCommand(terms); } + ( LPAREN_TOK termList[terms,expr] RPAREN_TOK + { $cmd = new GetValueCommand(terms); } + | term[expr, expr2] + { PARSER_STATE->parseError("The get-value command expects a list of terms. Perhaps you forgot a pair of parentheses?"); } ) | /* get-assignment */ GET_ASSIGNMENT_TOK { PARSER_STATE->checkThatLogicIsSet(); } { cmd = new GetAssignmentCommand(); } diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index 49ded4ecb..ca463d10b 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -80,7 +80,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo // null if(n.getKind() == kind::NULL_EXPR) { - out << "NULL"; + out << "null"; return; } diff --git a/src/printer/printer.h b/src/printer/printer.h index a7ae8c447..9ddac096d 100644 --- a/src/printer/printer.h +++ b/src/printer/printer.h @@ -54,7 +54,21 @@ public: /** Get the Printer for a given OutputLanguage */ static Printer* getPrinter(OutputLanguage lang) throw() { if(lang == language::output::LANG_AUTO) { - lang = language::output::LANG_CVC4; // default + // Infer the language to use for output. + // + // Options can be null in certain circumstances (e.g., when printing + // the singleton "null" expr. So we guard against segfault + if(&Options::current() != NULL) { + if(options::outputLanguage.wasSetByUser()) { + lang = options::outputLanguage(); + } + if(lang == language::output::LANG_AUTO && options::inputLanguage.wasSetByUser()) { + lang = language::toOutputLanguage(options::inputLanguage()); + } + } + if(lang == language::output::LANG_AUTO) { + lang = language::output::LANG_CVC4; // default + } } if(d_printers[lang] == NULL) { d_printers[lang] = makePrinter(lang); diff --git a/src/theory/arith/options_handlers.h b/src/theory/arith/options_handlers.h index a72ced0bc..f81f1b227 100644 --- a/src/theory/arith/options_handlers.h +++ b/src/theory/arith/options_handlers.h @@ -52,7 +52,7 @@ This decides on kind of propagation arithmetic attempts to do during the search. "; static const std::string errorSelectionRulesHelp = "\ -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\ Heuristic pivot rules available:\n\ +min\n\ diff --git a/src/theory/bv/theory_bv_utils.h b/src/theory/bv/theory_bv_utils.h index 5140bd498..f35fc2896 100644 --- a/src/theory/bv/theory_bv_utils.h +++ b/src/theory/bv/theory_bv_utils.h @@ -25,7 +25,6 @@ #include "expr/node_manager.h" #include "theory/decision_attributes.h" - namespace CVC4 { namespace theory { namespace bv { diff --git a/src/theory/idl/idl_assertion_db.h b/src/theory/idl/idl_assertion_db.h index 205102b0f..358a5386e 100644 --- a/src/theory/idl/idl_assertion_db.h +++ b/src/theory/idl/idl_assertion_db.h @@ -35,7 +35,7 @@ class IDLAssertionDB { struct IDLAssertionListElement { /** The assertion itself */ IDLAssertion d_assertion; - /** The inndex of the previous element (-1 for null) */ + /** The index of the previous element (-1 for null) */ unsigned d_previous; IDLAssertionListElement(const IDLAssertion& assertion, unsigned previous) diff --git a/src/theory/idl/idl_model.h b/src/theory/idl/idl_model.h index 22e05c469..c69a0c38f 100644 --- a/src/theory/idl/idl_model.h +++ b/src/theory/idl/idl_model.h @@ -33,7 +33,7 @@ namespace idl { struct IDLReason { /** The variable of the reason */ TNode x; - /** The constraint of the reaason */ + /** The constraint of the reason */ TNode constraint; IDLReason(TNode x, TNode constraint) diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index a47f7bd77..9ed4be0c3 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief Regular Expresion Operations
+ ** \brief Regular Expression Operations
**
- ** Regular Expresion Operations
+ ** Regular Expression Operations
**/
#include "cvc4_private.h"
diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 9f4d84765..62e71327e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -218,7 +218,7 @@ void TheoryStrings::collectModelInfo( TheoryModel* m, bool fullModel ) { std::map< Node, Node > processed; std::vector< std::vector< Node > > col; std::vector< Node > lts; - seperateByLength( nodes, col, lts ); + separateByLength( nodes, col, lts ); //step 1 : get all values for known lengths std::vector< Node > lts_values; std::map< unsigned, bool > values_used; @@ -1667,7 +1667,7 @@ bool TheoryStrings::checkNormalForms() { getEquivalenceClasses( eqcs ); std::vector< std::vector< Node > > cols; std::vector< Node > lts; - seperateByLength( eqcs, cols, lts ); + separateByLength( eqcs, cols, lts ); for( unsigned i=0; i<cols.size(); i++ ){ if( cols[i].size()>1 && d_lemma_cache.empty() ){ Trace("strings-solve") << "- Verify disequalities are processed for "; @@ -1745,7 +1745,7 @@ bool TheoryStrings::checkCardinality() { std::vector< std::vector< Node > > cols; std::vector< Node > lts; - seperateByLength( eqcs, cols, lts ); + separateByLength( eqcs, cols, lts ); for( unsigned i = 0; i<cols.size(); ++i ){ Node lr = lts[i]; @@ -1862,7 +1862,7 @@ void TheoryStrings::getFinalNormalForm( Node n, std::vector< Node >& nf, std::ve } } -void TheoryStrings::seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols, +void TheoryStrings::separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& cols, std::vector< Node >& lts ) { unsigned leqc_counter = 0; std::map< Node, unsigned > eqc_to_leqc; diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index 4d2a192cf..875f407c5 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -188,7 +188,7 @@ private: /** map from representatives to information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; EqcInfo * getOrMakeEqcInfo( Node eqc, bool doMake = true ); - //maintain which concat terms have the length lemma instantiatied + //maintain which concat terms have the length lemma instantiated std::map< Node, bool > d_length_inst; private: bool getNormalForms(Node &eqc, std::vector< Node > & visited, std::vector< Node > & nf, @@ -223,11 +223,11 @@ public: /** Conflict when merging two constants */ void conflict(TNode a, TNode b); - /** called when a new equivalance class is created */ + /** called when a new equivalence class is created */ void eqNotifyNewClass(TNode t); - /** called when two equivalance classes will merge */ + /** called when two equivalence classes will merge */ void eqNotifyPreMerge(TNode t1, TNode t2); - /** called when two equivalance classes have merged */ + /** called when two equivalence classes have merged */ void eqNotifyPostMerge(TNode t1, TNode t2); /** called when two equivalence classes are made disequal */ void eqNotifyDisequal(TNode t1, TNode t2, TNode reason); @@ -255,8 +255,8 @@ protected: //get final normal form void getFinalNormalForm( Node n, std::vector< Node >& nf, std::vector< Node >& exp ); - //seperate into collections with equal length - void seperateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); + //separate into collections with equal length + void separateByLength( std::vector< Node >& n, std::vector< std::vector< Node > >& col, std::vector< Node >& lts ); void printConcat( std::vector< Node >& n, const char * c ); // Measurement diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index ffc36e59b..92469aa31 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -749,7 +749,7 @@ public: theory::EqualityStatus getEqualityStatus(TNode a, TNode b); /** - * Retruns the value that a theory that owns the type of var currently + * Returns the value that a theory that owns the type of var currently * has (or null if none); */ Node getModelValue(TNode var); diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h index c5844c6c4..57ed94771 100644 --- a/src/util/backtrackable.h +++ b/src/util/backtrackable.h @@ -170,7 +170,7 @@ void List<T>::concat (List<T>* other) { template <class T> void List<T>::unconcat(List<T>* other) { // we do not need to check consistency since this is only called by the - //Backtracker when we are inconsistent + // Backtracker when we are inconsistent Assert(other->ptr_to_head != NULL); other->ptr_to_head->next = NULL; tail = other->ptr_to_head; diff --git a/src/util/bool.h b/src/util/bool.h index 8e3c8849c..373b4fdec 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -9,15 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief A multi-precision rational constant. + ** \brief A hash function for Boolean ** - ** 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 consequence is that that the numerator and denominator may be - ** different than the values used to construct the Rational. + ** A hash function for Boolean. **/ #include "cvc4_public.h" |