summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--NEWS6
-rw-r--r--src/decision/justification_heuristic.cpp2
-rw-r--r--src/decision/options_handlers.h2
-rw-r--r--src/expr/attribute.cpp2
-rw-r--r--src/expr/attribute_unique_id.h2
-rw-r--r--src/expr/command.cpp2
-rw-r--r--src/expr/command.h4
-rw-r--r--src/expr/expr_template.h4
-rw-r--r--src/expr/node.h2
-rw-r--r--src/expr/node_value.cpp7
-rw-r--r--src/expr/node_value.h2
-rw-r--r--src/expr/type_node.h9
-rw-r--r--src/main/portfolio.cpp2
-rw-r--r--src/parser/smt2/Smt2.g6
-rw-r--r--src/printer/cvc/cvc_printer.cpp2
-rw-r--r--src/printer/printer.h16
-rw-r--r--src/theory/arith/options_handlers.h2
-rw-r--r--src/theory/bv/theory_bv_utils.h1
-rw-r--r--src/theory/idl/idl_assertion_db.h2
-rw-r--r--src/theory/idl/idl_model.h2
-rw-r--r--src/theory/strings/regexp_operation.h4
-rw-r--r--src/theory/strings/theory_strings.cpp8
-rw-r--r--src/theory/strings/theory_strings.h12
-rw-r--r--src/theory/theory_engine.h2
-rw-r--r--src/util/backtrackable.h2
-rw-r--r--src/util/bool.h10
-rw-r--r--test/unit/expr/expr_public.h13
-rw-r--r--test/unit/expr/node_black.h12
28 files changed, 83 insertions, 57 deletions
diff --git a/NEWS b/NEWS
index 74b9a6c0a..d30c0ab77 100644
--- a/NEWS
+++ b/NEWS
@@ -14,6 +14,12 @@ Changes since 1.3
of CVC4.
* Small API adjustments to Datatypes to even out the API and make it
function better in Java.
+* Better automatic handling of output language setting when using CVC4
+ via API. Previously, the "automatic" language setting was sometimes
+ (though not always) defaulting to the internal "AST" language; it
+ should now (correctly) default to the same as the input language
+ (if the input language is supported as an output language), or the
+ "CVC4" native output language if no input language setting is applied.
Changes since 1.2
=================
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"
diff --git a/test/unit/expr/expr_public.h b/test/unit/expr/expr_public.h
index 7f6385d36..4a9d73cb7 100644
--- a/test/unit/expr/expr_public.h
+++ b/test/unit/expr/expr_public.h
@@ -30,6 +30,8 @@ using namespace std;
class ExprPublic : public CxxTest::TestSuite {
private:
+ Options opts;
+
ExprManager* d_em;
Expr* a_bool;
@@ -51,7 +53,14 @@ public:
void setUp() {
try {
- d_em = new ExprManager;
+ char *argv[2];
+ argv[0] = strdup("");
+ argv[1] = strdup("--output-language=ast");
+ opts.parseOptions(2, argv);
+ free(argv[0]);
+ free(argv[1]);
+
+ d_em = new ExprManager(opts);
a_bool = new Expr(d_em->mkVar("a",d_em->booleanType()));
b_bool = new Expr(d_em->mkVar("b", d_em->booleanType()));
@@ -61,7 +70,7 @@ public:
fun_type = new Type(d_em->mkFunctionType(d_em->booleanType(), d_em->booleanType()));
fun_op = new Expr(d_em->mkVar("f", *fun_type));
d_apply_fun_bool = new Expr(d_em->mkExpr(APPLY_UF, *fun_op, *a_bool));
- null = new Expr;
+ null = new Expr();
i1 = new Expr(d_em->mkConst(Rational("0")));
i2 = new Expr(d_em->mkConst(Rational(23)));
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h
index 8e8263fe7..6cf85fb7e 100644
--- a/test/unit/expr/node_black.h
+++ b/test/unit/expr/node_black.h
@@ -34,6 +34,7 @@ using namespace std;
class NodeBlack : public CxxTest::TestSuite {
private:
+ Options opts;
Context* d_ctxt;
NodeManager* d_nodeManager;
NodeManagerScope* d_scope;
@@ -43,8 +44,15 @@ private:
public:
void setUp() {
- d_ctxt = new Context;
- d_nodeManager = new NodeManager(d_ctxt, NULL);
+ char *argv[2];
+ argv[0] = strdup("");
+ argv[1] = strdup("--output-language=ast");
+ opts.parseOptions(2, argv);
+ free(argv[0]);
+ free(argv[1]);
+
+ d_ctxt = new Context();
+ d_nodeManager = new NodeManager(d_ctxt, NULL, opts);
d_scope = new NodeManagerScope(d_nodeManager);
d_booleanType = new TypeNode(d_nodeManager->booleanType());
d_realType = new TypeNode(d_nodeManager->realType());
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback