From 4f630f2a009b7fda2ea7cd3bafdbb5cfe3be4e38 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 8 Feb 2018 09:09:53 -0800
Subject: [PATCH] fix configuration for compiling equalities, add extended
binaries
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/opt/opt_context.cpp | 2 +-
src/sat/sat_big.cpp | 21 +++++++++++++++++++--
src/shell/opt_frontend.cpp | 19 +++++++++++++------
3 files changed, 33 insertions(+), 9 deletions(-)
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index f2e98fa59..ec2059642 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -738,7 +738,7 @@ namespace opt {
tac3 = mk_eq2bv_tactic(m);
params_ref lia_p;
lia_p.set_bool("compile_equality", optp.pb_compile_equality());
- tac3->updt_params(lia_p);
+ tac2->updt_params(lia_p);
set_simplify(and_then(tac0.get(), tac1.get(), tac2.get(), tac3.get(), mk_simplify_tactic(m)));
}
else {
diff --git a/src/sat/sat_big.cpp b/src/sat/sat_big.cpp
index b7dc0bf8a..1845a9632 100644
--- a/src/sat/sat_big.cpp
+++ b/src/sat/sat_big.cpp
@@ -30,6 +30,7 @@ namespace sat {
unsigned num_lits = m_num_vars * 2;
literal_vector lits, r;
SASSERT(num_lits == m_dag.size() && num_lits == m_roots.size());
+ size_t_map<bool> seen_idx;
for (unsigned l_idx = 0; l_idx < num_lits; l_idx++) {
literal u = to_literal(l_idx);
if (s.was_eliminated(u.var()))
@@ -41,11 +42,27 @@ namespace sat {
m_roots[v.index()] = false;
edges.push_back(v);
}
-#if 0
+#if 1
if (w.is_ext_constraint() &&
s.m_ext &&
+ learned &&
+ !seen_idx.contains(w.get_ext_constraint_idx()) &&
s.m_ext->is_extended_binary(w.get_ext_constraint_idx(), r)) {
- IF_VERBOSE(0, verbose_stream() << "extended binary " << r.size() << "\n";);
+ seen_idx.insert(w.get_ext_constraint_idx(), true);
+ for (unsigned i = 0; i < r.size(); ++i) {
+ literal u = r[i];
+ for (unsigned j = i + 1; j < r.size(); ++j) {
+ // add r[i] -> ~r[j]
+ literal v = ~r[j];
+ m_roots[v.index()] = false;
+ m_dag[u.index()].push_back(v);
+ // add r[j] -> ~r[i]
+ v.neg();
+ u.neg();
+ m_roots[u.index()] = false;
+ m_dag[v.index()].push_back(u);
+ }
+ }
}
#endif
}
diff --git a/src/shell/opt_frontend.cpp b/src/shell/opt_frontend.cpp
index 7dcb761db..8ce573e9a 100644
--- a/src/shell/opt_frontend.cpp
+++ b/src/shell/opt_frontend.cpp
@@ -7,13 +7,14 @@ Copyright (c) 2015 Microsoft Corporation
#include<fstream>
#include<signal.h>
#include<time.h>
-#include "opt/opt_context.h"
+#include "util/gparams.h"
+#include "util/timeout.h"
#include "ast/ast_util.h"
#include "ast/arith_decl_plugin.h"
#include "ast/ast_pp.h"
-#include "util/gparams.h"
-#include "util/timeout.h"
#include "ast/reg_decl_plugins.h"
+#include "model/model_smt2_pp.h"
+#include "opt/opt_context.h"
#include "opt/opt_parse.h"
#include "shell/opt_frontend.h"
@@ -27,9 +28,15 @@ static unsigned_vector g_handles;
static void display_results() {
if (g_opt) {
- for (unsigned i = 0; i < g_handles.size(); ++i) {
- expr_ref lo = g_opt->get_lower(g_handles[i]);
- expr_ref hi = g_opt->get_upper(g_handles[i]);
+ model_ref mdl;
+ g_opt->get_model(mdl);
+ if (mdl) {
+ model_smt2_pp(std::cout, g_opt->get_manager(), *mdl, 0);
+ }
+
+ for (unsigned h : g_handles) {
+ expr_ref lo = g_opt->get_lower(h);
+ expr_ref hi = g_opt->get_upper(h);
if (lo == hi) {
std::cout << " " << lo << "\n";
}