diff --git a/scripts/delete_failing_smt2_solver_tests b/scripts/delete_failing_smt2_solver_tests index 2fe8127538c..ea65366e44b 100755 --- a/scripts/delete_failing_smt2_solver_tests +++ b/scripts/delete_failing_smt2_solver_tests @@ -39,7 +39,6 @@ rm Float4/test.desc rm Float5/test.desc rm Float6/test.desc rm Float8/test.desc -rm Free2/test.desc rm Function1/test.desc rm Initialization6/test.desc rm Linking4/test.desc @@ -51,14 +50,12 @@ rm Malloc19/test.desc rm Malloc21/test.desc rm Malloc23/test.desc rm Malloc24/test.desc -rm Memory_leak1/test.desc rm Memory_leak2/test.desc rm Multi_Dimensional_Array1/test.desc rm Multi_Dimensional_Array2/test.desc rm Multi_Dimensional_Array3/test.desc rm Multi_Dimensional_Array4/test.desc rm Multi_Dimensional_Array6/test.desc -rm Multiple_Properties1/test.desc rm Overflow_Leftshift1/test.desc rm Overflow_Multiplication1/test.desc rm Overflow_Subtraction1/test.desc @@ -92,14 +89,12 @@ rm Quantifiers-not-exists/test.desc rm Quantifiers-two-dimension-array/test.desc rm Quantifiers-type/test.desc rm Quantifiers1/test.desc -rm Recursion5/test.desc rm String2/test.desc rm Struct_Bytewise1/test.desc rm Struct_Bytewise2/test.desc rm Struct_Initialization2/test.desc rm Struct_Padding1/test.desc rm Typecast1/test.desc -rm Undefined_Shift1/test.desc rm Union_Initialization1/test.desc rm Unwinding_Locality1/test.desc rm address_space_size_limit1/test.desc @@ -117,7 +112,6 @@ rm byte_update6/test.desc rm byte_update7/test.desc rm byte_update8/test.desc rm byte_update9/test.desc -rm compact-trace/test.desc rm dynamic_size1/stack_object.desc rm equality_through_array1/test.desc rm equality_through_array2/test.desc @@ -134,19 +128,14 @@ rm equality_through_struct_containing_arrays2/test.desc rm equality_through_union1/test.desc rm equality_through_union2/test.desc rm equality_through_union3/test.desc -rm full_slice1/test.desc -rm full_slice2/test.desc rm gcc_bswap1/test.desc rm gcc_c99-bool-1/test.desc rm gcc_statement_expression4/test.desc -rm gcc_switch_case_range1/test.desc -rm gcc_switch_case_range2/test.desc rm gcc_vector1/test.desc rm gcc_vector2/test.desc rm graphml_witness1/test.desc rm havoc_object1/test.desc rm hex_trace/test.desc -rm if2/test.desc rm integer-assignments1/test.desc rm little-endian-array1/test.desc rm memory_allocation1/test.desc diff --git a/src/solvers/Makefile b/src/solvers/Makefile index b5cc4118de9..743613373ea 100644 --- a/src/solvers/Makefile +++ b/src/solvers/Makefile @@ -185,6 +185,7 @@ SRC = $(BOOLEFORCE_SRC) \ sat/resolution_proof.cpp \ smt2/smt2_conv.cpp \ smt2/smt2_dec.cpp \ + smt2/smt2_format.cpp \ smt2/smt2_parser.cpp \ smt2/smt2_tokenizer.cpp \ smt2/smt2irep.cpp \ diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp new file mode 100644 index 00000000000..9f943574593 --- /dev/null +++ b/src/solvers/smt2/smt2_format.cpp @@ -0,0 +1,71 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#include "smt2_format.h" + +#include +#include +#include + +std::ostream &smt2_format_rec(std::ostream &out, const typet &type) +{ + if(type.id() == ID_unsignedbv) + out << "(_ BitVec " << to_unsignedbv_type(type).get_width() << ')'; + else if(type.id() == ID_bool) + out << "Bool"; + else if(type.id() == ID_integer) + out << "Int"; + else if(type.id() == ID_real) + out << "Real"; + else + out << "? " << type.id(); + + return out; +} + +std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr) +{ + if(expr.id() == ID_constant) + { + const auto &value = to_constant_expr(expr).get_value(); + + const typet &expr_type = expr.type(); + + if(expr_type.id() == ID_unsignedbv) + { + const std::size_t width = to_unsignedbv_type(expr_type).get_width(); + + const auto value = numeric_cast_v(expr); + + out << "(_ bv" << value << " " << width << ")"; + } + else if(expr_type.id() == ID_bool) + { + if(expr.is_true()) + out << "true"; + else if(expr.is_false()) + out << "false"; + else + DATA_INVARIANT(false, "unknown Boolean constant"); + } + else if(expr_type.id() == ID_integer) + { + out << value; + } + else + DATA_INVARIANT(false, "unhandled constant: " + expr_type.id_string()); + } + else if(expr.id() == ID_symbol) + { + out << to_symbol_expr(expr).get_identifier(); + } + else + out << "? " << expr.id(); + + return out; +} diff --git a/src/solvers/smt2/smt2_format.h b/src/solvers/smt2/smt2_format.h new file mode 100644 index 00000000000..d2eaa2412cf --- /dev/null +++ b/src/solvers/smt2/smt2_format.h @@ -0,0 +1,40 @@ +/*******************************************************************\ + +Module: + +Author: Daniel Kroening, kroening@kroening.com + +\*******************************************************************/ + +#ifndef CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H +#define CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H + +#include + +template +struct smt2_format_containert +{ + explicit smt2_format_containert(const T &_o) : o(_o) + { + } + + const T &o; +}; + +template +static inline smt2_format_containert smt2_format(const T &_o) +{ + return smt2_format_containert(_o); +} + +template +static inline std::ostream & +operator<<(std::ostream &out, const smt2_format_containert &c) +{ + return smt2_format_rec(out, c.o); +} + +std::ostream &smt2_format_rec(std::ostream &, const exprt &); +std::ostream &smt2_format_rec(std::ostream &, const typet &); + +#endif // CPROVER_SOLVERS_SMT2_SMT2_FORMAT_H diff --git a/src/solvers/smt2/smt2_parser.cpp b/src/solvers/smt2/smt2_parser.cpp index 900900ae6d8..598c01c688b 100644 --- a/src/solvers/smt2/smt2_parser.cpp +++ b/src/solvers/smt2/smt2_parser.cpp @@ -8,23 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com #include "smt2_parser.h" -#include - -std::ostream &operator<<(std::ostream &out, const smt2_parsert::smt2_format &f) -{ - if(f.type.id() == ID_unsignedbv) - out << "(_ BitVec " << to_unsignedbv_type(f.type).get_width() << ')'; - else if(f.type.id() == ID_bool) - out << "Bool"; - else if(f.type.id() == ID_integer) - out << "Int"; - else if(f.type.id() == ID_real) - out << "Real"; - else - out << "? " << f.type.id(); +#include "smt2_format.h" - return out; -} +#include void smt2_parsert::command_sequence() { diff --git a/src/solvers/smt2/smt2_parser.h b/src/solvers/smt2/smt2_parser.h index 19acb751630..1c787bc93d3 100644 --- a/src/solvers/smt2/smt2_parser.h +++ b/src/solvers/smt2/smt2_parser.h @@ -43,15 +43,6 @@ class smt2_parsert:public smt2_tokenizert using id_mapt=std::map; id_mapt id_map; - struct smt2_format - { - explicit smt2_format(const typet &_type) : type(_type) - { - } - - const typet type; - }; - protected: bool exit; void command_sequence(); @@ -91,6 +82,4 @@ class smt2_parsert:public smt2_tokenizert exprt cast_bv_to_unsigned(const exprt &); }; -std::ostream &operator<<(std::ostream &, const smt2_parsert::smt2_format &); - #endif // CPROVER_SOLVERS_SMT2_SMT2_PARSER_H diff --git a/src/solvers/smt2/smt2_solver.cpp b/src/solvers/smt2/smt2_solver.cpp index 07d324edb4b..eaad9d8a00e 100644 --- a/src/solvers/smt2/smt2_solver.cpp +++ b/src/solvers/smt2/smt2_solver.cpp @@ -6,11 +6,13 @@ Author: Daniel Kroening, kroening@kroening.com \*******************************************************************/ +#include "smt2_parser.h" + +#include "smt2_format.h" + #include #include -#include "smt2_parser.h" - #include #include #include @@ -23,11 +25,8 @@ Author: Daniel Kroening, kroening@kroening.com class smt2_solvert:public smt2_parsert { public: - smt2_solvert( - std::istream &_in, - decision_proceduret &_solver): - smt2_parsert(_in), - solver(_solver) + smt2_solvert(std::istream &_in, decision_proceduret &_solver) + : smt2_parsert(_in), solver(_solver), status(NOT_SOLVED) { } @@ -39,6 +38,13 @@ class smt2_solvert:public smt2_parsert void expand_function_applications(exprt &); std::set constants_done; + + enum + { + NOT_SOLVED, + SAT, + UNSAT + } status; }; void smt2_solvert::define_constants(const exprt &expr) @@ -139,14 +145,17 @@ void smt2_solvert::command(const std::string &c) { case decision_proceduret::resultt::D_SATISFIABLE: std::cout << "sat\n"; + status = SAT; break; case decision_proceduret::resultt::D_UNSATISFIABLE: std::cout << "unsat\n"; + status = UNSAT; break; case decision_proceduret::resultt::D_ERROR: std::cout << "error\n"; + status = NOT_SOLVED; } } else if(c=="check-sat-assuming") @@ -162,6 +171,63 @@ void smt2_solvert::command(const std::string &c) std::cout << e.pretty() << '\n'; // need to do an 'smt2_format' } } + else if(c == "get-value") + { + std::vector ops; + + if(next_token() != OPEN) + throw "get-value expects list as argument"; + + while(peek() != CLOSE && peek() != END_OF_FILE) + ops.push_back(expression()); // any term + + if(next_token() != CLOSE) + throw "get-value expects ')' at end of list"; + + if(status != SAT) + throw "model is not available"; + + std::vector values; + values.reserve(ops.size()); + + for(const auto &op : ops) + { + if(op.id() != ID_symbol) + throw "get-value expects symbol"; + + const auto &identifier = to_symbol_expr(op).get_identifier(); + + const auto id_map_it = id_map.find(identifier); + + if(id_map_it == id_map.end()) + throw "unexpected symbol " + id2string(identifier); + + exprt value; + + if(id_map_it->second.definition.is_nil()) + value = solver.get(op); + else + value = solver.get(id_map_it->second.definition); + + if(value.is_nil()) + throw "no value for " + id2string(identifier); + + values.push_back(value); + } + + std::cout << '('; + + for(std::size_t op_nr = 0; op_nr < ops.size(); op_nr++) + { + if(op_nr != 0) + std::cout << "\n "; + + std::cout << '(' << smt2_format(ops[op_nr]) << ' ' + << smt2_format(values[op_nr]) << ')'; + } + + std::cout << ")\n"; + } else if(c=="simplify") { // this is a command that Z3 appears to implement @@ -195,7 +261,6 @@ void smt2_solvert::command(const std::string &c) | ( get-proof ) | ( get-unsat-assumptions ) | ( get-unsat-core ) - | ( get-value ( htermi + ) ) | ( pop hnumerali ) | ( push hnumerali ) | ( reset )