Skip to content

Revert "Re enable features" #39

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
makaimann merged 1 commit into from
May 28, 2020
Merged

Revert "Re enable features" #39

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion ic3ia/utils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ msat_config get_config(ModelGeneration model, bool interpolation, bool approx)
OPT_("theory.bv.eager", "false");
// This option is a hack to handle interpolation failure in the
// case of QF_UFLIA
// OPT_("theory.la.interpolation_laz_split_mixed_eq", "false");
OPT_("theory.la.interpolation_laz_split_mixed_eq", "false");
}

OPT_("model_generation", "false");
Expand Down
107 changes: 46 additions & 61 deletions prophic3/main.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -51,9 +51,6 @@ bool check_witness(const Options &opts, TransitionSystem &ts,

int main(int argc, const char **argv)
{
// 3 is an error
int ret_status = 3;
Prover *the_prover = NULL;
try
{
Options opts = get_options(argc, argv);
Expand Down Expand Up @@ -88,92 +85,80 @@ int main(int argc, const char **argv)
LiveEncoder liveenc(product, opts);

msat_truth_value res = MSAT_UNDEF;
// final_ts is only different for prophic3 which returns the refined
// abstract system
TransitionSystem *final_ts = &product;
if (opts.bmc) {
Bmc *bmc = new Bmc(product, opts);
the_prover = bmc;
Bmc bmc(product, opts);
if (opts.bmc_max_k > 0) {
if (!bmc->check_until(opts.bmc_max_k)) {
if (!bmc.check_until(opts.bmc_max_k)) {
res = MSAT_FALSE;
}
} else {
res = bmc->prove();
res = bmc.prove();
}
} else if (opts.kind) {
Kind *kind = new Kind(product, opts);
the_prover = kind;
Kind kind(product, opts);
if (opts.bmc_max_k > 0) {
res = kind->check_until(opts.bmc_max_k);
res = kind.check_until(opts.bmc_max_k);
} else {
res = kind->prove();
res = kind.prove();
}
}
else
{
ProphIC3 *prophic3 = new ProphIC3(product, opts, liveenc, opts.verbosity);
res = prophic3->prove();
the_prover = prophic3;
final_ts = &(prophic3->get_abs_ts());
}

if (opts.witness && res != MSAT_UNDEF) {
bool safe = (res == MSAT_TRUE);
std::vector<TermList> wit;
int loopback = the_prover->witness(wit);
if (loopback == Prover::CEX_ERROR) {
std::cout << "ERROR computing witness" << std::endl;
} else {
std::cout << (safe ? "invariant" : "counterexample") << "\n";

for (size_t i = 0; i < wit.size(); ++i) {
TermList &w = wit[i];
bool loophere = loopback >= 0 && size_t(loopback) == i;
std::cout << ";; " << (loophere ? "loopback " : "")
<< (safe ? "clause " : "step ") << i << "\n"
<< (safe ? "(or" : "(and") << "\n";
for (msat_term t : w) {
std::cout << " " << logterm(env, t) << "\n";
}
std::cout << ")\n";
}
std::cout.flush();
}
double witness_check_time;

if (safe && opts.check_witness) {
TimeKeeper tk(witness_check_time);
if (!check_witness(opts, *final_ts, wit, ltl, tableau, liveenc)) {
std::cout << "ERROR: the witness is incorrect\n" << std::endl;
} else {
std::cout << "the witness is correct\n" << std::endl;
}
}
ProphIC3 prophic3(product, opts, liveenc, opts.verbosity);
res = prophic3.prove();
}

if (res == MSAT_FALSE) {
// cout << "The property is false" << endl;
cout << "unsat" << endl; // similar to spacer
ret_status = 1;
return 1;
} else if (res == MSAT_TRUE) {
// cout << "The property is true" << endl;
cout << "sat" << endl; // similar to spacer
ret_status = 0;
return 0;
} else {
// cout << "Failed to prove or disprove the property..." << endl;
cout << "unknown" << endl; // similar to spacer
ret_status = 2;
return 2;
}

// if (opts.witness && res != MSAT_UNDEF) {
// bool safe = (res == MSAT_TRUE);
// std::vector<TermList> wit;
// int loopback = prophic3.witness(wit);
// if (loopback == Prover::CEX_ERROR) {
// std::cout << "ERROR computing witness" << std::endl;
// } else {
// std::cout << (safe ? "invariant" : "counterexample") << "\n";

// for (size_t i = 0; i < wit.size(); ++i) {
// TermList &w = wit[i];
// bool loophere = loopback >= 0 && size_t(loopback) == i;
// std::cout << ";; " << (loophere ? "loopback " : "")
// << (safe ? "clause " : "step ") << i
// << "\n" << (safe ? "(or" : "(and") << "\n";
// for (msat_term t : w) {
// std::cout << " " << logterm(env, t) << "\n";
// }
// std::cout << ")\n";
// }
// std::cout.flush();
// }
// double witness_check_time;

// if (safe && opts.check_witness) {
// TransitionSystem & abs_ts = prophic3.get_abs_ts();
// TimeKeeper tk(witness_check_time);
// if (!check_witness(opts, abs_ts, wit, ltl, tableau, liveenc)) {
// std::cout << "ERROR: the witness is incorrect\n" << std::endl;
// } else {
// std::cout << "the witness is correct\n" << std::endl;
// }
// }
// }

} catch (std::exception &e) {
std::cerr << e.what() << std::endl;
ret_status = 3;
}

if (the_prover) {
delete the_prover;
return 3;
}
return ret_status;
}