3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00

finish (inefficient) BMC for non-linear Horn

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-10-15 10:49:19 -07:00
commit 2c24f25050
6 changed files with 46 additions and 13 deletions

View file

@ -30,6 +30,10 @@ Version 4.2
- Z3 by default switches to an incremental solver when a Solver object is used to solve many queries. - Z3 by default switches to an incremental solver when a Solver object is used to solve many queries.
In the this version, we switch back to the tactic framework if the incremental solver returns "unknown". In the this version, we switch back to the tactic framework if the incremental solver returns "unknown".
- Allow negative numerals in the SMT 2.0 frontend. That is, Z3 SMT 2.0 parser now accepts numerals such as "-2". It is not needed to encode them as "(- 2)" anymore.
The parser still accepts -foo as a symbol. That is, it is *not* a shorthand for (- foo).
This feature is disabled when SMTLIB2_COMPLIANT=true is set in the command line.
- Now, Z3 can be compiled inside cygwin using gcc. - Now, Z3 can be compiled inside cygwin using gcc.
- Fixed bug in the unsat core generation. - Fixed bug in the unsat core generation.

View file

@ -246,6 +246,7 @@ protected:
public: public:
cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null); cmd_context(front_end_params & params, bool main_ctx = true, ast_manager * m = 0, symbol const & l = symbol::null);
~cmd_context(); ~cmd_context();
bool is_smtlib2_compliant() const { return m_params.m_smtlib2_compliant; }
void set_logic(symbol const & s); void set_logic(symbol const & s);
bool has_logic() const { return m_logic != symbol::null; } bool has_logic() const { return m_logic != symbol::null; }
symbol const & get_logic() const { return m_logic; } symbol const & get_logic() const { return m_logic; }

View file

@ -186,7 +186,7 @@ void dl_interface::collect_params(param_descrs& p) {
p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"); p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object"); p.insert(":generate-proof-trace", CPK_BOOL, "PDR: (default false) trace for 'sat' answer as proof object");
p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)"); p.insert(":inline-proofs", CPK_BOOL, "PDR: (default true) run PDR with proof mode turned on and extract Farkas coefficients directly (instead of creating a separate proof object when extracting coefficients)");
p.insert(":flexible-trace", CPK_BOOL, "PDR: (default true) allow PDR generate long counter-examples by extending candidate trace within search area"); p.insert(":flexible-trace", CPK_BOOL, "PDR: (default false) allow PDR generate long counter-examples by extending candidate trace within search area");
PRIVATE_PARAMS(p.insert(":use-farkas-model", CPK_BOOL, "PDR: (default false) enable using Farkas generalization through model propagation");); PRIVATE_PARAMS(p.insert(":use-farkas-model", CPK_BOOL, "PDR: (default false) enable using Farkas generalization through model propagation"););
PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions");); PRIVATE_PARAMS(p.insert(":use-precondition-generalizer", CPK_BOOL, "PDR: (default false) enable generalizations from weakest pre-conditions"););
PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states");); PRIVATE_PARAMS(p.insert(":use-multicore-generalizer", CPK_BOOL, "PDR: (default false) extract multiple cores for blocking states"););

View file

@ -2353,7 +2353,7 @@ namespace smt2 {
public: public:
parser(cmd_context & ctx, std::istream & is, bool interactive): parser(cmd_context & ctx, std::istream & is, bool interactive):
m_ctx(ctx), m_ctx(ctx),
m_scanner(is, interactive), m_scanner(ctx, is, interactive),
m_curr(scanner::NULL_TOKEN), m_curr(scanner::NULL_TOKEN),
m_curr_cmd(0), m_curr_cmd(0),
m_num_bindings(0), m_num_bindings(0),

View file

@ -88,16 +88,11 @@ namespace smt2 {
} }
} }
scanner::token scanner::read_symbol() { scanner::token scanner::read_symbol_core() {
SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':');
m_string.reset();
m_string.push_back(curr());
next();
while (true) { while (true) {
char c = curr(); char c = curr();
char n = m_normalized[static_cast<unsigned char>(c)]; char n = m_normalized[static_cast<unsigned char>(c)];
if (n == 'a' || n == '0') { if (n == 'a' || n == '0' || n == '-') {
m_string.push_back(c); m_string.push_back(c);
next(); next();
} }
@ -110,6 +105,14 @@ namespace smt2 {
} }
} }
scanner::token scanner::read_symbol() {
SASSERT(m_normalized[static_cast<unsigned>(curr())] == 'a' || curr() == ':' || curr() == '-');
m_string.reset();
m_string.push_back(curr());
next();
read_symbol_core();
}
scanner::token scanner::read_number() { scanner::token scanner::read_number() {
SASSERT('0' <= curr() && curr() <= '9'); SASSERT('0' <= curr() && curr() <= '9');
rational q(1); rational q(1);
@ -141,6 +144,22 @@ namespace smt2 {
return is_float ? FLOAT_TOKEN : INT_TOKEN; return is_float ? FLOAT_TOKEN : INT_TOKEN;
} }
scanner::token scanner::read_signed_number() {
SASSERT(curr() == '-');
next();
if ('0' <= curr() && curr() <= '9') {
scanner::token r = read_number();
m_number.neg();
return r;
}
else {
// it is a symbol.
m_string.reset();
m_string.push_back('-');
return read_symbol_core();
}
}
scanner::token scanner::read_string() { scanner::token scanner::read_string() {
SASSERT(curr() == '\"'); SASSERT(curr() == '\"');
next(); next();
@ -222,7 +241,8 @@ namespace smt2 {
} }
} }
scanner::scanner(std::istream& stream, bool interactive): scanner::scanner(cmd_context & ctx, std::istream& stream, bool interactive):
m_ctx(ctx),
m_interactive(interactive), m_interactive(interactive),
m_spos(0), m_spos(0),
m_curr(0), // avoid Valgrind warning m_curr(0), // avoid Valgrind warning
@ -259,7 +279,7 @@ namespace smt2 {
m_normalized[static_cast<int>('&')] = 'a'; m_normalized[static_cast<int>('&')] = 'a';
m_normalized[static_cast<int>('*')] = 'a'; m_normalized[static_cast<int>('*')] = 'a';
m_normalized[static_cast<int>('_')] = 'a'; m_normalized[static_cast<int>('_')] = 'a';
m_normalized[static_cast<int>('-')] = 'a'; m_normalized[static_cast<int>('-')] = '-';
m_normalized[static_cast<int>('+')] = 'a'; m_normalized[static_cast<int>('+')] = 'a';
m_normalized[static_cast<int>('=')] = 'a'; m_normalized[static_cast<int>('=')] = 'a';
m_normalized[static_cast<int>('<')] = 'a'; m_normalized[static_cast<int>('<')] = 'a';
@ -304,6 +324,11 @@ namespace smt2 {
return read_number(); return read_number();
case '#': case '#':
return read_bv_literal(); return read_bv_literal();
case '-':
if (m_ctx.is_smtlib2_compliant())
return read_symbol();
else
return read_signed_number();
case -1: case -1:
return EOF_TOKEN; return EOF_TOKEN;
default: { default: {

View file

@ -31,6 +31,7 @@ namespace smt2 {
class scanner { class scanner {
private: private:
cmd_context & m_ctx;
bool m_interactive; bool m_interactive;
int m_spos; // position in the current line of the stream int m_spos; // position in the current line of the stream
char m_curr; // current char; char m_curr; // current char;
@ -73,7 +74,7 @@ namespace smt2 {
EOF_TOKEN EOF_TOKEN
}; };
scanner(std::istream& stream, bool interactive = false); scanner(cmd_context & ctx, std::istream& stream, bool interactive = false);
~scanner() {} ~scanner() {}
@ -85,10 +86,12 @@ namespace smt2 {
char const * get_string() const { return m_string.begin(); } char const * get_string() const { return m_string.begin(); }
token scan(); token scan();
token read_symbol_core();
token read_symbol(); token read_symbol();
token read_quoted_symbol(); token read_quoted_symbol();
void read_comment(); void read_comment();
token read_number(); token read_number();
token read_signed_number();
token read_string(); token read_string();
token read_bv_literal(); token read_bv_literal();