From 7b670cdde566e47b1d2f84738d1a0e9b2a401f96 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 25 Feb 2018 12:13:26 +0000 Subject: [PATCH 1/7] fix line number counting in SMT2 tokenizer --- src/solvers/smt2/smt2_tokenizer.cpp | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/solvers/smt2/smt2_tokenizer.cpp b/src/solvers/smt2/smt2_tokenizer.cpp index ec6c3181fc3..d96db803bec 100644 --- a/src/solvers/smt2/smt2_tokenizer.cpp +++ b/src/solvers/smt2/smt2_tokenizer.cpp @@ -219,9 +219,13 @@ smt2_tokenizert::tokent smt2_tokenizert::next_token() case ';': // comment // skip until newline - while(in->get(ch) && ch!='\n') + while(in->get(ch)) { - // ignore + if(ch=='\n') + { + line_no++; + break; + } } break; From 37f69b22f3171ad4c3b8c810695024ca4f50b66b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 7 Mar 2018 10:28:39 +0000 Subject: [PATCH 2/7] added to_mathematical_function_type --- src/util/std_types.h | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/util/std_types.h b/src/util/std_types.h index cc7b4706d41..a13a334b038 100644 --- a/src/util/std_types.h +++ b/src/util/std_types.h @@ -1752,4 +1752,31 @@ class mathematical_function_typet:public typet } }; +/*! \brief Cast a generic typet to a \ref mathematical_function_typet + * + * This is an unchecked conversion. \a type must be known to be \ref + * mathematical_function_typet. + * + * \param type Source type + * \return Object of type \ref mathematical_function_typet + * + * \ingroup gr_std_types +*/ +inline const mathematical_function_typet & + to_mathematical_function_type(const typet &type) +{ + PRECONDITION(type.id()==ID_mathematical_function); + return static_cast(type); +} + +/*! \copydoc to_mathematical_function_type(const typet &) + * \ingroup gr_std_types +*/ +inline mathematical_function_typet & + to_mathematical_function_type(typet &type) +{ + PRECONDITION(type.id()==ID_mathematical_function); + return static_cast(type); +} + #endif // CPROVER_UTIL_STD_TYPES_H From 6dde6b177238546bcafe747657886402277570f8 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 7 Mar 2018 18:50:40 +0000 Subject: [PATCH 3/7] add support for let_exprt --- src/ansi-c/expr2c.cpp | 23 +++++++++++++++++++ src/ansi-c/expr2c_class.h | 1 + src/solvers/Makefile | 1 + src/solvers/flattening/boolbv.cpp | 19 ++++++++++------ src/solvers/flattening/boolbv.h | 1 + src/solvers/flattening/boolbv_let.cpp | 32 +++++++++++++++++++++++++++ src/solvers/flattening/boolbv_map.cpp | 7 ++++++ src/solvers/flattening/boolbv_map.h | 4 ++++ src/solvers/prop/prop_conv.cpp | 21 ++++++++++++++++-- 9 files changed, 100 insertions(+), 9 deletions(-) create mode 100644 src/solvers/flattening/boolbv_let.cpp diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp index 15bb1bd4608..36d5941947d 100644 --- a/src/ansi-c/expr2c.cpp +++ b/src/ansi-c/expr2c.cpp @@ -944,6 +944,26 @@ std::string expr2ct::convert_with( return dest; } +std::string expr2ct::convert_let( + const let_exprt &src, + unsigned precedence) +{ + if(src.operands().size()<3) + return convert_norep(src, precedence); + + unsigned p0; + std::string op0=convert_with_precedence(src.op0(), p0); + + std::string dest="LET "; + dest+=convert(src.symbol()); + dest+='='; + dest+=convert(src.value()); + dest+=" IN "; + dest+=convert(src.where()); + + return dest; +} + std::string expr2ct::convert_update( const exprt &src, unsigned precedence) @@ -3936,6 +3956,9 @@ std::string expr2ct::convert_with_precedence( else if(src.id()==ID_sizeof) return convert_sizeof(src, precedence); + else if(src.id()==ID_let) + return convert_let(to_let_expr(src), precedence=16); + else if(src.id()==ID_type) return convert(src.type()); diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h index 021457331fe..6dafa1cd84c 100644 --- a/src/ansi-c/expr2c_class.h +++ b/src/ansi-c/expr2c_class.h @@ -253,6 +253,7 @@ class expr2ct std::string convert_designated_initializer(const exprt &src, unsigned &precedence); std::string convert_concatenation(const exprt &src, unsigned &precedence); std::string convert_sizeof(const exprt &src, unsigned &precedence); + std::string convert_let(const let_exprt &, unsigned precedence); std::string convert_struct( const exprt &src, diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 8fbdd95aead..9ef3132f1ea 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -125,6 +125,7 @@ SRC = $(BOOLEFORCE_SRC) \ flattening/boolbv_ieee_float_rel.cpp \ flattening/boolbv_if.cpp \ flattening/boolbv_index.cpp \ + flattening/boolbv_let.cpp \ flattening/boolbv_map.cpp \ flattening/boolbv_member.cpp \ flattening/boolbv_mod.cpp \ diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp index d8a475239c6..4c4d5b60bd2 100644 --- a/src/solvers/flattening/boolbv.cpp +++ b/src/solvers/flattening/boolbv.cpp @@ -278,14 +278,10 @@ bvt boolbvt::convert_bitvector(const exprt &expr) else if(expr.id()==ID_array_of) return convert_array_of(to_array_of_expr(expr)); else if(expr.id()==ID_let) - { - // const let_exprt &let_expr=to_let_expr(expr); - throw "let is todo"; - } + return convert_let(to_let_expr(expr)); else if(expr.id()==ID_function_application) - { - return convert_function_application(to_function_application_expr(expr)); - } + return convert_function_application( + to_function_application_expr(expr)); else if(expr.id()==ID_reduction_or || expr.id()==ID_reduction_and || expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand || expr.id()==ID_reduction_xor || expr.id()==ID_reduction_xnor) @@ -463,6 +459,15 @@ literalt boolbvt::convert_rest(const exprt &expr) return convert_quantifier(expr); else if(expr.id()==ID_exists) return convert_quantifier(expr); + else if(expr.id()==ID_let) + { + bvt bv=convert_let(to_let_expr(expr)); + + DATA_INVARIANT(bv.size()==1, + "convert_let must return 1-bit vector for boolean let"); + + return bv[0]; + } else if(expr.id()==ID_index) { bvt bv=convert_index(to_index_expr(expr)); diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h index 585bbdfeca6..08a39d05c80 100644 --- a/src/solvers/flattening/boolbv.h +++ b/src/solvers/flattening/boolbv.h @@ -145,6 +145,7 @@ class boolbvt:public arrayst virtual bvt convert_complex_real(const exprt &expr); virtual bvt convert_complex_imag(const exprt &expr); virtual bvt convert_lambda(const exprt &expr); + virtual bvt convert_let(const let_exprt &); virtual bvt convert_array_of(const array_of_exprt &expr); virtual bvt convert_union(const union_exprt &expr); virtual bvt convert_bv_typecast(const typecast_exprt &expr); diff --git a/src/solvers/flattening/boolbv_let.cpp b/src/solvers/flattening/boolbv_let.cpp new file mode 100644 index 00000000000..d14aa8487c6 --- /dev/null +++ b/src/solvers/flattening/boolbv_let.cpp @@ -0,0 +1,32 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "boolbv.h" + +#include +#include + +bvt boolbvt::convert_let(const let_exprt &expr) +{ + const bvt value_bv=convert_bv(expr.value()); + + // We expect the identifiers of the bound symbols to be unique, + // and thus, these can go straight into the symbol to literal map. + // This property also allows us to cache any subexpressions. + const irep_idt &id=expr.symbol().get_identifier(); + + // the symbol shall be visible during the recursive call + // to convert_bv + map.set_literals(id, expr.symbol().type(), value_bv); + bvt result_bv=convert_bv(expr.where()); + + // now remove, no longer needed + map.erase_literals(id, expr.symbol().type()); + + return result_bv; +} diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp index 7e5c069cd64..f9dc4fa9a16 100644 --- a/src/solvers/flattening/boolbv_map.cpp +++ b/src/solvers/flattening/boolbv_map.cpp @@ -146,3 +146,10 @@ void boolbv_mapt::set_literals( mb.l=literal; } } + +void boolbv_mapt::erase_literals( + const irep_idt &identifier, + const typet &) +{ + mapping.erase(identifier); +} diff --git a/src/solvers/flattening/boolbv_map.h b/src/solvers/flattening/boolbv_map.h index 7059da0ae78..501ef232dd0 100644 --- a/src/solvers/flattening/boolbv_map.h +++ b/src/solvers/flattening/boolbv_map.h @@ -75,6 +75,10 @@ class boolbv_mapt const typet &type, const bvt &literals); + void erase_literals( + const irep_idt &identifier, + const typet &type); + protected: propt ∝ const namespacet &ns; diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp index 04880fa6739..1469b25e040 100644 --- a/src/solvers/prop/prop_conv.cpp +++ b/src/solvers/prop/prop_conv.cpp @@ -327,8 +327,25 @@ literalt prop_conv_solvert::convert_bool(const exprt &expr) } else if(expr.id()==ID_let) { - // const let_exprt &let_expr=to_let_expr(expr); - throw "let is todo"; + const let_exprt &let_expr=to_let_expr(expr); + + // first check whether this is all boolean + if(let_expr.value().type().id()==ID_bool && + let_expr.where().type().id()==ID_bool) + { + literalt value=convert(let_expr.value()); + + // We expect the identifier of the bound symbols to be unique, + // and thus, these can go straight into the symbol map. + // This property also allows us to cache any subexpressions. + const irep_idt &id=let_expr.symbol().get_identifier(); + symbols[id]=value; + literalt result=convert(let_expr.where()); + + // remove again + symbols.erase(id); + return result; + } } return convert_rest(expr); From 5268c44444c1e5842099a7f07faf1c7f4bfcc392 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 25 Feb 2018 12:16:06 +0000 Subject: [PATCH 4/7] a translator from SMT2 into expressions --- src/solvers/smt2/smt2_parser.cpp | 1259 +++++++++++++++++++++++++----- src/solvers/smt2/smt2_parser.h | 88 ++- 2 files changed, 1133 insertions(+), 214 deletions(-) diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index c29d54dda2e..39bb7c0d519 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -8,302 +8,1191 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2_parser.h" -#include -#include +#include -bool smt2_parsert::is_simple_symbol_character(char ch) +void smt2_parsert::command_sequence() { - // any non-empty sequence of letters, digits and the characters - // ~ ! @ $ % ^ & * _ - + = < > . ? / - // that does not start with a digit and is not a reserved word. - - return isalnum(ch) || - ch=='~' || ch=='!' || ch=='@' || ch=='$' || ch=='%' || - ch=='^' || ch=='&' || ch=='*' || ch=='_' || ch=='-' || - ch=='+' || ch=='=' || ch=='<' || ch=='>' || ch=='.' || - ch=='?' || ch=='/'; -} + exit=false; -void smt2_parsert::get_simple_symbol() -{ - // any non-empty sequence of letters, digits and the characters - // ~ ! @ $ % ^ & * _ - + = < > . ? / - // that does not start with a digit and is not a reserved word. + while(next_token()==OPEN) + { + if(next_token()!=SYMBOL) + { + error() << "expected symbol as command" << eom; + return; + } - buffer.clear(); + command(buffer); - char ch; - while(in.get(ch)) - { - if(is_simple_symbol_character(ch)) + if(exit) + return; + + switch(next_token()) { - buffer+=ch; + case END_OF_FILE: + error() << "expected closing parenthesis at end of command," + " but got EOF" << eom; + return; + + case CLOSE: + // what we expect + break; + + default: + error() << "expected end of command" << eom; + return; } - else + } + + if(token!=END_OF_FILE) + { + error() << "unexpected token in command sequence" << eom; + } +} + +void smt2_parsert::ignore_command() +{ + std::size_t parentheses=0; + while(true) + { + switch(peek()) { - in.unget(); // put back + case OPEN: + next_token(); + parentheses++; + break; + + case CLOSE: + if(parentheses==0) + return; // done + + next_token(); + parentheses--; + break; + + case END_OF_FILE: + error() << "unexpected EOF in command" << eom; return; + + default: + next_token(); } } +} +exprt::operandst smt2_parsert::operands() +{ + exprt::operandst result; - // eof -- this is ok here + while(peek()!=CLOSE) + result.push_back(expression()); + + next_token(); // eat the ')' + + return result; } -void smt2_parsert::get_decimal_numeral() +irep_idt smt2_parsert::get_fresh_id(const irep_idt &id) { - // we accept any sequence of digits and dots + if(id_map[id].type.is_nil()) + return id; // id not yet used + + auto &count=renaming_counters[id]; + irep_idt new_id; + do + { + new_id=id2string(id)+'#'+std::to_string(count); + count++; + } + while(id_map.find(new_id)!=id_map.end()); - buffer.clear(); + // record renaming + renaming_map[id]=new_id; + + return new_id; +} - char ch; - while(in.get(ch)) +irep_idt smt2_parsert::rename_id(const irep_idt &id) const +{ + auto it=renaming_map.find(id); + + if(it==renaming_map.end()) + return id; + else + return it->second; +} + +exprt smt2_parsert::let_expression() +{ + if(next_token()!=OPEN) + { + error() << "expected bindings after let" << eom; + return nil_exprt(); + } + + std::vector> bindings; + + while(peek()==OPEN) { - if(isdigit(ch) || ch=='.') + next_token(); + + if(next_token()!=SYMBOL) { - buffer+=ch; + error() << "expected symbol in binding" << eom; + return nil_exprt(); } - else + + irep_idt identifier=buffer; + + // note that the previous bindings are _not_ visible yet + exprt value=expression(); + + if(next_token()!=CLOSE) { - in.unget(); // put back - return; + error() << "expected ')' after value in binding" << eom; + return nil_exprt(); } + + bindings.push_back( + std::pair(identifier, value)); + } + + if(next_token()!=CLOSE) + { + error() << "expected ')' at end of bindings" << eom; + return nil_exprt(); + } + + // save the renaming map + renaming_mapt old_renaming_map=renaming_map; + + // go forwards, add to id_map, renaming if need be + for(auto &b : bindings) + { + // get a fresh id for it + b.first=get_fresh_id(b.first); + auto &entry=id_map[b.first]; + entry.type=b.second.type(); + entry.definition=b.second; } - // eof -- this is ok here + exprt expr=expression(); + + if(next_token()!=CLOSE) + { + error() << "expected ')' after let" << eom; + return nil_exprt(); + } + + exprt result=expr; + + // go backwards, build let_expr + for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++) + { + let_exprt let; + let.symbol()=symbol_exprt(r_it->first, r_it->second.type()); + let.value()=r_it->second; + let.type()=result.type(); + let.where().swap(result); + result=let; + } + + // remove bindings from id_map + for(const auto &b : bindings) + id_map.erase(b.first); + + // restore renamings + renaming_map=old_renaming_map; + + return result; } -void smt2_parsert::get_bin_numeral() +exprt smt2_parsert::quantifier_expression(irep_idt id) { - // we accept any sequence of '0' or '1' + if(next_token()!=OPEN) + { + error() << "expected bindings after " << id << eom; + return nil_exprt(); + } - buffer.clear(); - buffer+='#'; - buffer+='b'; + std::vector bindings; - char ch; - while(in.get(ch)) + while(peek()==OPEN) { - if(ch=='0' || ch=='1') + next_token(); + + if(next_token()!=SYMBOL) { - buffer+=ch; + error() << "expected symbol in binding" << eom; + return nil_exprt(); } - else + + irep_idt identifier=buffer; + + typet type=sort(); + + if(next_token()!=CLOSE) { - in.unget(); // put back - return; + error() << "expected ')' after sort in binding" << eom; + return nil_exprt(); } + + bindings.push_back(symbol_exprt(identifier, type)); } - // eof -- this is ok here + if(next_token()!=CLOSE) + { + error() << "expected ')' at end of bindings" << eom; + return nil_exprt(); + } + + // go forwards, add to id_map + for(const auto &b : bindings) + { + auto &entry=id_map[b.get_identifier()]; + entry.type=b.type(); + entry.definition=nil_exprt(); + } + + exprt expr=expression(); + + if(next_token()!=CLOSE) + { + error() << "expected ')' after " << id << eom; + return nil_exprt(); + } + + exprt result=expr; + + // remove bindings from id_map + for(const auto &b : bindings) + id_map.erase(b.get_identifier()); + + // go backwards, build quantified expression + for(auto r_it=bindings.rbegin(); r_it!=bindings.rend(); r_it++) + { + binary_predicate_exprt quantifier(id); + quantifier.op0()=*r_it; + quantifier.op1().swap(result); + result=quantifier; + } + + return result; } -void smt2_parsert::get_hex_numeral() +exprt smt2_parsert::function_application( + const irep_idt &identifier, + const exprt::operandst &op) { - // we accept any sequence of '0'-'9', 'a'-'f', 'A'-'F' + #if 0 + const auto &f = id_map[identifier]; + + function_application_exprt result; - buffer.clear(); - buffer+='#'; - buffer+='x'; + result.function()=symbol_exprt(identifier, f.type); + result.arguments()=op; - char ch; - while(in.get(ch)) + // check the arguments + if(op.size()!=f.type.variables().size()) { - if(isxdigit(ch)) - { - buffer+=ch; - } - else + error() << "wrong number of arguments for function" << eom; + return nil_exprt(); + } + + for(std::size_t i=0; i(160): // non-breaking space - // skip any whitespace - break; + error() << "expression must have operands with matching types" << eom; + return nil_exprt(); + } + + return binary_exprt(op[0], id, op[1], op[0].type()); + } +} - case ';': // comment - // skip until newline - while(in.get(ch) && ch!='\n') +exprt smt2_parsert::function_application() +{ + switch(next_token()) + { + case SYMBOL: + if(buffer=="_") // indexed identifier + { + // indexed identifier + if(next_token()!=SYMBOL) { - // ignore + error() << "expected symbol after '_'" << eom; + return nil_exprt(); } - break; - case '(': - // produce sub-expression - open_parentheses++; - open_expression(); - break; + if(has_prefix(buffer, "bv")) + { + mp_integer i=string2integer(std::string(buffer, 2, std::string::npos)); + + if(next_token()!=NUMERAL) + { + error() << "expected numeral as bitvector literal width" << eom; + return nil_exprt(); + } + + auto width=std::stoll(buffer); + + if(next_token()!=CLOSE) + { + error() << "expected ')' after bitvector literal" << eom; + return nil_exprt(); + } - case ')': - // done with sub-expression - if(open_parentheses==0) // unexpected ')'. This is an error. + return from_integer(i, unsignedbv_typet(width)); + } + else { - error("unexpected closing parenthesis"); - return; + error() << "unknown indexed identifier " << buffer << eom; + return nil_exprt(); } + } + else + { + // non-indexed symbol; hash it + const irep_idt id=buffer; - open_parentheses--; + if(id==ID_let) + return let_expression(); + else if(id==ID_forall || id==ID_exists) + return quantifier_expression(id); - close_expression(); + auto op=operands(); - if(open_parentheses==0) - return; // done + if(id==ID_and || + id==ID_or || + id==ID_xor) + { + return multi_ary(id, op); + } + else if(id==ID_not) + { + return unary(id, op); + } + else if(id==ID_equal || + id==ID_le || + id==ID_ge || + id==ID_lt || + id==ID_gt) + { + return binary_predicate(id, op); + } + else if(id=="bvule") + { + return binary_predicate(ID_le, op); + } + else if(id=="bvsle") + { + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return binary_predicate(ID_le, op); + } + else if(id=="bvuge") + { + return binary_predicate(ID_ge, op); + } + else if(id=="bvsge") + { + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return binary_predicate(ID_ge, op); + } + else if(id=="bvult") + { + return binary_predicate(ID_lt, op); + } + else if(id=="bvslt") + { + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return binary_predicate(ID_lt, op); + } + else if(id=="bvugt") + { + return binary_predicate(ID_gt, op); + } + else if(id=="bvsgt") + { + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return binary_predicate(ID_gt, op); + } + else if(id=="bvashr") + { + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return cast_bv_to_unsigned(binary(ID_ashr, op)); + } + else if(id=="bvlshr" || id=="bvshr") + { + return binary(ID_lshr, op); + } + else if(id=="bvlshr" || id=="bvashl" || id=="bvshl") + { + return binary(ID_shl, op); + } + else if(id=="bvand") + { + return multi_ary(ID_bitand, op); + } + else if(id=="bvnand") + { + return multi_ary(ID_bitnand, op); + } + else if(id=="bvor") + { + return multi_ary(ID_bitor, op); + } + else if(id=="bvnor") + { + return multi_ary(ID_bitnor, op); + } + else if(id=="bvxor") + { + return multi_ary(ID_bitxor, op); + } + else if(id=="bvxnor") + { + return multi_ary(ID_bitxnor, op); + } + else if(id=="bvnot") + { + return unary(ID_bitnot, op); + } + else if(id=="bvneg") + { + return unary(ID_unary_minus, op); + } + else if(id=="bvadd") + { + return multi_ary(ID_plus, op); + } + else if(id==ID_plus) + { + return multi_ary(id, op); + } + else if(id=="bvsub" || id=="-") + { + return binary(ID_minus, op); + } + else if(id=="bvmul" || id=="*") + { + return binary(ID_mult, op); + } + else if(id=="bvsdiv") + { + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return cast_bv_to_unsigned(binary(ID_div, op)); + } + else if(id=="bvudiv") + { + return binary(ID_div, op); + } + else if(id=="/" || id=="div") + { + return binary(ID_div, op); + } + else if(id=="bvsrem") + { + // 2's complement signed remainder (sign follows dividend) + // This matches our ID_mod, and what C does since C99. + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return cast_bv_to_unsigned(binary(ID_mod, op)); + } + else if(id=="bvsmod") + { + // 2's complement signed remainder (sign follows divisor) + // We don't have that. + op[0]=cast_bv_to_signed(op[0]); + op[1]=cast_bv_to_signed(op[1]); + return cast_bv_to_unsigned(binary(ID_mod, op)); + } + else if(id=="bvurem" || id=="%") + { + return binary(ID_mod, op); + } + else if(id=="concat") + { + if(op.size()!=2) + { + error() << "concat takes two operands " << op.size() << eom; + return nil_exprt(); + } - break; + auto width0=to_unsignedbv_type(op[0].type()).get_width(); + auto width1=to_unsignedbv_type(op[1].type()).get_width(); - case '|': // quoted symbol - get_quoted_symbol(); - symbol(); - if(open_parentheses==0) - return; // done - break; + unsignedbv_typet t(width0+width1); - case '"': // string literal - get_string_literal(); - string_literal(); - if(open_parentheses==0) - return; // done - break; + return binary_exprt(op[0], ID_concatenation, op[1], t); + } + else if(id=="distinct") + { + // pair-wise different constraint, multi-ary + return multi_ary("distinct", op); + } + else if(id=="ite") + { + if(op.size()!=3) + { + error() << "ite takes three operands" << eom; + return nil_exprt(); + } - case ':': // keyword - get_simple_symbol(); - keyword(); - if(open_parentheses==0) - return; // done - break; + if(op[0].type().id()!=ID_bool) + { + error() << "ite takes a boolean as first operand" << eom; + return nil_exprt(); + } - case '#': - if(in.get(ch)) + if(op[1].type()!=op[2].type()) + { + error() << "ite needs matching types" << eom; + return nil_exprt(); + } + + return if_exprt(op[0], op[1], op[2]); + } + else if(id=="=>" || id=="implies") + { + return binary(ID_implies, op); + } + else { - if(ch=='b') + // rummage through id_map + const irep_idt final_id=rename_id(id); + auto id_it=id_map.find(final_id); + if(id_it!=id_map.end()) { - get_bin_numeral(); - numeral(); + if(id_it->second.type.id()==ID_mathematical_function) + { + function_application_exprt app; + app.function()=symbol_exprt(final_id, id_it->second.type); + app.arguments()=op; + app.type()=to_mathematical_function_type( + id_it->second.type).codomain(); + return app; + } + else + return symbol_exprt(final_id, id_it->second.type); + } + + error() << "2 unknown symbol " << id << eom; + return nil_exprt(); + } + } + break; + + case OPEN: // likely indexed identifier + if(peek()==SYMBOL) + { + next_token(); // eat symbol + if(buffer=="_") + { + // indexed identifier + if(next_token()!=SYMBOL) + { + error() << "expected symbol after '_'" << eom; + return nil_exprt(); + } + + irep_idt id=buffer; // hash it + + if(id=="extract") + { + if(next_token()!=NUMERAL) + { + error() << "expected numeral after extract" << eom; + return nil_exprt(); + } + + auto upper=std::stoll(buffer); + + if(next_token()!=NUMERAL) + { + error() << "expected two numerals after extract" << eom; + return nil_exprt(); + } + + auto lower=std::stoll(buffer); + + if(next_token()!=CLOSE) + { + error() << "expected ')' after extract" << eom; + return nil_exprt(); + } + + auto op=operands(); + + if(op.size()!=1) + { + error() << "extract takes one operand" << eom; + return nil_exprt(); + } + + auto upper_e=from_integer(upper, integer_typet()); + auto lower_e=from_integer(lower, integer_typet()); + + if(uppersecond.type); + + error() << "1 unknown symbol " << identifier << eom; + return nil_exprt(); } - break; + } + + case NUMERAL: + if(buffer.size()>=2 && buffer[0]=='#' && buffer[1]=='x') + { + mp_integer value= + string2integer(std::string(buffer, 2, std::string::npos), 16); + const std::size_t width = 4*(buffer.size() - 2); + CHECK_RETURN(width!=0 && width%4==0); + unsignedbv_typet type(width); + return from_integer(value, type); + } + else if(buffer.size()>=2 && buffer[0]=='#' && buffer[1]=='b') + { + mp_integer value= + string2integer(std::string(buffer, 2, std::string::npos), 2); + const std::size_t width = buffer.size() - 2; + CHECK_RETURN(width!=0); + unsignedbv_typet type(width); + return from_integer(value, type); + } + else + { + return constant_exprt(buffer, integer_typet()); + } + + case OPEN: // function application + return function_application(); + + case END_OF_FILE: + error() << "EOF in an expression" << eom; + return nil_exprt(); + + default: + error() << "unexpected token in an expression" << eom; + return nil_exprt(); + } +} - default: // likely a simple symbol or a numeral - if(isdigit(ch)) +typet smt2_parsert::sort() +{ + switch(next_token()) + { + case SYMBOL: + if(buffer=="Bool") + return bool_typet(); + else if(buffer=="Int") + return integer_typet(); + else if(buffer=="Real") + return real_typet(); + else + { + error() << "unexpected sort: `" << buffer << '\'' << eom; + return nil_typet(); + } + + case OPEN: + if(next_token()!=SYMBOL) + { + error() << "expected symbol after '(' in a sort " << eom; + return nil_typet(); + } + + if(buffer=="_") + { + // indexed identifier + if(next_token()!=SYMBOL) { - in.unget(); - get_decimal_numeral(); - numeral(); - if(open_parentheses==0) - return; // done + error() << "expected symbol after '_' in a sort" << eom; + return nil_typet(); } - else if(is_simple_symbol_character(ch)) + + if(buffer=="BitVec") { - in.unget(); - get_simple_symbol(); - symbol(); - if(open_parentheses==0) - return; // done + if(next_token()!=NUMERAL) + { + error() << "expected numeral as bit-width" << eom; + return nil_typet(); + } + + auto width=std::stoll(buffer); + + // eat the ')' + if(next_token()!=CLOSE) + { + error() << "expected ')' at end of sort" << eom; + return nil_typet(); + } + + return unsignedbv_typet(width); } else { - // illegal character, error - error("unexpected character"); - return; + error() << "unexpected sort: `" << buffer << '\'' << eom; + return nil_typet(); } } + else + { + error() << "unexpected sort: `" << buffer << '\'' << eom; + return nil_typet(); + } + + default: + error() << "unexpected token in a sort " << buffer << eom; + return nil_typet(); } +} - if(open_parentheses==0) +typet smt2_parsert::function_signature_definition() +{ + if(next_token()!=OPEN) { - // Hmpf, eof before we got anything. Blank file! + error() << "expected '(' at beginning of signature" << eom; + return nil_typet(); } - else + + if(peek()==CLOSE) + { + next_token(); // eat the ')' + return sort(); + } + + mathematical_function_typet result; + + while(peek()!=CLOSE) + { + if(next_token()!=OPEN) + { + error() << "expected '(' at beginning of parameter" << eom; + return result; + } + + if(next_token()!=SYMBOL) + { + error() << "expected symbol in parameter" << eom; + return result; + } + + auto &var=result.add_variable(); + std::string id=buffer; + var.set_identifier(id); + var.type()=sort(); + + auto &entry=id_map[id]; + entry.type=var.type(); + entry.definition=nil_exprt(); + + if(next_token()!=CLOSE) + { + error() << "expected ')' at end of parameter" << eom; + return result; + } + } + + next_token(); // eat the ')' + + result.codomain()=sort(); + + return result; +} + +typet smt2_parsert::function_signature_declaration() +{ + if(next_token()!=OPEN) + { + error() << "expected '(' at beginning of signature" << eom; + return nil_typet(); + } + + if(peek()==CLOSE) + { + next_token(); // eat the ')' + return sort(); + } + + mathematical_function_typet result; + + while(peek()!=CLOSE) + { + if(next_token()!=OPEN) + { + error() << "expected '(' at beginning of parameter" << eom; + return result; + } + + if(next_token()!=SYMBOL) + { + error() << "expected symbol in parameter" << eom; + return result; + } + + auto &var=result.add_variable(); + var.type()=sort(); + + if(next_token()!=CLOSE) + { + error() << "expected ')' at end of parameter" << eom; + return result; + } + } + + next_token(); // eat the ')' + + result.codomain()=sort(); + + return result; +} + +void smt2_parsert::command(const std::string &c) +{ + if(c=="declare-const") + { + if(next_token()!=SYMBOL) + { + error() << "expected a symbol after declare-const" << eom; + ignore_command(); + return; + } + + irep_idt id=buffer; + + if(id_map.find(id)!=id_map.end()) + { + error() << "identifier `" << id << "' defined twice" << eom; + ignore_command(); + return; + } + + auto &entry=id_map[id]; + entry.type=sort(); + entry.definition=nil_exprt(); + } + else if(c=="declare-fun") { - // Eof before end of expression. Error! - error("EOF before end of expression"); + if(next_token()!=SYMBOL) + { + error() << "expected a symbol after declare-fun" << eom; + ignore_command(); + return; + } + + irep_idt id=buffer; + + if(id_map.find(id)!=id_map.end()) + { + error() << "identifier `" << id << "' defined twice" << eom; + ignore_command(); + return; + } + + auto &entry=id_map[id]; + entry.type=function_signature_declaration(); + entry.definition=nil_exprt(); } + else if(c=="define-fun") + { + if(next_token()!=SYMBOL) + { + error() << "expected a symbol after define-fun" << eom; + ignore_command(); + return; + } + + const irep_idt id=buffer; + + if(id_map.find(id)!=id_map.end()) + { + error() << "identifier `" << id << "' defined twice" << eom; + ignore_command(); + return; + } + + // create the entry + id_map[id]; + + auto signature=function_signature_definition(); + exprt body=expression(); + + // set up the entry + auto &entry=id_map[id]; + entry.type=signature; + entry.definition=body; + } + else if(c=="exit") + { + exit=true; + } + else + ignore_command(); } diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 46633eaa174..143ecc61583 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -6,46 +6,76 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ - #ifndef CPROVER_SOLVERS_SMT2_SMT2_PARSER_H #define CPROVER_SOLVERS_SMT2_SMT2_PARSER_H -#include -#include +#include + +#include -class smt2_parsert +#include "smt2_tokenizer.h" + +class smt2_parsert:public smt2_tokenizert { public: - explicit smt2_parsert(std::istream &_in):in(_in) + explicit smt2_parsert(std::istream &_in): + smt2_tokenizert(_in), + exit(false) { } - void operator()(); + bool parse() override + { + command_sequence(); + return !ok; + } + + struct idt + { + idt():type(nil_typet()) + { + } + + typet type; + exprt definition; + }; + + using id_mapt=std::map; + id_mapt id_map; protected: - std::istream ∈ - std::string buffer; - - // string literal, numeral, simple symbol, quoted symbol - // and keyword are in 'buffer' - virtual void string_literal() = 0; - virtual void numeral() = 0; - virtual void symbol() = 0; - virtual void keyword() = 0; - virtual void open_expression() = 0; // '(' - virtual void close_expression() = 0; // ')' - - // parse errors - virtual void error(const std::string &) = 0; - -private: - void get_decimal_numeral(); - void get_hex_numeral(); - void get_bin_numeral(); - void get_simple_symbol(); - void get_quoted_symbol(); - void get_string_literal(); - bool is_simple_symbol_character(char ch); + bool exit; + void command_sequence(); + + virtual void command(const std::string &); + + // for let/quantifier bindings, function parameters + using renaming_mapt=std::map; + renaming_mapt renaming_map; + using renaming_counterst=std::map; + renaming_counterst renaming_counters; + irep_idt get_fresh_id(const irep_idt &); + irep_idt rename_id(const irep_idt &) const; + + void ignore_command(); + exprt expression(); + exprt function_application(); + typet sort(); + exprt::operandst operands(); + typet function_signature_declaration(); + typet function_signature_definition(); + exprt multi_ary(irep_idt, exprt::operandst &); + exprt binary_predicate(irep_idt, exprt::operandst &); + exprt binary(irep_idt, exprt::operandst &); + exprt unary(irep_idt, exprt::operandst &); + + exprt let_expression(); + exprt quantifier_expression(irep_idt); + exprt function_application( + const irep_idt &identifier, + const exprt::operandst &op); + exprt cast_bv_to_signed(const exprt &); + exprt cast_bv_to_unsigned(const exprt &); }; #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H From a75ee3f6f37ce23fbfbc23b6b2f4fb9fd77250d9 Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Fri, 16 Mar 2018 09:52:11 +0000 Subject: [PATCH 5/7] Add missing langapi dependency to util This dependency was introduced by moving language.h to langapi. The dependency will be removed by the work in 1869 / 1935. --- src/util/CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 19e7810aba2..055eabc7891 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(util ${sources}) generic_includes(util) -target_link_libraries(util big-int) +target_link_libraries(util big-int langapi) From 246472fb45b55cc34cbbae56eab340eb0487527b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Sun, 25 Feb 2018 12:48:03 +0000 Subject: [PATCH 6/7] an SMT2 solver using boolbv and satcheckt --- .gitignore | 2 + src/solvers/CMakeLists.txt | 9 +- src/solvers/Makefile | 16 +- src/solvers/smt2/smt2_solver.cpp | 266 +++++++++++++++++++++++++++++++ 4 files changed, 287 insertions(+), 6 deletions(-) create mode 100644 src/solvers/smt2/smt2_solver.cpp diff --git a/.gitignore b/.gitignore index 9693fb2faef..4636f5a8380 100644 --- a/.gitignore +++ b/.gitignore @@ -104,6 +104,8 @@ src/goto-instrument/goto-instrument.exe src/jbmc/jbmc src/musketeer/musketeer src/musketeer/musketeer.exe +src/solvers/smt2/smt2_solver +src/solvers/smt2/smt2_solver.exe src/symex/symex src/symex/symex.exe src/goto-diff/goto-diff diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index 6fd78fba152..5acd6652114 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -1,3 +1,6 @@ +set(CMAKE_CXX_STANDARD 11) +set(CMAKE_CXX_STANDARD_REQUIRED true) + # We may use one of several different solver libraries. # The following files wrap the chosen solver library. # We remove them all from the solver-library sources list, and then add the @@ -104,6 +107,10 @@ elseif("${sat_impl}" STREQUAL "glucose") target_link_libraries(solvers glucose-condensed) endif() -target_link_libraries(solvers java_bytecode util) +target_link_libraries(solvers util) + +# Executable +add_executable(smt2_solver smt2/smt2_solver.cpp) +target_link_libraries(smt2_solver solvers) generic_includes(solvers) diff --git a/src/solvers/Makefile b/src/solvers/Makefile index 9ef3132f1ea..293d0419361 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -216,9 +216,9 @@ INCLUDES += -I .. \ $(SMVSAT_INCLUDE) $(SQUOLEM2_INC) $(CUDD_INCLUDE) $(GLUCOSE_INCLUDE) \ $(PRECOSAT_INCLUDE) $(PICOSAT_INCLUDE) $(LINGELING_INCLUDE) -CLEANFILES = solvers$(LIBEXT) +CLEANFILES = solvers$(LIBEXT) smt2_solver$(EXEEXT) -all: solvers$(LIBEXT) +all: solvers$(LIBEXT) smt2_solver$(EXEEXT) ifneq ($(SQUOLEM2),) CP_CXXFLAGS += -DHAVE_QBF_CORE @@ -232,9 +232,15 @@ endif -include $(SRC:.cpp=.d) -############################################################################### - -solvers$(LIBEXT): $(OBJ) $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \ +SOLVER_LIB = $(CHAFF_LIB) $(BOOLEFORCE_LIB) $(MINISAT_LIB) \ $(MINISAT2_LIB) $(SMVSAT_LIB) $(SQUOLEM2_LIB) $(CUDD_LIB) \ $(PRECOSAT_LIB) $(PICOSAT_LIB) $(LINGELING_LIB) $(GLUCOSE_LIB) + +############################################################################### + +solvers$(LIBEXT): $(OBJ) $(SOLVER_LIB) $(LINKLIB) $(LIBSOLVER) + +smt2_solver$(EXEEXT): $(OBJ) smt2/smt2_solver$(OBJEXT) \ + ../util/util$(LIBEXT) ../langapi/langapi$(LIBEXT) ../big-int/big-int$(LIBEXT) $(SOLVER_LIB) + $(LINKBIN) $(LIBSOLVER) diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp new file mode 100644 index 00000000000..9c1a6c00602 --- /dev/null +++ b/src/solvers/smt2/smt2_solver.cpp @@ -0,0 +1,266 @@ +/*******************************************************************\ + +Module: SMT2 Solver that uses boolbv and the default SAT solver + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include +#include + +#include "smt2_parser.h" + +#include +#include +#include +#include +#include + +#include +#include + +class smt2_solvert:public smt2_parsert +{ +public: + smt2_solvert( + std::istream &_in, + decision_proceduret &_solver): + smt2_parsert(_in), + solver(_solver) + { + } + +protected: + decision_proceduret &solver; + + void command(const std::string &) override; + void define_constants(const exprt &); + void expand_function_applications(exprt &); + + std::set constants_done; +}; + +void smt2_solvert::define_constants(const exprt &expr) +{ + for(const auto &op : expr.operands()) + define_constants(op); + + if(expr.id()==ID_symbol) + { + irep_idt identifier=to_symbol_expr(expr).get_identifier(); + + // already done? + if(constants_done.find(identifier)!=constants_done.end()) + return; + + constants_done.insert(identifier); + + auto f_it=id_map.find(identifier); + + if(f_it!=id_map.end()) + { + const auto &f=f_it->second; + + if(f.type.id()!=ID_mathematical_function && + f.definition.is_not_nil()) + { + exprt def=f.definition; + expand_function_applications(def); + define_constants(def); // recursive! + solver.set_to_true(equal_exprt(expr, def)); + } + } + } +} + +void smt2_solvert::expand_function_applications(exprt &expr) +{ + for(exprt &op : expr.operands()) + expand_function_applications(op); + + if(expr.id()==ID_function_application) + { + auto &app=to_function_application_expr(expr); + + // look it up + irep_idt identifier=app.function().get_identifier(); + auto f_it=id_map.find(identifier); + + if(f_it!=id_map.end()) + { + const auto &f=f_it->second; + + DATA_INVARIANT(f.type.id()==ID_mathematical_function, + "type of function symbol must be mathematical_function_type"); + + const auto f_type= + to_mathematical_function_type(f.type); + + DATA_INVARIANT(f_type.domain().size()== + app.arguments().size(), + "number of function parameters"); + + replace_symbolt replace_symbol; + + std::map parameter_map; + for(std::size_t i=0; i Date: Tue, 6 Mar 2018 17:55:34 +0000 Subject: [PATCH 7/7] tests for smt2_solver --- regression/Makefile | 1 + regression/smt2_solver/Makefile | 18 ++++++ .../smt2_solver/basic-bv1/basic-bv1.smt2 | 64 +++++++++++++++++++ regression/smt2_solver/basic-bv1/test.desc | 7 ++ .../let-with-bv1/let-with-bv1.smt2 | 32 ++++++++++ regression/smt2_solver/let-with-bv1/test.desc | 7 ++ regression/smt2_solver/let1/let1.smt2 | 30 +++++++++ regression/smt2_solver/let1/test.desc | 7 ++ 8 files changed, 166 insertions(+) create mode 100644 regression/smt2_solver/Makefile create mode 100644 regression/smt2_solver/basic-bv1/basic-bv1.smt2 create mode 100644 regression/smt2_solver/basic-bv1/test.desc create mode 100644 regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 create mode 100644 regression/smt2_solver/let-with-bv1/test.desc create mode 100644 regression/smt2_solver/let1/let1.smt2 create mode 100644 regression/smt2_solver/let1/test.desc diff --git a/regression/Makefile b/regression/Makefile index c5f7c41764f..eefb1f9e047 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -11,6 +11,7 @@ DIRS = cbmc \ strings-smoke-tests \ cbmc-cover \ goto-instrument-typedef \ + smt2_solver \ strings \ invariants \ goto-diff \ diff --git a/regression/smt2_solver/Makefile b/regression/smt2_solver/Makefile new file mode 100644 index 00000000000..3be14ea765c --- /dev/null +++ b/regression/smt2_solver/Makefile @@ -0,0 +1,18 @@ +default: tests.log + +test: + @../test.pl -p -c ../../../src/solvers/smt2_solver + +tests.log: ../test.pl + @../test.pl -p -c ../../../src/solvers/smt2_solver + +show: + @for dir in *; do \ + if [ -d "$$dir" ]; then \ + vim -o "$$dir/*.c" "$$dir/*.out"; \ + fi; \ + done; + +clean: + find -name '*.out' -execdir $(RM) '{}' \; + $(RM) tests.log diff --git a/regression/smt2_solver/basic-bv1/basic-bv1.smt2 b/regression/smt2_solver/basic-bv1/basic-bv1.smt2 new file mode 100644 index 00000000000..13c3a739dcb --- /dev/null +++ b/regression/smt2_solver/basic-bv1/basic-bv1.smt2 @@ -0,0 +1,64 @@ +(set-logic QF_BV) + +; From https://rise4fun.com/z3/tutorialcontent/guide + +; Basic Bitvector Arithmetic +(define-fun b01 () Bool (= (bvadd #x07 #x03) #x0a)) ; addition +(define-fun b02 () Bool (= (bvsub #x07 #x03) #x04)) ; subtraction +(define-fun b03 () Bool (= (bvneg #x07) #xf9)) ; unary minus +(define-fun b04 () Bool (= (bvmul #x07 #x03) #x15)) ; multiplication +(define-fun b05 () Bool (= (bvurem #x07 #x03) #x01)) ; unsigned remainder +(define-fun b06 () Bool (= (bvsrem #x07 #x03) #x01)) ; signed remainder +(define-fun b07 () Bool (= (bvsmod #x07 #x03) #x01)) ; signed modulo +(define-fun b08 () Bool (= (bvshl #x07 #x03) #x38)) ; shift left +(define-fun b09 () Bool (= (bvlshr #xf0 #x03) #x1e)) ; unsigned (logical) shift right +(define-fun b10 () Bool (= (bvashr #xf0 #x03) #xfe)) ; signed (arithmetical) shift right#x0a + +; Bitwise Operations + +(define-fun w1 () Bool (= (bvor #x6 #x3) #x7)) ; bitwise or +(define-fun w2 () Bool (= (bvand #x6 #x3) #x2)) ; bitwise and +(define-fun w3 () Bool (= (bvnot #x6) #x9)) ; bitwise not +(define-fun w4 () Bool (= (bvnand #x6 #x3) #xd)) ; bitwise nand +(define-fun w5 () Bool (= (bvnor #x6 #x3) #x8)) ; bitwise nor +(define-fun w6 () Bool (= (bvxnor #x6 #x3) #xa)) ; bitwise xnor + +; We can prove a bitwise version of deMorgan's law + +(declare-const x (_ BitVec 64)) +(declare-const y (_ BitVec 64)) +(define-fun d01 () Bool (= (bvand (bvnot x) (bvnot y)) (bvnot (bvor x y)))) + +; There is a fast way to check that fixed size numbers are powers of two + +(define-fun is-power-of-two ((x (_ BitVec 4))) Bool + (= #x0 (bvand x (bvsub x #x1)))) +(declare-const a (_ BitVec 4)) +(define-fun power-test () Bool + (= (is-power-of-two a) + (or (= a #x0) + (= a #x1) + (= a #x2) + (= a #x4) + (= a #x8)))) + +; Predicates over Bitvectors + +(define-fun p1 () Bool (= (bvule #x0a #xf0) true)) ; unsigned less or equal +(define-fun p2 () Bool (= (bvult #x0a #xf0) true)) ; unsigned less than +(define-fun p3 () Bool (= (bvuge #x0a #xf0) false)) ; unsigned greater or equal +(define-fun p4 () Bool (= (bvugt #x0a #xf0) false)) ; unsigned greater than +(define-fun p5 () Bool (= (bvsle #x0a #xf0) false)) ; signed less or equal +(define-fun p6 () Bool (= (bvslt #x0a #xf0) false)) ; signed less than +(define-fun p7 () Bool (= (bvsge #x0a #xf0) true)) ; signed greater or equal +(define-fun p8 () Bool (= (bvsgt #x0a #xf0) true)) ; signed greater than + +; all must be true + +(assert (not (and + b01 b02 b03 b04 b05 b06 b07 b08 b09 b10 + d01 + power-test + p1 p2 p3 p4 p5 p6 p7 p8))) + +(check-sat) diff --git a/regression/smt2_solver/basic-bv1/test.desc b/regression/smt2_solver/basic-bv1/test.desc new file mode 100644 index 00000000000..aee65a85d4c --- /dev/null +++ b/regression/smt2_solver/basic-bv1/test.desc @@ -0,0 +1,7 @@ +CORE +basic-bv1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 b/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 new file mode 100644 index 00000000000..baea8cee9ae --- /dev/null +++ b/regression/smt2_solver/let-with-bv1/let-with-bv1.smt2 @@ -0,0 +1,32 @@ +(set-logic QF_BV) + +; try 'let' on bitvectors + +(define-fun x () (_ BitVec 4) #x0) + +; very simple +(define-fun let0 () Bool (= (let ((x #x0)) #x1) #x1)) + +; let hides the function 'x' +(define-fun let1 () Bool (= (let ((x #x1)) x) #x1)) + +; the binding isn't visible immediately +(define-fun let2 () Bool (= (let ((x x)) x) #x0)) + +; parallel let +(define-fun let3 () Bool (= (let ((x #x1) (y x)) y) #x0)) + +; limited scope +(define-fun let4 () Bool (and (= (let ((x #x1)) x) #x1) (= x #x0))) + +; all must be true + +(assert (not (and + let0 + let1 + let2 + let3 + let4 + ))) + +(check-sat) diff --git a/regression/smt2_solver/let-with-bv1/test.desc b/regression/smt2_solver/let-with-bv1/test.desc new file mode 100644 index 00000000000..6fc75569439 --- /dev/null +++ b/regression/smt2_solver/let-with-bv1/test.desc @@ -0,0 +1,7 @@ +CORE +let-with-bv1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +-- diff --git a/regression/smt2_solver/let1/let1.smt2 b/regression/smt2_solver/let1/let1.smt2 new file mode 100644 index 00000000000..543c993b2c3 --- /dev/null +++ b/regression/smt2_solver/let1/let1.smt2 @@ -0,0 +1,30 @@ +(set-logic QF_BV) + +(define-fun x () Bool false) + +; very simple +(define-fun let0 () Bool (let ((x false)) true)) + +; let hides the function 'x' +(define-fun let1 () Bool (let ((x true)) x)) + +; the binding isn't visible immediately +(define-fun let2 () Bool (not (let ((x x)) x))) + +; parallel let +(define-fun let3 () Bool (let ((x true) (y x)) (not y))) + +; limited scope +(define-fun let4 () Bool (and (let ((x true)) x) (not x))) + +; all must be true + +(assert (not (and + let0 + let1 + let2 + let3 + let4 + ))) + +(check-sat) diff --git a/regression/smt2_solver/let1/test.desc b/regression/smt2_solver/let1/test.desc new file mode 100644 index 00000000000..834542aa891 --- /dev/null +++ b/regression/smt2_solver/let1/test.desc @@ -0,0 +1,7 @@ +CORE +let1.smt2 + +^EXIT=0$ +^SIGNAL=0$ +^unsat$ +--