Skip to content
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

Feat: add z3 maxsat support #12

Open
wants to merge 8 commits into
base: main
Choose a base branch
from
Open

Feat: add z3 maxsat support #12

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
e928466
prevent suffix for `Real`
timbeurskens Dec 19, 2024
60ca43a
add commands from maximal satisfaction paper
timbeurskens Dec 19, 2024
99c45c6
add `maximize` and `minimize` to solver
timbeurskens Dec 19, 2024
4ae57d0
add `assert_soft` to solver
timbeurskens Dec 19, 2024
7c842e9
fix function signature for assert-soft
timbeurskens Dec 19, 2024
6d24e85
use `Real` division for `impl Div`
timbeurskens Dec 19, 2024
16f524c
allow custimization of optimization priorities
timbeurskens Dec 19, 2024
4d4e0a6
add support for z3 `eval` command
timbeurskens Dec 20, 2024
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
217 changes: 215 additions & 2 deletions lowlevel/src/ast.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1406,6 +1406,14 @@ pub enum Command {
SetOption(Option),
/// `(simplify <term>)`
Simplify(Term),
/// `(eval <term>)`
Eval(Term),
/// `(maximize <term>)`
Maximize(Term),
/// `(minimize <term>)`
Minimize(Term),
/// `(assert-soft <term> <optimization_attribute>*)`
AssertSoft(Term, Vec<OptimizationAttribute>),
}
impl std::fmt::Display for Command {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
Expand Down Expand Up @@ -1459,6 +1467,12 @@ impl std::fmt::Display for Command {
Self::SetLogic(m0) => write!(f, "(set-logic {})", m0),
Self::SetOption(m0) => write!(f, "(set-option {})", m0),
Self::Simplify(m0) => write!(f, "(simplify {})", m0),
Self::Eval(m0) => write!(f, "(eval {})", m0),
Self::Maximize(m0) => write!(f, "(maximize {})", m0),
Self::Minimize(m0) => write!(f, "(minimize {})", m0),
Self::AssertSoft(m0, m1) => {
write!(f, "(assert-soft {} {})", m0, m1.iter().format(" "))
}
}
}
}
Expand All @@ -1485,6 +1499,14 @@ impl SmtlibParse for Command {
|| (p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Reserved, "check-sat-assuming")
&& p.nth(offset + 2) == Token::LParen)
|| (p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "assert-soft"))
|| (p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "minimize"))
|| (p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "maximize"))
|| (p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "eval"))
|| (p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "simplify"))
|| (p.nth(offset) == Token::LParen
Expand Down Expand Up @@ -1633,6 +1655,44 @@ impl SmtlibParse for Command {
#[allow(clippy::useless_conversion)]
return Ok(Self::CheckSatAssuming(m0.into()));
}
if p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "assert-soft")
{
p.expect(Token::LParen)?;
p.expect_matches(Token::Symbol, "assert-soft")?;
let m0 = <Term as SmtlibParse>::parse(p)?;
let m1 = p.any::<OptimizationAttribute>()?;
p.expect(Token::RParen)?;
#[allow(clippy::useless_conversion)]
return Ok(Self::AssertSoft(m0.into(), m1.into()));
}
if p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "minimize")
{
p.expect(Token::LParen)?;
p.expect_matches(Token::Symbol, "minimize")?;
let m0 = <Term as SmtlibParse>::parse(p)?;
p.expect(Token::RParen)?;
#[allow(clippy::useless_conversion)] return Ok(Self::Minimize(m0.into()));
}
if p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "maximize")
{
p.expect(Token::LParen)?;
p.expect_matches(Token::Symbol, "maximize")?;
let m0 = <Term as SmtlibParse>::parse(p)?;
p.expect(Token::RParen)?;
#[allow(clippy::useless_conversion)] return Ok(Self::Maximize(m0.into()));
}
if p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "eval")
{
p.expect(Token::LParen)?;
p.expect_matches(Token::Symbol, "eval")?;
let m0 = <Term as SmtlibParse>::parse(p)?;
p.expect(Token::RParen)?;
#[allow(clippy::useless_conversion)] return Ok(Self::Eval(m0.into()));
}
if p.nth(offset) == Token::LParen
&& p.nth_matches(offset + 1, Token::Symbol, "simplify")
{
Expand Down Expand Up @@ -1902,6 +1962,10 @@ impl Command {
Self::SetLogic(_) => false,
Self::SetOption(_) => false,
Self::Simplify(_) => true,
Self::Eval(_) => true,
Self::Maximize(_) => false,
Self::Minimize(_) => false,
Self::AssertSoft(_, _) => false,
}
}
pub fn parse_response(
Expand Down Expand Up @@ -2044,7 +2108,68 @@ impl Command {
),
)
}
Self::Eval(_) => {
Ok(
Some(
SpecificSuccessResponse::EvalResponse(
EvalResponse::parse(response)?,
),
),
)
}
Self::Maximize(_) => Ok(None),
Self::Minimize(_) => Ok(None),
Self::AssertSoft(_, _) => Ok(None),
}
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum OptimizationAttribute {
/// `:weight <numeral>`
Weight(Numeral),
/// `:id <symbol>`
Id(Symbol),
/// `<attribute>`
Attribute(Attribute),
}
impl std::fmt::Display for OptimizationAttribute {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
match self {
Self::Weight(m0) => write!(f, ":weight {}", m0),
Self::Id(m0) => write!(f, ":id {}", m0),
Self::Attribute(m0) => write!(f, "{}", m0),
}
}
}
impl OptimizationAttribute {
pub fn parse(src: &str) -> Result<Self, ParseError> {
SmtlibParse::parse(&mut Parser::new(src))
}
}
impl SmtlibParse for OptimizationAttribute {
fn is_start_of(offset: usize, p: &mut Parser) -> bool {
(p.nth_matches(offset, Token::Keyword, ":id"))
|| (p.nth_matches(offset, Token::Keyword, ":weight"))
|| (Attribute::is_start_of(offset, p))
}
fn parse(p: &mut Parser) -> Result<Self, ParseError> {
let offset = 0;
if p.nth_matches(offset, Token::Keyword, ":id") {
p.expect_matches(Token::Keyword, ":id")?;
let m0 = <Symbol as SmtlibParse>::parse(p)?;
#[allow(clippy::useless_conversion)] return Ok(Self::Id(m0.into()));
}
if p.nth_matches(offset, Token::Keyword, ":weight") {
p.expect_matches(Token::Keyword, ":weight")?;
let m0 = <Numeral as SmtlibParse>::parse(p)?;
#[allow(clippy::useless_conversion)] return Ok(Self::Weight(m0.into()));
}
if Attribute::is_start_of(offset, p) {
let m0 = <Attribute as SmtlibParse>::parse(p)?;
#[allow(clippy::useless_conversion)] return Ok(Self::Attribute(m0.into()));
}
Err(p.stuck("optimization_attribute"))
}
}
/// `<command>*`
Expand Down Expand Up @@ -2101,6 +2226,8 @@ pub enum Option {
ReproducibleResourceLimit(Numeral),
/// `:verbosity <numeral>`
Verbosity(Numeral),
/// `:opt.priority <optimization_priority>`
OptPriority(OptimizationPriority),
/// `<attribute>`
Attribute(Attribute),
}
Expand All @@ -2127,6 +2254,7 @@ impl std::fmt::Display for Option {
write!(f, ":reproducible-resource-limit {}", m0)
}
Self::Verbosity(m0) => write!(f, ":verbosity {}", m0),
Self::OptPriority(m0) => write!(f, ":opt.priority {}", m0),
Self::Attribute(m0) => write!(f, "{}", m0),
}
}
Expand All @@ -2138,7 +2266,8 @@ impl Option {
}
impl SmtlibParse for Option {
fn is_start_of(offset: usize, p: &mut Parser) -> bool {
(p.nth_matches(offset, Token::Keyword, ":verbosity"))
(p.nth_matches(offset, Token::Keyword, ":opt.priority"))
|| (p.nth_matches(offset, Token::Keyword, ":verbosity"))
|| (p.nth_matches(offset, Token::Keyword, ":reproducible-resource-limit"))
|| (p.nth_matches(offset, Token::Keyword, ":regular-output-channel"))
|| (p.nth_matches(offset, Token::Keyword, ":random-seed"))
Expand All @@ -2156,6 +2285,11 @@ impl SmtlibParse for Option {
}
fn parse(p: &mut Parser) -> Result<Self, ParseError> {
let offset = 0;
if p.nth_matches(offset, Token::Keyword, ":opt.priority") {
p.expect_matches(Token::Keyword, ":opt.priority")?;
let m0 = <OptimizationPriority as SmtlibParse>::parse(p)?;
#[allow(clippy::useless_conversion)] return Ok(Self::OptPriority(m0.into()));
}
if p.nth_matches(offset, Token::Keyword, ":verbosity") {
p.expect_matches(Token::Keyword, ":verbosity")?;
let m0 = <Numeral as SmtlibParse>::parse(p)?;
Expand Down Expand Up @@ -2247,6 +2381,53 @@ impl SmtlibParse for Option {
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum OptimizationPriority {
/// `pareto`
Pareto,
/// `lex`
Lex,
/// `box`
Box,
}
impl std::fmt::Display for OptimizationPriority {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
match self {
Self::Pareto => write!(f, "pareto"),
Self::Lex => write!(f, "lex"),
Self::Box => write!(f, "box"),
}
}
}
impl OptimizationPriority {
pub fn parse(src: &str) -> Result<Self, ParseError> {
SmtlibParse::parse(&mut Parser::new(src))
}
}
impl SmtlibParse for OptimizationPriority {
fn is_start_of(offset: usize, p: &mut Parser) -> bool {
(p.nth_matches(offset, Token::Symbol, "box"))
|| (p.nth_matches(offset, Token::Symbol, "lex"))
|| (p.nth_matches(offset, Token::Symbol, "pareto"))
}
fn parse(p: &mut Parser) -> Result<Self, ParseError> {
let offset = 0;
if p.nth_matches(offset, Token::Symbol, "box") {
p.expect_matches(Token::Symbol, "box")?;
#[allow(clippy::useless_conversion)] return Ok(Self::Box);
}
if p.nth_matches(offset, Token::Symbol, "lex") {
p.expect_matches(Token::Symbol, "lex")?;
#[allow(clippy::useless_conversion)] return Ok(Self::Lex);
}
if p.nth_matches(offset, Token::Symbol, "pareto") {
p.expect_matches(Token::Symbol, "pareto")?;
#[allow(clippy::useless_conversion)] return Ok(Self::Pareto);
}
Err(p.stuck("optimization_priority"))
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum InfoFlag {
/// `:all-statistics`
AllStatistics,
Expand Down Expand Up @@ -2951,6 +3132,29 @@ impl SmtlibParse for SimplifyResponse {
Ok(Self(m0))
}
}
/// `<term>`
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub struct EvalResponse(pub Term);
impl std::fmt::Display for EvalResponse {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
write!(f, "{}", self.0)
}
}
impl EvalResponse {
pub fn parse(src: &str) -> Result<Self, ParseError> {
SmtlibParse::parse(&mut Parser::new(src))
}
}
impl SmtlibParse for EvalResponse {
fn is_start_of(offset: usize, p: &mut Parser) -> bool {
Term::is_start_of(offset, p)
}
fn parse(p: &mut Parser) -> Result<Self, ParseError> {
let m0 = <Term as SmtlibParse>::parse(p)?;
Ok(Self(m0))
}
}
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
#[cfg_attr(feature = "serde", derive(serde::Serialize, serde::Deserialize))]
pub enum SpecificSuccessResponse {
Expand Down Expand Up @@ -2978,6 +3182,8 @@ pub enum SpecificSuccessResponse {
GetValueResponse(GetValueResponse),
/// `<simplify_response>`
SimplifyResponse(SimplifyResponse),
/// `<eval_response>`
EvalResponse(EvalResponse),
}
impl std::fmt::Display for SpecificSuccessResponse {
fn fmt(&self, f: &mut std::fmt::Formatter) -> std::fmt::Result {
Expand All @@ -2994,6 +3200,7 @@ impl std::fmt::Display for SpecificSuccessResponse {
Self::GetUnsatCoreResponse(m0) => write!(f, "{}", m0),
Self::GetValueResponse(m0) => write!(f, "{}", m0),
Self::SimplifyResponse(m0) => write!(f, "{}", m0),
Self::EvalResponse(m0) => write!(f, "{}", m0),
}
}
}
Expand All @@ -3004,7 +3211,8 @@ impl SpecificSuccessResponse {
}
impl SmtlibParse for SpecificSuccessResponse {
fn is_start_of(offset: usize, p: &mut Parser) -> bool {
(SimplifyResponse::is_start_of(offset, p))
(EvalResponse::is_start_of(offset, p))
|| (SimplifyResponse::is_start_of(offset, p))
|| (GetValueResponse::is_start_of(offset, p))
|| (GetUnsatCoreResponse::is_start_of(offset, p))
|| (GetProofResponse::is_start_of(offset, p))
Expand All @@ -3019,6 +3227,11 @@ impl SmtlibParse for SpecificSuccessResponse {
}
fn parse(p: &mut Parser) -> Result<Self, ParseError> {
let offset = 0;
if EvalResponse::is_start_of(offset, p) {
let m0 = <EvalResponse as SmtlibParse>::parse(p)?;
#[allow(clippy::useless_conversion)]
return Ok(Self::EvalResponse(m0.into()));
}
if SimplifyResponse::is_start_of(offset, p) {
let m0 = <SimplifyResponse as SmtlibParse>::parse(p)?;
#[allow(clippy::useless_conversion)]
Expand Down
Loading