mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-28 08:58:44 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-08-17 15:59:40 -07:00
commit d15f8c52a0
2 changed files with 264 additions and 246 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/api/java/Optimize.java
View file

@ -298,6 +298,24 @@ public class Optimize extends Z3Object {
return Native.optimizeToString(getContext().nCtx(), getNativeObject());
}
/**
* Parse an SMT-LIB2 file with optimization objectives and constraints.
* The parsed constraints and objectives are added to the optimization context.
*/
public void fromFile(String file)
{
Native.optimizeFromFile(getContext().nCtx(), getNativeObject(), file);
}
/**
* Similar to FromFile. Instead it takes as argument a string.
*/
public void fromString(String s)
{
Native.optimizeFromString(getContext().nCtx(), getNativeObject(), s);
}
/**
* Optimize statistics.
**/

2
src/smt/mam.cpp
View file

@ -2087,9 +2087,9 @@ namespace smt {
for (; it != end; ++it) {
enode * p = *it;
if (p->get_decl() == f &&
p->get_num_args() == num_args &&
m_context.is_relevant(p) &&
p->is_cgr() &&
i < p->get_num_args() &&
p->get_arg(i)->get_root() == n) {
v->push_back(p);
}