From 1239c8f8e885f82a89e965f229c65c67f731e631 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jul 2016 11:20:31 -0700 Subject: [PATCH 1/3] update MSF example Signed-off-by: Nikolaj Bjorner --- .../Properties/AssemblyInfo.cs | 36 +++++++++++++++++++ .../Z3BaseSolver.cs | 8 ++--- 2 files changed, 40 insertions(+), 4 deletions(-) create mode 100644 examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs new file mode 100644 index 000000000..6d495a895 --- /dev/null +++ b/examples/msf/SolverFoundation.Plugin.Z3/Properties/AssemblyInfo.cs @@ -0,0 +1,36 @@ +using System.Reflection; +using System.Runtime.CompilerServices; +using System.Runtime.InteropServices; + +// General Information about an assembly is controlled through the following +// set of attributes. Change these attribute values to modify the information +// associated with an assembly. +[assembly: AssemblyTitle("SolverFoundation.Plugin.Z3")] +[assembly: AssemblyDescription("")] +[assembly: AssemblyConfiguration("")] +[assembly: AssemblyCompany("Microsoft")] +[assembly: AssemblyProduct("SolverFoundation.Plugin.Z3")] +[assembly: AssemblyCopyright("Copyright © Microsoft 2010")] +[assembly: AssemblyTrademark("")] +[assembly: AssemblyCulture("")] + +// Setting ComVisible to false makes the types in this assembly not visible +// to COM components. If you need to access a type in this assembly from +// COM, set the ComVisible attribute to true on that type. +[assembly: ComVisible(false)] + +// The following GUID is for the ID of the typelib if this project is exposed to COM +[assembly: Guid("ed1476c0-96de-4d2c-983d-3888b140c3ad")] + +// Version information for an assembly consists of the following four values: +// +// Major Version +// Minor Version +// Build Number +// Revision +// +// You can specify all the values or you can default the Build and Revision Numbers +// by using the '*' as shown below: +// [assembly: AssemblyVersion("1.0.*")] +[assembly: AssemblyVersion("1.0.0.0")] +[assembly: AssemblyFileVersion("1.0.0.0")] diff --git a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs index af8bc92a2..1c82406be 100644 --- a/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs +++ b/examples/msf/SolverFoundation.Plugin.Z3/Z3BaseSolver.cs @@ -47,7 +47,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 private Dictionary _variables = new Dictionary(); /// A map from MSF variable ids to Z3 goal ids - private Dictionary _goals = new Dictionary(); + private Dictionary _goals = new Dictionary(); internal Z3BaseSolver(IRowVariableModel model) { @@ -64,7 +64,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 get { return _variables; } } - internal Dictionary Goals + internal Dictionary Goals { get { return _goals; } } @@ -332,7 +332,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 // Remember all objective values foreach (var pair in _goals) { - var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value)); + var optimalValue = Utils.ToRational(pair.Value.Upper); _model.SetValue(pair.Key.Index, optimalValue); } model.Dispose(); @@ -356,7 +356,7 @@ namespace Microsoft.SolverFoundation.Plugin.Z3 // Remember all objective values foreach (var pair in _goals) { - var optimalValue = Utils.ToRational(_optSolver.GetUpper(pair.Value)); + var optimalValue = Utils.ToRational(pair.Value.Upper); _model.SetValue(pair.Key.Index, optimalValue); } subOptimalModel.Dispose(); From 0997eba700b3a2b5b7c989aea47a7e50d55bb470 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jul 2016 13:41:41 -0700 Subject: [PATCH 2/3] adding hash/eq to uint_set Signed-off-by: Nikolaj Bjorner --- src/test/uint_set.cpp | 27 +++++++++++++++++++++++++++ src/util/uint_set.h | 12 ++++++++++++ 2 files changed, 39 insertions(+) diff --git a/src/test/uint_set.cpp b/src/test/uint_set.cpp index 582a1d42f..fcbbd5c48 100644 --- a/src/test/uint_set.cpp +++ b/src/test/uint_set.cpp @@ -131,6 +131,32 @@ static void tst4() { SASSERT(!s.contains(0)); } +#include "map.h" + +template +struct uint_map : public map {}; + +static void tst5() { + uint_set s; + std::cout << s.get_hash() << "\n"; + s.insert(1); + std::cout << s.get_hash() << "\n"; + s.insert(2); + std::cout << s.get_hash() << "\n"; + s.insert(44); + std::cout << s.get_hash() << "\n"; + + uint_map m; + m.insert(s, 1); + s.insert(4); + m.insert(s, 3); + uint_map::iterator it = m.begin(), end = m.end(); + for (; it != end; ++it) { + std::cout << it->m_key << " : " << it->m_value << "\n"; + } + +} + void tst_uint_set() { for (unsigned i = 0; i < 100; i++) { tst1(1 + rand()%31); @@ -146,5 +172,6 @@ void tst_uint_set() { tst3(12); tst3(100); tst4(); + tst5(); } diff --git a/src/util/uint_set.h b/src/util/uint_set.h index aca73a5c5..525638f4f 100644 --- a/src/util/uint_set.h +++ b/src/util/uint_set.h @@ -218,6 +218,18 @@ public: iterator const begin() const { return iterator(*this, false); } iterator const end() const { return iterator(*this, true); } + + unsigned get_hash() const { + unsigned h = 0; + for (unsigned i = 0; i < size(); ++i) { + h += (i+1)*((*this)[i]); + } + return h; + } + + struct eq { bool operator()(uint_set const& s1, uint_set const& s2) const { return s1 == s2; } }; + struct hash { unsigned operator()(uint_set const& s) const { return s.get_hash(); } }; + }; inline std::ostream & operator<<(std::ostream & target, const uint_set & s) { From b7de813c6386a5625c5570c99d8daf0b00e245f8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 27 Jul 2016 15:35:44 -0700 Subject: [PATCH 3/3] set solver on simplify command Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.h | 3 +++ src/ast/rewriter/th_rewriter.cpp | 9 +++++++++ src/ast/rewriter/th_rewriter.h | 5 +++++ src/cmd_context/simplify_cmd.cpp | 25 ++++++++++++++++++++++++- src/solver/solver.h | 9 +++++++-- 5 files changed, 48 insertions(+), 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index 82579d53a..2b434f475 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -149,6 +149,9 @@ public: void updt_params(params_ref const & p) {} static void get_param_descrs(param_descrs & r) {} + void set_solver(expr_solver* solver) { m_re2aut.set_solver(solver); } + + br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result); br_status mk_eq_core(expr * lhs, expr * rhs, expr_ref & result); diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index 6f6daf8df..ff6a10274 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -692,6 +692,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return false; } + }; template class rewriter_tpl; @@ -705,6 +706,10 @@ struct th_rewriter::imp : public rewriter_tpl { expr_ref mk_app(func_decl* f, unsigned sz, expr* const* args) { return m_cfg.mk_app(f, sz, args); } + + void set_solver(expr_solver* solver) { + m_cfg.m_seq_rw.set_solver(solver); + } }; th_rewriter::th_rewriter(ast_manager & m, params_ref const & p): @@ -790,3 +795,7 @@ void th_rewriter::reset_used_dependencies() { expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args) { return m_imp->mk_app(f, num_args, args); } + +void th_rewriter::set_solver(expr_solver* solver) { + m_imp->set_solver(solver); +} diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h index bd5ce9c66..6aa4bb3da 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -25,6 +25,8 @@ Notes: class expr_substitution; +class expr_solver; + class th_rewriter { struct imp; imp * m_imp; @@ -58,6 +60,9 @@ public: // Remark: reset_used_dependecies will reset the internal cache if get_used_dependencies() != 0 expr_dependency * get_used_dependencies(); void reset_used_dependencies(); + + void set_solver(expr_solver* solver); + }; #endif diff --git a/src/cmd_context/simplify_cmd.cpp b/src/cmd_context/simplify_cmd.cpp index 1c249ce1f..8b354c8b7 100644 --- a/src/cmd_context/simplify_cmd.cpp +++ b/src/cmd_context/simplify_cmd.cpp @@ -24,9 +24,30 @@ Notes: #include"scoped_timer.h" #include"scoped_ctrl_c.h" #include"cancel_eh.h" +#include"seq_rewriter.h" #include class simplify_cmd : public parametric_cmd { + + class th_solver : public expr_solver { + cmd_context& m_ctx; + params_ref m_params; + ref m_solver; + public: + th_solver(cmd_context& ctx): m_ctx(ctx) {} + + virtual lbool check_sat(expr* e) { + if (!m_solver) { + m_solver = m_ctx.get_solver_factory()(m_ctx.m(), m_params, false, true, false, symbol::null); + } + m_solver->push(); + m_solver->assert_expr(e); + lbool r = m_solver->check_sat(0,0); + m_solver->pop(1); + return r; + } + }; + expr * m_target; public: simplify_cmd(char const * name = "simplify"):parametric_cmd(name) {} @@ -70,10 +91,12 @@ public: if (m_params.get_bool("som", false)) m_params.set_bool("flat", true); th_rewriter s(ctx.m(), m_params); + th_solver solver(ctx); + s.set_solver(alloc(th_solver, ctx)); unsigned cache_sz; unsigned num_steps = 0; unsigned timeout = m_params.get_uint("timeout", UINT_MAX); - unsigned rlimit = m_params.get_uint("rlimit", UINT_MAX); + unsigned rlimit = m_params.get_uint("rlimit", UINT_MAX); bool failed = false; cancel_eh eh(ctx.m().limit()); { diff --git a/src/solver/solver.h b/src/solver/solver.h index f320bec7c..e4e4942d3 100644 --- a/src/solver/solver.h +++ b/src/solver/solver.h @@ -149,8 +149,13 @@ public: */ virtual expr * get_assumption(unsigned idx) const = 0; - - + /** + \brief under assumptions, asms, retrieve set of consequences that fix values for expressions that can be + built from fns. For functions that take 0 arguments, we require that the function returns all consequences + that mention these functions. The consequences are clauses whose first literal constrain one of the + functions from fns and the other literals are negations of literals from asms. + */ + //virtual lbool get_consequences(expr_ref_vector const& asms, func_ref_vector const& fns, expr_ref_vector& consequences); /** \brief Display the content of this solver.