use std::fs::File;
use std::io::{BufReader, BufWriter, Read, Write};
use std::process::{Child, ChildStdin, ChildStdout, Command, Stdio};
use crate::{
common::*,
conf::SmtConf,
parse::{ExprParser, IdentParser, ModelParser, RSmtParser, ValueParser},
};
pub static ACTLIT_PREF: &str = "|rsmt2 actlit ";
pub static ACTLIT_SUFF: &str = "|";
#[derive(Debug)]
pub struct Actlit {
id: usize,
}
impl Actlit {
pub fn uid(&self) -> usize {
self.id
}
pub fn write<W>(&self, w: &mut W) -> SmtRes<()>
where
W: Write,
{
write!(w, "{}{}{}", ACTLIT_PREF, self.id, ACTLIT_SUFF)?;
Ok(())
}
}
impl Expr2Smt<()> for Actlit {
fn expr_to_smt2<Writer>(&self, w: &mut Writer, _: ()) -> SmtRes<()>
where
Writer: ::std::io::Write,
{
self.write(w)
}
}
impl ::std::ops::Deref for Actlit {
type Target = usize;
fn deref(&self) -> &usize {
&self.id
}
}
pub struct FutureCheckSat {
_nothing: (),
}
fn future_check_sat() -> FutureCheckSat {
FutureCheckSat { _nothing: () }
}
pub struct Solver<Parser> {
conf: SmtConf,
kid: Child,
stdin: BufWriter<ChildStdin>,
tee: Option<BufWriter<File>>,
smt_parser: RSmtParser,
parser: Parser,
actlit: usize,
}
impl<Parser> Write for Solver<Parser> {
fn write(&mut self, buf: &[u8]) -> std::io::Result<usize> {
if let Some(tee) = self.tee.as_mut() {
let _ = tee.write(buf);
}
self.stdin.write(buf)
}
fn flush(&mut self) -> ::std::io::Result<()> {
if let Some(tee) = self.tee.as_mut() {
let _ = tee.flush();
}
self.stdin.flush()
}
}
impl<Parser> Read for Solver<Parser> {
fn read(&mut self, buf: &mut [u8]) -> std::io::Result<usize> {
self.smt_parser.read(buf)
}
}
macro_rules! tee_write {
($slf:expr, |$w:ident| $($tail:tt)*) => ({
if let Some(ref mut $w) = $slf.tee {
$($tail)*;
writeln!($w)?;
$w.flush() ?
}
let $w = & mut $slf.stdin;
$($tail)*;
$w.flush() ?
});
}
impl<Parser> ::std::ops::Drop for Solver<Parser> {
fn drop(&mut self) {
let _ = self.kill();
()
}
}
impl<Parser> Solver<Parser> {
fn spawn(conf: &SmtConf) -> SmtRes<(Child, BufWriter<ChildStdin>, BufReader<ChildStdout>)> {
let mut kid = Command::new(
conf.get_cmd(),
)
.args(
conf.get_options(),
)
.stdin(Stdio::piped())
.stdout(Stdio::piped())
.stderr(Stdio::piped())
.spawn()
.chain_err::<_, ErrorKind>(|| {
format!(
"While spawning child process with {}",
conf.get_cmd().to_string()
)
.into()
})?;
let mut stdin_opt = None;
::std::mem::swap(&mut stdin_opt, &mut kid.stdin);
let stdin = if let Some(inner) = stdin_opt {
BufWriter::new(inner)
} else {
bail!("could not retrieve solver's stdin")
};
let mut stdout_opt = None;
::std::mem::swap(&mut stdout_opt, &mut kid.stdout);
let stdout = if let Some(inner) = stdout_opt {
BufReader::new(inner)
} else {
bail!("could not retrieve solver's stdout")
};
Ok((kid, stdin, stdout))
}
pub fn new(conf: SmtConf, parser: Parser) -> SmtRes<Self> {
let (kid, stdin, stdout) = Self::spawn(&conf)?;
let smt_parser = RSmtParser::new(stdout);
let tee = None;
let actlit = 0;
Ok(Solver {
kid,
stdin,
tee,
conf,
smt_parser,
parser,
actlit,
})
}
pub fn z3(parser: Parser, cmd: impl Into<String>) -> SmtRes<Self> {
Self::new(SmtConf::z3(cmd), parser)
}
pub fn cvc4(parser: Parser, cmd: impl Into<String>) -> SmtRes<Self> {
Self::new(SmtConf::cvc4(cmd), parser)
}
pub fn yices_2(parser: Parser, cmd: impl Into<String>) -> SmtRes<Self> {
Self::new(SmtConf::yices_2(cmd), parser)
}
pub fn default_z3(parser: Parser) -> SmtRes<Self> {
Self::new(SmtConf::default_z3(), parser)
}
pub fn default_cvc4(parser: Parser) -> SmtRes<Self> {
Self::new(SmtConf::default_cvc4(), parser)
}
pub fn default_yices_2(parser: Parser) -> SmtRes<Self> {
Self::new(SmtConf::default_yices_2(), parser)
}
pub fn conf(&self) -> &SmtConf {
&self.conf
}
pub fn tee(&mut self, file: File) -> SmtRes<()> {
if self.tee.is_some() {
bail!("Trying to tee a solver that's already tee-ed")
}
let mut tee = BufWriter::with_capacity(1000, file);
write!(tee, "; Command:\n; > {}", self.conf.get_cmd())?;
for option in self.conf.get_options() {
write!(tee, " {}", option)?
}
writeln!(tee, "\n")?;
self.tee = Some(tee);
Ok(())
}
pub fn path_tee<P>(&mut self, path: P) -> SmtRes<()>
where
P: AsRef<::std::path::Path>,
{
use std::fs::OpenOptions;
let path: &::std::path::Path = path.as_ref();
let file = OpenOptions::new()
.create(true)
.write(true)
.truncate(true)
.open(path)
.chain_err(|| format!("while opening tee file `{}`", path.to_string_lossy()))?;
self.tee(file)
}
pub fn is_teed(&self) -> bool {
self.tee.is_some()
}
#[cfg(windows)]
pub fn kill(&mut self) -> SmtRes<()> {
let _ = writeln!(self.stdin, "(exit)");
let _ = self.stdin.flush();
let _ = self.kid.kill();
Ok(())
}
#[cfg(not(windows))]
pub fn kill(&mut self) -> SmtRes<()> {
let _ = writeln!(self.stdin, "(exit)");
let _ = self.stdin.flush();
let _ = self.kid.kill();
let join = self
.kid
.try_wait()
.chain_err(|| "waiting for child process to exit")?;
if join.is_none() {
self.kid
.kill()
.chain_err::<_, ErrorKind>(|| "while killing child process".into())?
}
Ok(())
}
#[inline]
fn cmt(file: &mut BufWriter<File>, blah: &str) -> SmtRes<()> {
for line in blah.lines() {
writeln!(file, "; {}", line)?
}
file.flush()?;
Ok(())
}
#[inline]
pub fn comment_args(&mut self, args: std::fmt::Arguments) -> SmtRes<()> {
if let Some(ref mut file) = self.tee {
Self::cmt(file, &format!("{}", args))?
}
Ok(())
}
#[inline]
pub fn comment(&mut self, blah: &str) -> SmtRes<()> {
if let Some(ref mut file) = self.tee {
Self::cmt(file, blah)?
}
Ok(())
}
}
impl<Parser> Solver<Parser> {
#[inline]
pub fn assert<Expr>(&mut self, expr: &Expr) -> SmtRes<()>
where
Expr: ?Sized + Expr2Smt<()>,
{
self.assert_with(expr, ())
}
pub fn check_sat(&mut self) -> SmtRes<bool> {
let future = self.print_check_sat()?;
self.parse_check_sat(future)
}
pub fn check_sat_or_unk(&mut self) -> SmtRes<Option<bool>> {
let future = self.print_check_sat()?;
self.parse_check_sat_or_unk(future)
}
#[inline]
pub fn reset(&mut self) -> SmtRes<()> {
self.actlit = 0;
tee_write! {
self, |w| write_str(w, "(reset)\n") ?
}
Ok(())
}
#[inline]
pub fn declare_const<Sym, Sort>(&mut self, symbol: &Sym, out_sort: &Sort) -> SmtRes<()>
where
Sym: ?Sized + Sym2Smt<()>,
Sort: ?Sized + Sort2Smt,
{
self.declare_const_with(symbol, out_sort, ())
}
#[inline]
pub fn declare_fun<'a, FunSym, ArgSort, Args, OutSort>(
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
) -> SmtRes<()>
where
FunSym: ?Sized + Sym2Smt<()>,
ArgSort: ?Sized + Sort2Smt + 'a,
OutSort: ?Sized + Sort2Smt,
Args: IntoIterator<Item = &'a ArgSort>,
{
self.declare_fun_with(symbol, args, out, ())
}
#[inline]
pub fn define_const<FunSym, OutSort, Body>(
&mut self,
symbol: &FunSym,
out: &OutSort,
body: &Body,
) -> SmtRes<()>
where
OutSort: ?Sized + Sort2Smt,
FunSym: ?Sized + Sym2Smt<()>,
Body: ?Sized + Expr2Smt<()>,
{
self.define_const_with(symbol, out, body, ())
}
#[inline]
pub fn define_fun<'a, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
body: &Body,
) -> SmtRes<()>
where
ArgSort: Sort2Smt + 'a,
OutSort: ?Sized + Sort2Smt,
FunSym: ?Sized + Sym2Smt<()>,
ArgSym: Sym2Smt<()> + 'a,
Body: ?Sized + Expr2Smt<()>,
Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
{
self.define_fun_with(symbol, args, out, body, ())
}
#[inline]
pub fn push(&mut self, n: u8) -> SmtRes<()> {
tee_write! {
self, |w| writeln!(w, "(push {})", n) ?
}
Ok(())
}
#[inline]
pub fn pop(&mut self, n: u8) -> SmtRes<()> {
tee_write! {
self, |w| writeln!(w, "(pop {})", n) ?
}
Ok(())
}
pub fn check_sat_assuming<'a, Ident, Idents>(&mut self, idents: Idents) -> SmtRes<bool>
where
Ident: ?Sized + Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
{
self.check_sat_assuming_with(idents, ())
}
pub fn check_sat_assuming_or_unk<'a, Ident, Idents>(
&mut self,
idents: Idents,
) -> SmtRes<Option<bool>>
where
Ident: ?Sized + Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
{
self.check_sat_assuming_or_unk_with(idents, ())
}
#[inline]
pub fn set_logic(&mut self, logic: Logic) -> SmtRes<()> {
tee_write! {
self, |w| {
write_str(w, "(set-logic ")?;
logic.to_smt2(w, ())?;
write_str(w, ")\n") ?
}
}
Ok(())
}
#[inline]
pub fn set_custom_logic<Str>(&mut self, logic: Str) -> SmtRes<()>
where
Str: AsRef<str>,
{
tee_write! {
self, |w| {
write_str(w, "(set-logic ")?;
write_str(w, logic.as_ref())?;
write_str(w, ")\n") ?
}
}
Ok(())
}
#[inline]
pub fn define_fun_rec<'a, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
body: &Body,
) -> SmtRes<()>
where
ArgSort: Sort2Smt + 'a,
OutSort: ?Sized + Sort2Smt,
FunSym: ?Sized + Sym2Smt<()>,
ArgSym: Sym2Smt<()> + 'a,
Body: ?Sized + Expr2Smt<()>,
Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
{
self.define_fun_rec_with(symbol, args, out, body, ())
}
#[inline]
pub fn define_funs_rec<'a, FunSym, ArgSym, ArgSort, Args, ArgsRef, OutSort, Body, Funs>(
&mut self,
funs: Funs,
) -> SmtRes<()>
where
FunSym: Sym2Smt<()> + 'a,
ArgSym: Sym2Smt<()> + 'a,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt + 'a,
Body: Expr2Smt<()> + 'a,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)> + 'a,
Args: ?Sized,
ArgsRef: 'a + AsRef<Args>,
Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
Funs::IntoIter: Clone,
{
self.define_funs_rec_with(funs, ())
}
pub fn declare_datatypes<'a, Sort, Param, ParamList, Def, DefList, All>(
&mut self,
defs: All,
) -> SmtRes<()>
where
Sort: Sort2Smt + 'a,
Param: Sort2Smt + 'a,
&'a ParamList: IntoIterator<Item = &'a Param> + 'a,
Def: Sort2Smt + 'a,
&'a DefList: IntoIterator<Item = &'a Def> + 'a,
All: IntoIterator<Item = &'a (Sort, usize, ParamList, DefList)> + 'a,
All::IntoIter: Clone,
{
tee_write! {
self, |w| write!(w, "(declare-datatypes (") ?
}
let def_iter = defs.into_iter();
for &(ref sort, arity, _, _) in def_iter.clone() {
tee_write! {
self, |w| {
write!(w, " (")?;
sort.sort_to_smt2(w)?;
write!(w, " {})", arity) ?
}
}
}
tee_write! {
self, |w| write!(w, " ) (") ?
}
for &(_, arity, ref params, ref defs) in def_iter {
tee_write! {
self, |w| {
write!(w, " (")?;
if arity > 0 {
write!(w, "par (")?;
for param in params {
write!(w, " ")?;
param.sort_to_smt2(w)?;
}
write!(w, " ) (") ?
}
}
}
for def in defs {
tee_write! {
self, |w| {
write!(w, " ")?;
def.sort_to_smt2(w) ?
}
}
}
tee_write! {
self, |w| {
write!(w, " )")?;
if arity > 0 {
write!(w, " )") ?
}
}
}
}
tee_write! {
self, |w| writeln!(w, " ) )") ?
}
Ok(())
}
}
impl<Parser> Solver<Parser> {
pub fn get_model<Ident, Type, Value>(&mut self) -> SmtRes<Model<Ident, Type, Value>>
where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser>
+ for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
{
self.print_get_model()?;
self.parse_get_model()
}
pub fn get_model_const<Ident, Type, Value>(&mut self) -> SmtRes<Vec<(Ident, Type, Value)>>
where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser>
+ for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
{
self.print_get_model()?;
self.parse_get_model_const()
}
pub fn get_values<'a, Expr, Exprs, PExpr, PValue>(
&mut self,
exprs: Exprs,
) -> SmtRes<Vec<(PExpr, PValue)>>
where
Parser: for<'b> ExprParser<PExpr, (), &'b mut RSmtParser>
+ for<'b> ValueParser<PValue, &'b mut RSmtParser>,
Expr: ?Sized + Expr2Smt<()> + 'a,
Exprs: IntoIterator<Item = &'a Expr>,
{
self.get_values_with(exprs, ())
.map_err(|e| self.conf.enrich_get_values_error(e))
}
}
impl<Parser> Solver<Parser> {
#[inline]
fn has_actlits(&self) -> bool {
self.actlit > 0
}
#[inline]
pub fn get_actlit(&mut self) -> SmtRes<Actlit> {
let id = self.actlit;
self.actlit += 1;
let next_actlit = Actlit { id };
tee_write! {
self, |w| writeln!(
w, "(declare-fun {}{}{} () Bool)",
ACTLIT_PREF, next_actlit.id, ACTLIT_SUFF
) ?
}
Ok(next_actlit)
}
#[inline]
pub fn de_actlit(&mut self, actlit: Actlit) -> SmtRes<()> {
self.set_actlit(actlit, false)
}
#[inline]
pub fn set_actlit(&mut self, actlit: Actlit, b: bool) -> SmtRes<()> {
tee_write! {
self, |w| {
if b {
write!(w, "(assert ") ?
} else {
write!(w, "(assert (not ") ?
}
actlit.write(w)?;
if b {
writeln!(w, ")") ?
} else {
writeln!(w, ") )") ?
}
}
}
::std::mem::drop(actlit);
Ok(())
}
#[inline]
pub fn assert_act<Expr>(&mut self, actlit: &Actlit, expr: &Expr) -> SmtRes<()>
where
Expr: ?Sized + Expr2Smt<()>,
{
self.assert_act_with(actlit, expr, ())
}
pub fn check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<bool>
where
Actlits: IntoIterator<Item = &'a Actlit>,
{
let future = self.print_check_sat_act(actlits)?;
self.parse_check_sat(future)
}
pub fn check_sat_act_or_unk<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<Option<bool>>
where
Actlits: IntoIterator<Item = &'a Actlit>,
{
let future = self.print_check_sat_act(actlits)?;
self.parse_check_sat_or_unk(future)
}
}
impl<Parser> Solver<Parser> {
#[inline]
pub fn print_check_sat(&mut self) -> SmtRes<FutureCheckSat> {
tee_write! {
self, |w| write_str(w, "(check-sat)\n") ?
}
Ok(future_check_sat())
}
#[inline]
pub fn print_check_sat_act<'a, Actlits>(&mut self, actlits: Actlits) -> SmtRes<FutureCheckSat>
where
Actlits: IntoIterator<Item = &'a Actlit>,
{
match self.conf.get_check_sat_assuming() {
Some(ref cmd) => {
tee_write! {
self, |w| write!(w, "({} (", cmd) ?
}
for actlit in actlits {
tee_write! {
self, |w| {
write!(w, " ")?;
actlit.write(w) ?
}
}
}
tee_write! {
self, |w| write_str(w, ") )\n") ?
}
Ok(future_check_sat())
}
None => {
let msg = format!("{} does not support check-sat-assuming", self.conf.desc());
Err(msg.into())
}
}
}
#[inline]
pub fn parse_check_sat(&mut self, _: FutureCheckSat) -> SmtRes<bool> {
if let Some(res) = self.smt_parser.check_sat()? {
Ok(res)
} else {
Err(ErrorKind::Unknown.into())
}
}
#[inline]
pub fn parse_check_sat_or_unk(&mut self, _: FutureCheckSat) -> SmtRes<Option<bool>> {
self.smt_parser.check_sat()
}
#[inline]
fn print_get_model(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(get-model)\n") ?
}
Ok(())
}
#[allow(dead_code)]
fn print_get_assertions(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(get-assertions)\n") ?
}
Ok(())
}
#[allow(dead_code)]
fn print_get_assignment(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(get-assignment)\n") ?
}
Ok(())
}
#[allow(dead_code)]
fn print_get_unsat_assumptions(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(get-unsat-assumptions)\n") ?
}
Ok(())
}
#[allow(dead_code)]
fn print_get_proof(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(get-proof)\n") ?
}
Ok(())
}
#[allow(dead_code)]
fn print_get_unsat_core(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(get-unsat-core)\n") ?
}
Ok(())
}
fn print_get_values_with<'a, Info, Expr, Exprs>(
&mut self,
exprs: Exprs,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
Expr: ?Sized + Expr2Smt<Info> + 'a,
Exprs: IntoIterator<Item = &'a Expr>,
{
tee_write! {
self, |w| write!(w, "(get-value (") ?
}
for e in exprs {
tee_write! {
self, |w| {
write_str(w, "\n ")?;
e.expr_to_smt2(w, info) ?
}
}
}
tee_write! {
self, |w| write_str(w, "\n) )\n") ?
}
Ok(())
}
pub fn print_check_sat_assuming<'a, Ident, Idents>(
&mut self,
bool_vars: Idents,
) -> SmtRes<FutureCheckSat>
where
Ident: ?Sized + Sym2Smt<()> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
{
self.print_check_sat_assuming_with(bool_vars, ())
}
pub fn print_check_sat_assuming_with<'a, Info, Ident, Idents>(
&mut self,
bool_vars: Idents,
info: Info,
) -> SmtRes<FutureCheckSat>
where
Info: Copy,
Ident: ?Sized + Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
{
match self.conf.get_check_sat_assuming() {
Some(ref cmd) => {
tee_write! {
self, |w| write!(w, "({} (\n ", cmd) ?
}
for sym in bool_vars {
tee_write! {
self, |w| {
write_str(w, " ")?;
sym.sym_to_smt2(w, info) ?
}
}
}
tee_write! {
self, |w| write_str(w, "\n))\n") ?
}
Ok(future_check_sat())
}
None => {
let msg = format!("{} does not support check-sat-assuming", self.conf.desc());
Err(msg.into())
}
}
}
fn parse_get_model<Ident, Type, Value>(&mut self) -> SmtRes<Model<Ident, Type, Value>>
where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser>
+ for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
{
let has_actlits = self.has_actlits();
let res = self.smt_parser.get_model(has_actlits, self.parser);
if res.is_err() && !self.conf.get_models() {
res.chain_err(|| {
"\
Note: model production is not active \
for this SmtConf (`conf.models()`)\
"
})
} else {
res
}
}
fn parse_get_model_const<Ident, Type, Value>(&mut self) -> SmtRes<Vec<(Ident, Type, Value)>>
where
Parser: for<'a> IdentParser<Ident, Type, &'a mut RSmtParser>
+ for<'a> ModelParser<Ident, Type, Value, &'a mut RSmtParser>,
{
let has_actlits = self.has_actlits();
let res = self.smt_parser.get_model_const(has_actlits, self.parser);
if res.is_err() && !self.conf.get_models() {
res.chain_err(|| {
"\
Note: model production is not active \
for this SmtConf (`conf.models()`)\
"
})
} else {
res
}
}
fn parse_get_values_with<Info, Expr, Val>(&mut self, info: Info) -> SmtRes<Vec<(Expr, Val)>>
where
Info: Copy,
Parser: for<'a> ExprParser<Expr, Info, &'a mut RSmtParser>
+ for<'a> ValueParser<Val, &'a mut RSmtParser>,
{
let res = self.smt_parser.get_values(self.parser, info);
if res.is_err() && !self.conf.get_models() {
res.chain_err(|| {
"\
Note: model production is not active \
for this SmtConf (`conf.models()`)\
"
})
} else {
res
}
}
fn get_values_with<'a, Info, Expr, Exprs, PExpr, PValue>(
&mut self,
exprs: Exprs,
info: Info,
) -> SmtRes<Vec<(PExpr, PValue)>>
where
Info: Copy,
Parser: for<'b> ExprParser<PExpr, Info, &'b mut RSmtParser>
+ for<'b> ValueParser<PValue, &'b mut RSmtParser>,
Expr: ?Sized + Expr2Smt<Info> + 'a,
Exprs: IntoIterator<Item = &'a Expr>,
{
self.print_get_values_with(exprs, info)?;
self.parse_get_values_with(info)
}
}
impl<Parser: Send + 'static> Solver<Parser> {
pub unsafe fn async_check_sat_or_unk(&mut self) -> crate::asynch::CheckSatFuture<Parser> {
crate::asynch::CheckSatFuture::new(self)
}
}
impl<Parser> Solver<Parser> {
#[inline]
pub fn declare_sort<Sort>(&mut self, sort: &Sort, arity: u8) -> SmtRes<()>
where
Sort: ?Sized + Sort2Smt,
{
tee_write! {
self, |w| {
write_str(w, "(declare-sort ")?;
sort.sort_to_smt2(w)?;
writeln!(w, " {})", arity) ?
}
}
Ok(())
}
#[inline]
pub fn define_sort<'a, Sort, Arg, Args, Body>(
&mut self,
sort: &Sort,
args: Args,
body: &Body,
) -> SmtRes<()>
where
Sort: ?Sized + Sort2Smt,
Arg: ?Sized + Sort2Smt + 'a,
Body: ?Sized + Sort2Smt,
Args: IntoIterator<Item = &'a Arg>,
{
tee_write! {
self, |w| {
write_str(w, "( define-sort ")?;
sort.sort_to_smt2(w)?;
write_str(w, "\n ( ")?;
}
}
for arg in args {
tee_write! {
self, |w| {
arg.sort_to_smt2(w)?;
write_str(w, " ") ?
}
}
}
tee_write! {
self, |w| {
write_str(w, ")\n ")?;
body.sort_to_smt2(w)?;
write_str(w, "\n)\n") ?
}
}
Ok(())
}
#[inline]
pub fn define_null_sort<Sort, Body>(&mut self, sort: &Sort, body: &Body) -> SmtRes<()>
where
Sort: ?Sized + Sort2Smt,
Body: ?Sized + Sort2Smt,
{
self.define_sort::<Sort, Body, Option<&Body>, Body>(sort, None, body)
}
}
impl<Parser> Solver<Parser> {
#[inline]
pub fn declare_const_with<Info, Sym, Sort>(
&mut self,
symbol: &Sym,
out_sort: &Sort,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
Sym: ?Sized + Sym2Smt<Info>,
Sort: ?Sized + Sort2Smt,
{
tee_write! {
self, |w| {
write_str(w, "(declare-const ")?;
symbol.sym_to_smt2(w, info)?;
write_str(w, " ")?;
out_sort.sort_to_smt2(w)?;
write_str(w, ")\n") ?
}
}
Ok(())
}
#[inline]
pub fn declare_fun_with<'a, Info, FunSym, ArgSort, Args, OutSort>(
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
FunSym: ?Sized + Sym2Smt<Info>,
ArgSort: ?Sized + Sort2Smt + 'a,
OutSort: ?Sized + Sort2Smt,
Args: IntoIterator<Item = &'a ArgSort>,
{
tee_write! {
self, |w| {
write_str(w, "(declare-fun ")?;
symbol.sym_to_smt2(w, info)?;
write_str(w, " ( ") ?
}
}
for arg in args {
tee_write! {
self, |w| {
arg.sort_to_smt2(w)?;
write_str(w, " ") ?
}
}
}
tee_write! {
self, |w| {
write_str(w, ") ")?;
out.sort_to_smt2(w)?;
write_str(w, ")\n") ?
}
}
Ok(())
}
#[inline]
pub fn define_const_with<Info, Sym, Sort, Body>(
&mut self,
symbol: &Sym,
out_sort: &Sort,
body: &Body,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
Sym: ?Sized + Sym2Smt<Info>,
Sort: ?Sized + Sort2Smt,
Body: ?Sized + Expr2Smt<Info>,
{
tee_write! {
self, |w| {
write_str(w, "(define-const ")?;
symbol.sym_to_smt2(w, info)?;
write_str(w, " ")?;
out_sort.sort_to_smt2(w)?;
write_str(w, " ")?;
body.expr_to_smt2(w, info)?;
write_str(w, ")\n") ?
}
}
Ok(())
}
#[inline]
pub fn define_fun_with<'a, Info, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
body: &Body,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
ArgSort: Sort2Smt + 'a,
OutSort: ?Sized + Sort2Smt,
FunSym: ?Sized + Sym2Smt<Info>,
ArgSym: Sym2Smt<Info> + 'a,
Body: ?Sized + Expr2Smt<Info>,
Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
{
tee_write! {
self, |w| {
write_str(w, "(define-fun ")?;
symbol.sym_to_smt2(w, info)?;
write_str(w, " ( ") ?
}
}
for arg in args {
let (ref sym, ref sort) = *arg;
tee_write! {
self, |w| {
write_str(w, "(")?;
sym.sym_to_smt2(w, info)?;
write_str(w, " ")?;
sort.sort_to_smt2(w)?;
write_str(w, ") ") ?
}
}
}
tee_write! {
self, |w| {
write_str(w, ") ")?;
out.sort_to_smt2(w)?;
write_str(w, "\n ")?;
body.expr_to_smt2(w, info)?;
write_str(w, "\n)\n") ?
}
}
Ok(())
}
#[inline]
pub fn define_funs_rec_with<
'a,
Info,
FunSym,
ArgSym,
ArgSort,
Args,
ArgsRef,
OutSort,
Body,
Funs,
>(
&mut self,
funs: Funs,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
FunSym: Sym2Smt<Info> + 'a,
ArgSym: Sym2Smt<Info> + 'a,
ArgSort: Sort2Smt + 'a,
OutSort: Sort2Smt + 'a,
Body: Expr2Smt<Info> + 'a,
&'a Args: IntoIterator<Item = &'a (ArgSym, ArgSort)> + 'a,
Args: ?Sized,
ArgsRef: 'a + AsRef<Args>,
Funs: IntoIterator<Item = &'a (FunSym, ArgsRef, OutSort, Body)>,
Funs::IntoIter: Clone,
{
tee_write! {
self, |w| write_str(w, "(define-funs-rec (\n") ?
}
let fun_iter = funs.into_iter();
for fun in fun_iter.clone() {
let (ref sym, ref args, ref out, _) = *fun;
tee_write! {
self, |w| {
write_str(w, " (")?;
sym.sym_to_smt2(w, info)?;
write_str(w, " ( ") ?
}
}
for arg in args.as_ref() {
tee_write! {
self, |w| {
let (ref sym, ref sort) = * arg;
write_str(w, "(")?;
sym.sym_to_smt2(w, info)?;
write_str(w, " ")?;
sort.sort_to_smt2(w)?;
write_str(w, ") ") ?
}
}
}
tee_write! {
self, |w| {
write_str(w, ") ")?;
out.sort_to_smt2(w)?;
write_str(w, ")\n") ?
}
}
}
tee_write! {
self, |w| write_str(w, " ) (") ?
}
for fun in fun_iter {
let (_, _, _, ref body) = *fun;
tee_write! {
self, |w| {
write_str(w, "\n ")?;
body.expr_to_smt2(w, info) ?
}
}
}
tee_write! {
self, |w| write_str(w, "\n )\n)\n") ?
}
Ok(())
}
#[inline]
pub fn define_fun_rec_with<'a, Info, FunSym, ArgSym, ArgSort, Args, OutSort, Body>(
&mut self,
symbol: &FunSym,
args: Args,
out: &OutSort,
body: &Body,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
ArgSort: Sort2Smt + 'a,
OutSort: ?Sized + Sort2Smt,
FunSym: ?Sized + Sym2Smt<Info>,
ArgSym: Sym2Smt<Info> + 'a,
Body: ?Sized + Expr2Smt<Info>,
Args: IntoIterator<Item = &'a (ArgSym, ArgSort)>,
{
tee_write! {
self, |w| write_str(w, "(define-fun-rec (\n") ?
}
tee_write! {
self, |w| {
write_str(w, " (")?;
symbol.sym_to_smt2(w, info)?;
write_str(w, " ( ") ?
}
}
for arg in args {
let (ref sym, ref sort) = *arg;
tee_write! {
self, |w| {
write_str(w, "(")?;
sym.sym_to_smt2(w, info)?;
write_str(w, " ")?;
sort.sort_to_smt2(w)?;
write_str(w, ") ") ?
}
}
}
tee_write! {
self, |w| {
write_str(w, ") ")?;
out.sort_to_smt2(w)?;
write_str(w, ")\n")?;
write_str(w, " ) (")?;
write_str(w, "\n ")?;
body.expr_to_smt2(w, info)?;
write_str(w, "\n )\n)\n") ?
}
}
Ok(())
}
#[inline]
pub fn assert_act_with<Info, Expr>(
&mut self,
actlit: &Actlit,
expr: &Expr,
info: Info,
) -> SmtRes<()>
where
Info: Copy,
Expr: ?Sized + Expr2Smt<Info>,
{
tee_write! {
self, |w| {
write_str(w, "(assert\n (=>\n ")?;
actlit.write(w)?;
write_str(w, "\n ")?;
expr.expr_to_smt2(w, info)?;
write_str(w, "\n )\n)\n") ?
}
}
Ok(())
}
#[inline]
pub fn assert_with<Info, Expr>(&mut self, expr: &Expr, info: Info) -> SmtRes<()>
where
Info: Copy,
Expr: ?Sized + Expr2Smt<Info>,
{
tee_write! {
self, |w| {
write_str(w, "(assert\n ")?;
expr.expr_to_smt2(w, info)?;
write_str(w, "\n)\n") ?
}
}
Ok(())
}
pub fn check_sat_assuming_with<'a, Info, Ident, Idents>(
&mut self,
idents: Idents,
info: Info,
) -> SmtRes<bool>
where
Info: Copy,
Ident: ?Sized + Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
{
let future = self.print_check_sat_assuming_with(idents, info)?;
self.parse_check_sat(future)
}
pub fn check_sat_assuming_or_unk_with<'a, Info, Ident, Idents>(
&mut self,
idents: Idents,
info: Info,
) -> SmtRes<Option<bool>>
where
Info: Copy,
Ident: ?Sized + Sym2Smt<Info> + 'a,
Idents: IntoIterator<Item = &'a Ident>,
{
let future = self.print_check_sat_assuming_with(idents, info)?;
self.parse_check_sat_or_unk(future)
}
}
impl<Parser> Solver<Parser> {
#[inline]
pub fn set_option<Value: ::std::fmt::Display>(
&mut self,
option: &str,
value: Value,
) -> SmtRes<()> {
match option {
":interactive_mode" => return Err("illegal set-option on interactive mode".into()),
":print_success" => {
return Err("illegal set-option on print success, \
use `SmtConf` to activate it"
.into())
}
_ => (),
};
tee_write! {
self, |w| writeln!(
w, "(set-option {} {})", option, value
) ?
}
Ok(())
}
#[inline]
pub fn produce_unsat_core(&mut self) -> SmtRes<()> {
self.set_option(":produce-unsat-cores", "true")
}
#[inline]
pub fn reset_assertions(&mut self) -> SmtRes<()> {
tee_write! {
self, |w| write_str(w, "(reset-assertions)\n") ?
}
Ok(())
}
#[inline]
pub fn get_info(&mut self, flag: &str) -> SmtRes<()> {
tee_write! {
self, |w| writeln!(w, "(get-info {})", flag) ?
}
Ok(())
}
#[inline]
pub fn get_option(&mut self, option: &str) -> SmtRes<()> {
tee_write! {
self, |w| writeln!(w, "(get-option {})", option) ?
}
Ok(())
}
#[inline]
pub fn set_info(&mut self, attribute: &str) -> SmtRes<()> {
tee_write! {
self, |w| writeln!(w, "(set-info {})", attribute) ?
}
Ok(())
}
#[inline]
pub fn echo(&mut self, text: &str) -> SmtRes<()> {
tee_write! {
self, |w| writeln!(w, "(echo \"{}\")", text) ?
}
Ok(())
}
}