Skip to content

Commit

Permalink
fix timeouts
Browse files Browse the repository at this point in the history
  • Loading branch information
Mark Law committed Dec 20, 2023
1 parent 03fbe76 commit c3e0e70
Show file tree
Hide file tree
Showing 2 changed files with 20 additions and 6 deletions.
2 changes: 1 addition & 1 deletion FastLAS2/implementation/meta_programs/Solve.h
Original file line number Diff line number Diff line change
Expand Up @@ -51,13 +51,13 @@ function onModel(m)
end
end
new_model = new_model.." b"..tostring(intermediate_penalty).."| ;|"
print(new_model)
end
function main(prg)
new_model = ""
prg:ground({{"base", {}}})
prg:solve{on_model=onModel}
print(new_model)
end
#end.
)";
Expand Down
24 changes: 19 additions & 5 deletions FastLAS2/implementation/stages/Solve.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -155,28 +155,42 @@ void FastLAS::solve_final_task(string program) {
exit(0);
}


set<set<Schema::RuleSchema*>> i_sat_disjs;
set<string> i_sat_intermediate_facts;
int i_hypothesis_length = 0;

Clingo(ss.str(),
((FastLAS::timeout < 0) ? " " : "--time=" + std::to_string(FastLAS::timeout) + " ")
+ "--opt-strat=usc,stratify")
('i', [&](const string& atom) {
auto rule = Schema::RuleSchema::get_schema(stoi(atom));
hypothesis_length += rule->get_score();
i_hypothesis_length += rule->get_score();
solution_ss << rule->print() << endl;
}) ('b', [&](const string& atom) {
hypothesis_length += stoi(atom);
i_hypothesis_length += stoi(atom);
}) ('d', [&](const string& atom) {
sat_disjs.insert(int_to_disj[stoi(atom)]);
i_sat_disjs.insert(int_to_disj[stoi(atom)]);
}) ('p', [&](const string& atom) {
sat_intermediate_facts.insert(atom);
i_sat_intermediate_facts.insert(atom);
}) ([&]() {
sat = true;

sat_intermediate_facts = i_sat_intermediate_facts;
sat_disjs = i_sat_disjs;
solution = solution_ss.str();
hypothesis_length = i_hypothesis_length;

solution_ss.str("");
i_sat_intermediate_facts.clear();
i_sat_disjs.clear();
i_hypothesis_length = 0;
}
);

if(!sat) {
solution = "UNSATISFIABLE";
} else {
solution = solution_ss.str();
boost::replace_all(solution, "n_v_a_r", "V");
boost::replace_all(solution, "v_a_r", "V");
boost::replace_all(solution, "naf__", "not ");
Expand Down

0 comments on commit c3e0e70

Please sign in to comment.