diff options
author | Tim King <taking@cs.nyu.edu> | 2012-12-14 20:13:53 -0500 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2012-12-14 20:13:53 -0500 |
commit | 52b4d02428cb002a612d3e286c68a556098e8104 (patch) | |
tree | fe83aa96fe8c256617db6d8b154eee131879f50e | |
parent | edf971e2934367d160830a35e97a2e664e742b28 (diff) | |
parent | 62e9f6d0a34d4f6623381429b51b65ddfae1e86d (diff) |
Merge remote-tracking branch 'main-repo/1.0.x' into 1.0.x
-rw-r--r-- | config/.gitignore | 1 | ||||
-rw-r--r-- | src/parser/parser.cpp | 9 | ||||
-rw-r--r-- | src/parser/parser.h | 6 | ||||
-rw-r--r-- | src/parser/smt2/Smt2.g | 43 | ||||
-rw-r--r-- | src/printer/cvc/cvc_printer.cpp | 6 | ||||
-rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 23 | ||||
-rw-r--r-- | src/theory/bv/bitblast_strategies.cpp | 22 | ||||
-rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h | 4 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 50 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_attributes.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/theory_quantifiers.h | 2 | ||||
-rw-r--r-- | src/util/bitvector.h | 18 | ||||
-rw-r--r-- | test/Makefile.am | 22 | ||||
-rw-r--r-- | test/regress/regress0/Makefile.am | 3 | ||||
-rw-r--r-- | test/regress/regress0/bug480.smt2 | 11 | ||||
-rwxr-xr-x | test/unit/no_cxxtest | 6 |
20 files changed, 168 insertions, 68 deletions
diff --git a/config/.gitignore b/config/.gitignore index dfeb8c222..c1e3d2423 100644 --- a/config/.gitignore +++ b/config/.gitignore @@ -9,3 +9,4 @@ /missing /ltoptions.m4 /install-sh +/test-driver diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 721dedc70..65d46220b 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -16,6 +16,7 @@ #include <iostream> #include <fstream> +#include <sstream> #include <iterator> #include <stdint.h> #include <cassert> @@ -500,6 +501,14 @@ Expr Parser::nextExpression() throw(ParserException) { return result; } +void Parser::attributeNotSupported(const std::string& attr) { + if(d_attributesWarnedAbout.find(attr) == d_attributesWarnedAbout.end()) { + stringstream ss; + ss << "warning: Attribute " << attr << " not supported (ignoring this and all following uses)"; + d_input->warning(ss.str()); + d_attributesWarnedAbout.insert(attr); + } +} }/* CVC4::parser namespace */ }/* CVC4 namespace */ diff --git a/src/parser/parser.h b/src/parser/parser.h index fc956b463..958c8a5b5 100644 --- a/src/parser/parser.h +++ b/src/parser/parser.h @@ -144,6 +144,9 @@ class CVC4_PUBLIC Parser { /** The set of operators available in the current logic. */ std::set<Kind> d_logicOperators; + /** The set of attributes already warned about. */ + std::set<std::string> d_attributesWarnedAbout; + /** * The current set of unresolved types. We can get by with this NOT * being on the scope, because we can only have one DATATYPE @@ -451,6 +454,9 @@ public: d_input->warning(msg); } + /** Issue a warning to the user, but only once per attribute. */ + void attributeNotSupported(const std::string& attr); + /** Raise a parse error with the given message. */ inline void parseError(const std::string& msg) throw(ParserException) { d_input->parseError(msg); diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 87cf2083d..648666091 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -629,7 +629,7 @@ pattern[CVC4::Expr& expr] } ; -simpleSymbolicExpr[CVC4::SExpr& sexpr] +simpleSymbolicExprNoKeyword[CVC4::SExpr& sexpr] @declarations { CVC4::Kind k; std::string s; @@ -647,6 +647,10 @@ simpleSymbolicExpr[CVC4::SExpr& sexpr] ss << Expr::setlanguage(CVC4::language::output::LANG_SMTLIB_V2) << EXPR_MANAGER->mkConst(k); sexpr = SExpr(ss.str()); } + ; + +simpleSymbolicExpr[CVC4::SExpr& sexpr] + : simpleSymbolicExprNoKeyword[sexpr] | KEYWORD { sexpr = SExpr(AntlrInput::tokenText($KEYWORD)); } ; @@ -715,8 +719,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2] expr = MK_EXPR(kind, args); } } - | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK - { + | LPAREN_TOK AS_TOK term[f, f2] sortSymbol[type, CHECK_DECLARED] RPAREN_TOK + { if(f.getKind() == CVC4::kind::APPLY_CONSTRUCTOR && type.isDatatype()) { std::vector<CVC4::Expr> v; Expr e = f.getOperator(); @@ -928,22 +932,31 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] Expr patexpr; std::vector<Expr> patexprs; Expr e2; + bool hasValue = false; } -: KEYWORD + : KEYWORD ( simpleSymbolicExprNoKeyword[sexpr] { hasValue = true; } )? { attr = AntlrInput::tokenText($KEYWORD); - //EXPR_MANAGER->setNamedAttribute( expr, attr ); - if( attr==":rewrite-rule" ){ - //do nothing - } else if( attr==":axiom" || attr==":conjecture" ){ + // EXPR_MANAGER->setNamedAttribute( expr, attr ); + if(attr == ":rewrite-rule") { + if(hasValue) { + std::stringstream ss; + ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; + PARSER_STATE->warning(ss.str()); + } + // do nothing + } else if(attr == ":axiom" || attr == ":conjecture") { + if(hasValue) { + std::stringstream ss; + ss << "warning: Attribute " << attr << " does not take a value (ignoring)"; + PARSER_STATE->warning(ss.str()); + } std::string attr_name = attr; attr_name.erase( attr_name.begin() ); Command* c = new SetUserAttributeCommand( attr_name, expr ); PARSER_STATE->preemptCommand(c); } else { - std::stringstream ss; - ss << "Attribute `" << attr << "' not supported"; - PARSER_STATE->parseError(ss.str()); + PARSER_STATE->attributeNotSupported(attr); } } | ATTRIBUTE_PATTERN_TOK LPAREN_TOK ( term[patexpr, e2] { patexprs.push_back( patexpr ); } )+ RPAREN_TOK @@ -951,6 +964,11 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr] attr = std::string(":pattern"); retExpr = MK_EXPR(kind::INST_PATTERN, patexprs); } + | ATTRIBUTE_NO_PATTERN_TOK LPAREN_TOK term[patexpr, e2]+ RPAREN_TOK + { + attr = std::string(":no-pattern"); + PARSER_STATE->attributeNotSupported(attr); + } | ATTRIBUTE_NAMED_TOK symbolicExpr[sexpr] { attr = std::string(":named"); @@ -1098,7 +1116,7 @@ quantOp[CVC4::Kind& kind] @init { Debug("parser") << "quant: " << AntlrInput::tokenText(LT(1)) << std::endl; } - : EXISTS_TOK { $kind = CVC4::kind::EXISTS; } + : EXISTS_TOK { $kind = CVC4::kind::EXISTS; } | FORALL_TOK { $kind = CVC4::kind::FORALL; } ; @@ -1374,6 +1392,7 @@ SIMPLIFY_TOK : 'simplify'; // attributes ATTRIBUTE_PATTERN_TOK : ':pattern'; +ATTRIBUTE_NO_PATTERN_TOK : ':no-pattern'; ATTRIBUTE_NAMED_TOK : ':named'; // operators (NOTE: theory symbols go here) diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp index f0a936c97..ecc224026 100644 --- a/src/printer/cvc/cvc_printer.cpp +++ b/src/printer/cvc/cvc_printer.cpp @@ -493,9 +493,15 @@ void CvcPrinter::toStream(std::ostream& out, TNode n, int depth, bool types, boo case kind::BITVECTOR_UDIV: op << "BVUDIV"; break; + case kind::BITVECTOR_UDIV_TOTAL: + op << "BVUDIV_TOTAL"; + break; case kind::BITVECTOR_UREM: op << "BVUREM"; break; + case kind::BITVECTOR_UREM_TOTAL: + op << "BVUREM_TOTAL"; + break; case kind::BITVECTOR_SDIV: op << "BVSDIV"; break; diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 5985f38ef..5821fbc77 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -254,7 +254,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n, case kind::BITVECTOR_SUB: out << "bvsub "; break; case kind::BITVECTOR_NEG: out << "bvneg "; break; case kind::BITVECTOR_UDIV: out << "bvudiv "; break; + case kind::BITVECTOR_UDIV_TOTAL: out << "bvudiv_total "; break; case kind::BITVECTOR_UREM: out << "bvurem "; break; + case kind::BITVECTOR_UREM_TOTAL: out << "bvurem_total "; break; case kind::BITVECTOR_SDIV: out << "bvsdiv "; break; case kind::BITVECTOR_SREM: out << "bvsrem "; break; case kind::BITVECTOR_SMOD: out << "bvsmod "; break; diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c82b7ca2c..77e43d518 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -631,6 +631,11 @@ void SmtEngine::finalOptionsAreSet() { } } + if(options::produceAssignments() && !options::produceModels()) { + Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << std::endl; + setOption("produce-models", SExpr("true")); + } + if(! d_logic.isLocked()) { // ensure that our heuristics are properly set up setLogicInternal(); @@ -2705,20 +2710,22 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { vector<SExpr> sexprs; TypeNode boolType = d_nodeManager->booleanType(); + TheoryModel* m = d_theoryEngine->getModel(); for(AssignmentSet::const_iterator i = d_assignments->begin(), iend = d_assignments->end(); i != iend; ++i) { Assert((*i).getType() == boolType); - // Normalize - Node n = Rewriter::rewrite(*i); + // Expand, then normalize + hash_map<Node, Node, NodeHashFunction> cache; + Node n = d_private->expandDefinitions(*i, cache); + n = Rewriter::rewrite(n); Trace("smt") << "--- getting value of " << n << endl; - TheoryModel* m = d_theoryEngine->getModel(); Node resultNode; - if( m ){ - resultNode = m->getValue( n ); + if(m != NULL) { + resultNode = m->getValue(n); } // type-check the result we got @@ -2727,12 +2734,12 @@ CVC4::SExpr SmtEngine::getAssignment() throw(ModalException) { vector<SExpr> v; if((*i).getKind() == kind::APPLY) { Assert((*i).getNumChildren() == 0); - v.push_back((*i).getOperator().toString()); + v.push_back(SExpr::Keyword((*i).getOperator().toString())); } else { Assert((*i).isVar()); - v.push_back((*i).toString()); + v.push_back(SExpr::Keyword((*i).toString())); } - v.push_back(resultNode.toString()); + v.push_back(SExpr::Keyword(resultNode.toString())); sexprs.push_back(v); } return SExpr(sexprs); diff --git a/src/theory/bv/bitblast_strategies.cpp b/src/theory/bv/bitblast_strategies.cpp index fbf9a45ee..c25c40c22 100644 --- a/src/theory/bv/bitblast_strategies.cpp +++ b/src/theory/bv/bitblast_strategies.cpp @@ -648,6 +648,17 @@ void DefaultUdivBB (TNode node, Bits& q, Bitblaster* bb) { Bits r; uDivModRec(a, b, q, r, getSize(node)); + // adding a special case for division by 0 + std::vector<Node> iszero; + for (unsigned i = 0; i < b.size(); ++i) { + iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); + } + Node b_is_0 = utils::mkAnd(iszero); + + for (unsigned i = 0; i < q.size(); ++i) { + q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]); + r[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), r[i]); + } // cache the remainder in case we need it later Node remainder = mkNode(kind::BITVECTOR_UREM_TOTAL, node[0], node[1]); @@ -664,6 +675,17 @@ void DefaultUremBB (TNode node, Bits& rem, Bitblaster* bb) { Bits q; uDivModRec(a, b, q, rem, getSize(node)); + // adding a special case for division by 0 + std::vector<Node> iszero; + for (unsigned i = 0; i < b.size(); ++i) { + iszero.push_back(utils::mkNode(kind::IFF, b[i], utils::mkFalse())); + } + Node b_is_0 = utils::mkAnd(iszero); + + for (unsigned i = 0; i < q.size(); ++i) { + q[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), q[i]); + rem[i] = utils::mkNode(kind::ITE, b_is_0, utils::mkFalse(), rem[i]); + } // cache the quotient in case we need it later Node quotient = mkNode(kind::BITVECTOR_UDIV_TOTAL, node[0], node[1]); diff --git a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h index 8b080d104..498378638 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h +++ b/src/theory/bv/theory_bv_rewrite_rules_constant_evaluation.h @@ -207,7 +207,7 @@ Node RewriteRule<EvalUdiv>::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule<EvalUdiv>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); BitVector b = node[1].getConst<BitVector>(); - BitVector res = a.unsignedDiv(b); + BitVector res = a.unsignedDivTotal(b); return utils::mkConst(res); } @@ -222,7 +222,7 @@ Node RewriteRule<EvalUrem>::apply(TNode node) { BVDebug("bv-rewrite") << "RewriteRule<EvalUrem>(" << node << ")" << std::endl; BitVector a = node[0].getConst<BitVector>(); BitVector b = node[1].getConst<BitVector>(); - BitVector res = a.unsignedRem(b); + BitVector res = a.unsignedRemTotal(b); return utils::mkConst(res); } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index e23d9deae..9da83ce41 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -45,7 +45,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), d_selector_apps( c ), d_labels( c ), - d_conflict( c, false ){ + d_conflict( c, false ), + d_collectTermsCache( c ){ // The kinds we are treating as function application in congruence d_equalityEngine.addFunctionKind(kind::APPLY_CONSTRUCTOR); @@ -758,31 +759,34 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ void TheoryDatatypes::collectTerms( Node n ) { - for( int i=0; i<(int)n.getNumChildren(); i++ ) { - collectTerms( n[i] ); - } - if( n.getKind() == APPLY_CONSTRUCTOR ){ - //we must take into account subterm relation when checking for cycles + if( d_collectTermsCache.find( n )==d_collectTermsCache.end() ){ + d_collectTermsCache[n] = true; for( int i=0; i<(int)n.getNumChildren(); i++ ) { - Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl; - bool result = d_cycle_check.addEdgeNode( n, n[i] ); - d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + collectTerms( n[i] ); } - }else if( n.getKind() == APPLY_SELECTOR ){ - if( d_selector_apps.find( n )==d_selector_apps.end() ){ - d_selector_apps[n] = false; - //we must also record which selectors exist - Debug("datatypes") << " Found selector " << n << endl; - if (n.getType().isBoolean()) { - d_equalityEngine.addTriggerPredicate( n ); - }else{ - d_equalityEngine.addTerm( n ); + if( n.getKind() == APPLY_CONSTRUCTOR ){ + //we must take into account subterm relation when checking for cycles + for( int i=0; i<(int)n.getNumChildren(); i++ ) { + Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl; + bool result = d_cycle_check.addEdgeNode( n, n[i] ); + d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); } - Node rep = getRepresentative( n[0] ); - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - if( !eqc->d_selectors ){ - eqc->d_selectors = true; - instantiate( eqc, rep ); + }else if( n.getKind() == APPLY_SELECTOR ){ + if( d_selector_apps.find( n )==d_selector_apps.end() ){ + d_selector_apps[n] = false; + //we must also record which selectors exist + Debug("datatypes") << " Found selector " << n << endl; + if (n.getType().isBoolean()) { + d_equalityEngine.addTriggerPredicate( n ); + }else{ + d_equalityEngine.addTerm( n ); + } + Node rep = getRepresentative( n[0] ); + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + if( !eqc->d_selectors ){ + eqc->d_selectors = true; + instantiate( eqc, rep ); + } } } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 90d82e255..9846e80f2 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -156,6 +156,8 @@ private: context::CDO<bool> d_conflict; /** The conflict node */ Node d_conflictNode; + /** cache for which terms we have called collectTerms(...) on */ + BoolMap d_collectTermsCache; /** pending assertions/merges */ std::vector< Node > d_pending; std::map< Node, Node > d_pending_exp; diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp index 493a49e54..2f6dc47db 100644 --- a/src/theory/quantifiers/quantifiers_attributes.cpp +++ b/src/theory/quantifiers/quantifiers_attributes.cpp @@ -22,7 +22,7 @@ using namespace CVC4::context; using namespace CVC4::theory;
using namespace CVC4::theory::quantifiers;
-void QuantifiersAttributes::setUserAttribute( std::string& attr, Node n ){
+void QuantifiersAttributes::setUserAttribute( const std::string& attr, Node n ){
if( n.getKind()==FORALL ){
if( attr=="axiom" ){
Trace("quant-attr") << "Set axiom " << n << std::endl;
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h index 822d6c59f..88bac8bc9 100644 --- a/src/theory/quantifiers/quantifiers_attributes.h +++ b/src/theory/quantifiers/quantifiers_attributes.h @@ -40,7 +40,7 @@ struct QuantifiersAttributes * This function will apply a custom set of attributes to all top-level universal
* quantifiers contained in n
*/
- static void setUserAttribute( std::string& attr, Node n );
+ static void setUserAttribute( const std::string& attr, Node n );
};
diff --git a/src/theory/quantifiers/theory_quantifiers.cpp b/src/theory/quantifiers/theory_quantifiers.cpp index cfdb30f38..b1a7c9927 100644 --- a/src/theory/quantifiers/theory_quantifiers.cpp +++ b/src/theory/quantifiers/theory_quantifiers.cpp @@ -192,6 +192,6 @@ bool TheoryQuantifiers::restart(){ } } -void TheoryQuantifiers::setUserAttribute( std::string& attr, Node n ){ +void TheoryQuantifiers::setUserAttribute( const std::string& attr, Node n ){ QuantifiersAttributes::setUserAttribute( attr, n ); } diff --git a/src/theory/quantifiers/theory_quantifiers.h b/src/theory/quantifiers/theory_quantifiers.h index c3987144c..b4c8966c7 100644 --- a/src/theory/quantifiers/theory_quantifiers.h +++ b/src/theory/quantifiers/theory_quantifiers.h @@ -70,7 +70,7 @@ public: void shutdown() { } std::string identify() const { return std::string("TheoryQuantifiers"); } bool flipDecision(); - void setUserAttribute( std::string& attr, Node n ); + void setUserAttribute( const std::string& attr, Node n ); eq::EqualityEngine* getMasterEqualityEngine() { return d_masterEqualityEngine; } private: void assertUniversal( Node n ); diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 2c178ec2e..4cbcba50e 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -178,23 +178,25 @@ public: Integer prod = d_value * y.d_value; return BitVector(d_size, prod); } - - BitVector unsignedDiv (const BitVector& y) const { + /** + * Total division function that returns 0 when the denominator is 0. + */ + BitVector unsignedDivTotal (const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - // TODO: decide whether we really want these semantics if (y.d_value == 0) { - return BitVector(d_size, Integer(0)); + return BitVector(d_size, 0u); } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); return BitVector(d_size, d_value.floorDivideQuotient(y.d_value)); } - - BitVector unsignedRem(const BitVector& y) const { + /** + * Total division function that returns 0 when the denominator is 0. + */ + BitVector unsignedRemTotal(const BitVector& y) const { CheckArgument(d_size == y.d_size, y); - // TODO: decide whether we really want these semantics if (y.d_value == 0) { - return BitVector(d_size, d_value); + return BitVector(d_size, 0u); } CheckArgument(d_value >= 0, this); CheckArgument(y.d_value > 0, y); diff --git a/test/Makefile.am b/test/Makefile.am index 014aecc43..6cccca05c 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -15,7 +15,7 @@ units systemtests regress regress0 regress1 regress2 regress3: test: check am__tty_colors = \ -red=; grn=; lgn=; blu=; std=; \ +red=; grn=; lgn=; blu=; mag=; std=; \ test "X$(AM_COLOR_TESTS)" != Xno \ && test "X$$TERM" != Xdumb \ && { test "X$(AM_COLOR_TESTS)" = Xalways || test -t 1 2>/dev/null; } \ @@ -24,6 +24,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \ grn='[0;32m'; \ lgn='[1;32m'; \ blu='[1;34m'; \ + mag='[1;35m'; \ std='[m'; \ } @@ -61,14 +62,23 @@ check-recursive: check-pre check-pre: @rm -f $(subdirs_to_check:=/test-suite.log) +if HAVE_CXXTESTGEN +HANDLE_UNIT_TEST_SUMMARY = \ + if test -s "unit/test-suite.log"; then :; else \ + echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \ + fi +else +HANDLE_UNIT_TEST_SUMMARY = \ + echo "$${mag}Unit tests not supported, since CxxTest wasn't found$$std"; \ + rm -f "unit/test-suite.log" +endif + if AUTOMAKE_1_11 # automake 1.11 version check-local: @$(am__tty_colors); \ echo $${blu}=============================== TESTING SUMMARY =============================$$std; \ - if test -s "unit/test-suite.log"; then :; else \ - echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \ - fi; \ + $(HANDLE_UNIT_TEST_SUMMARY); \ if test -s "system/test-suite.log"; then :; else \ echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \ fi; \ @@ -90,9 +100,7 @@ else check-local: @$(am__tty_colors); \ echo $${blu}=============================== TESTING SUMMARY =============================$$std; \ - if test -s "unit/test-suite.log"; then :; else \ - echo "$${red}Unit tests did not run; maybe there were compilation problems ?$$std"; \ - fi; \ + $(HANDLE_UNIT_TEST_SUMMARY); \ if test -s "system/test-suite.log"; then :; else \ echo "$${red}System tests did not run; maybe there were compilation problems ?$$std"; \ fi; \ diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 0f6c11be9..3b30a8d9e 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -142,7 +142,8 @@ BUG_TESTS = \ bug411.smt2 \ bug421.smt2 \ bug421b.smt2 \ - bug425.cvc + bug425.cvc \ + bug480.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bug480.smt2 b/test/regress/regress0/bug480.smt2 new file mode 100644 index 000000000..ba58f354b --- /dev/null +++ b/test/regress/regress0/bug480.smt2 @@ -0,0 +1,11 @@ +; EXPECT: sat +; EXPECT: ((foo true) (bar false) (baz true)) +; EXIT: 10 +(set-logic QF_LIA) +(set-option :produce-assignments true) +(declare-fun x () Int) +(declare-fun y () Int) +(assert (! (or (! (= x (+ y 5)) :named foo) (! (= x (- y 5)) :named bar)) :named baz)) +(assert (and (> x 0) (<= y 5))) +(check-sat) +(get-assignment) diff --git a/test/unit/no_cxxtest b/test/unit/no_cxxtest index cf8b8d729..57e5064d9 100755 --- a/test/unit/no_cxxtest +++ b/test/unit/no_cxxtest @@ -3,10 +3,10 @@ echo echo '***************************************************************************' echo '* *' -echo '* ERROR: CxxTest was not found at configure-time; tests cannot be run. *' +echo '* WARNING: CxxTest not found at configure time; tests cannot be run. *' echo '* *' echo '***************************************************************************' echo -exit 1 - +# skip this test, rather than reporting an error +exit 77 |