mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-13 20:38:43 +00:00
Code Activity

code reorg

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-11-01 12:47:24 -07:00
parent 26ffee95fc
commit ef0ee9a0c4
2 changed files with 91 additions and 73 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

80
src/tactic/goal.cpp
View file

@ -22,6 +22,13 @@ Revision History:
#include"for_each_expr.h"
#include"well_sorted.h"
goal::precision goal::mk_union(precision p1, precision p2) {
if (p1 == PRECISE) return p2;
if (p2 == PRECISE) return p1;
if (p1 != p2) return UNDER_OVER;
return p1;
}
std::ostream & operator<<(std::ostream & out, goal::precision p) {
switch (p) {
case goal::PRECISE: out << "precise"; break;
@ -32,6 +39,58 @@ std::ostream & operator<<(std::ostream & out, goal::precision p) {
return out;
}
goal::goal(ast_manager & m, bool models_enabled, bool core_enabled):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(m.proofs_enabled()),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
}
goal::goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(proofs_enabled),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
SASSERT(!proofs_enabled || m.proofs_enabled());
}
goal::goal(goal const & src):
m_manager(src.m()),
m_ref_count(0),
m_depth(0),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(PRECISE) {
copy_from(src);
}
// Copy configuration: depth, models/proofs/cores flags, and precision from src.
// The assertions are not copied
goal::goal(goal const & src, bool):
m_manager(src.m()),
m_ref_count(0),
m_depth(src.m_depth),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(src.m_precision) {
}
goal::~goal() {
reset_core();
}
void goal::copy_to(goal & target) const {
SASSERT(&m_manager == &(target.m_manager));
if (this == &target)
@ -570,6 +629,27 @@ goal * goal::translate(ast_translation & translator) const {
return res;
}
bool goal::sat_preserved() const {
return prec() == PRECISE || prec() == UNDER;
}
bool goal::unsat_preserved() const {
return prec() == PRECISE || prec() == OVER;
}
bool goal::is_decided_sat() const {
return size() == 0 && sat_preserved();
}
bool goal::is_decided_unsat() const {
return inconsistent() && unsat_preserved();
}
bool goal::is_decided() const {
return is_decided_sat() || is_decided_unsat();
}
bool is_equal(goal const & s1, goal const & s2) {
if (s1.size() != s2.size())
return false;

84
src/tactic/goal.h
View file

@ -45,12 +45,7 @@ public:
UNDER_OVER // goal is garbage: the produce of combined under and over approximation steps.
};
static precision mk_union(precision p1, precision p2) {
if (p1 == PRECISE) return p2;
if (p2 == PRECISE) return p1;
if (p1 != p2) return UNDER_OVER;
return p1;
}
static precision mk_union(precision p1, precision p2);
protected:
ast_manager & m_manager;
@ -78,55 +73,13 @@ protected:
void reset_core();
public:
goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(m.proofs_enabled()),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
}
goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled):
m_manager(m),
m_ref_count(0),
m_depth(0),
m_models_enabled(models_enabled),
m_proofs_enabled(proofs_enabled),
m_core_enabled(core_enabled),
m_inconsistent(false),
m_precision(PRECISE) {
SASSERT(!proofs_enabled || m.proofs_enabled());
}
goal(goal const & src):
m_manager(src.m()),
m_ref_count(0),
m_depth(0),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(PRECISE) {
copy_from(src);
}
goal(ast_manager & m, bool models_enabled = true, bool core_enabled = false);
goal(ast_manager & m, bool proofs_enabled, bool models_enabled, bool core_enabled);
goal(goal const & src);
// Copy configuration: depth, models/proofs/cores flags, and precision from src.
// The assertions are not copied
goal(goal const & src, bool):
m_manager(src.m()),
m_ref_count(0),
m_depth(src.m_depth),
m_models_enabled(src.models_enabled()),
m_proofs_enabled(src.proofs_enabled()),
m_core_enabled(src.unsat_core_enabled()),
m_inconsistent(false),
m_precision(src.m_precision) {
}
~goal() { reset_core(); }
goal(goal const & src, bool);
~goal();
void inc_ref() { ++m_ref_count; }
void dec_ref() { --m_ref_count; if (m_ref_count == 0) dealloc(this); }
@ -181,26 +134,11 @@ public:
void display_with_dependencies(ast_printer_context & ctx) const;
void display_with_dependencies(std::ostream & out) const;
bool sat_preserved() const {
return prec() == PRECISE || prec() == UNDER;
}
bool unsat_preserved() const {
return prec() == PRECISE || prec() == OVER;
}
bool is_decided_sat() const {
return size() == 0 && sat_preserved();
}
bool is_decided_unsat() const {
return inconsistent() && unsat_preserved();
}
bool is_decided() const {
return is_decided_sat() || is_decided_unsat();
}
bool sat_preserved() const;
bool unsat_preserved() const;
bool is_decided_sat() const;
bool is_decided_unsat() const;
bool is_decided() const;
bool is_well_sorted() const;
goal * translate(ast_translation & translator) const;