change the default solver to z3 and add manual switch

z3 is only slow for corner cases, while yices2 is actually suprisingly terrible

modules/json/src/lib.zz

@@ -93,6 +93,7 @@ export fn next(Parser+tail mut*self, err::Err+et mut *e, deserialize_t de, void
 }
 
 export fn push(Parser+tail mut *self, err::Err+et mut *e, char *str, usize strlen)
+    @solver = yices2
     where err::checked(*e)
     where len(str) >= strlen
     where tail > 2

modules/slice/src/mut_slice.zz

@@ -24,6 +24,7 @@ export fn borrow(MutSlice mut*self) -> MutSlice *
 }
 
 export fn new(u8 mut*mem, usize size) -> MutSlice
+    @solver = yices2
     where len(mem) >= size
     model return.slice.size == size
     model return.slice.size == len(return.slice.mem)
@@ -43,6 +44,7 @@ export fn new(u8 mut*mem, usize size) -> MutSlice
 
 
 export inline fn mem(MutSlice mut * self) -> u8 mut*
+    @solver = yices2
     model len(return) >= self->slice.size
     model len(return) >= self->at
 {
@@ -52,6 +54,7 @@ export inline fn mem(MutSlice mut * self) -> u8 mut*
 }
 
 export fn push(MutSlice mut * self, u8 b) -> bool
+    @solver = yices2
     where self->slice.size >= 1
     model self->at <= self->slice.size
 {
@@ -66,6 +69,7 @@ export fn push(MutSlice mut * self, u8 b) -> bool
 }
 
 export fn push16(MutSlice mut * self, u16 b) -> bool
+    @solver = yices2
     where self->slice.size >= 2
     model self->at <= self->slice.size
 {
@@ -80,6 +84,7 @@ export fn push16(MutSlice mut * self, u16 b) -> bool
 }
 
 export fn push32(MutSlice mut * self, u32 b) -> bool
+    @solver = yices2
     where self->slice.size >= 4
     model self->at <= self->slice.size
 {
@@ -94,6 +99,7 @@ export fn push32(MutSlice mut * self, u32 b) -> bool
 }
 
 export fn push64(MutSlice mut * self, u64 b) -> bool
+    @solver = yices2
     where self->slice.size > 8
 {
     if self->at > self->slice.size - 8 {

modules/string/src/lib.zz

@@ -61,6 +61,7 @@ export fn clear(String+tail mut * self)
 }
 
 export fn push(String+t mut * self, char cstr) -> bool
+    @solver = yices2
     where t > 2
     model self->len < t
     model nullterm(self->mem)
@@ -93,6 +94,7 @@ export fn pop(String+t mut * self) -> bool
 }
 
 export fn append_cstr(String+t mut * self, char * cstr)
+    @solver = yices2
     where nullterm(cstr)
     model nullterm(self->mem)
     model self->len < t
@@ -112,6 +114,7 @@ export fn append_cstr(String+t mut * self, char * cstr)
 }
 
 export fn append(String+t mut * self, String+t2 * other)
+    @solver = yices2
     model self->len < t
     model nullterm(self->mem)
 {
@@ -131,6 +134,7 @@ export fn append(String+t mut * self, String+t2 * other)
 
 
 export fn append_bytes(String+t mut* self, u8* bytes, usize mut inlen)
+    @solver = yices2
     where len(bytes) >= inlen
     model self->len < t
     model nullterm(self->mem)
@@ -220,6 +224,7 @@ export fn fgets(String+tail mut* self, FILE mut * unsafe stream) -> bool
 
 
 export fn substr(String+tail *self, usize from, usize mut size, String+tail2 mut* other)
+    @solver = yices2
     where tail  > 0
     where tail2 > 0
     model self->len  < tail

modules/time/src/lib.zz

@@ -33,7 +33,9 @@ export fn to_seconds(Time *self) -> u64 {
     return self->secs;
 }
 
-export fn to_millis(Time *self) -> u64 {
+export fn to_millis(Time *self) -> u64
+    @prover = yices2
+{
     if self->secs > (u64)UINT64_MAX/1000 {
         return (u64)UINT64_MAX;
     }

solvecomp.sh

@@ -0,0 +1,20 @@
+#!/bin/zsh
+echo "z3 , yices2, fn"
+for i in *.smt2
+do
+
+
+TIME_Z3=$(
+    (time z3 $i  >/dev/null)  2>&1  | rev | cut -d ' ' -f 2 | rev | tr -d '.'
+)
+TIME_YI=$(
+    (time yices_smt2  --incremental $i  >/dev/null)  2>&1  | rev | cut -d ' ' -f 2 | rev | tr -d '.'
+)
+
+    if [ $TIME_Z3 -gt $TIME_YI ]
+    then
+        echo -e "\e[31m$TIME_Z3\e[39m , \e[32m$TIME_YI\e[39m , $i"
+    else
+        echo -e "\e[32m$TIME_Z3\e[39m , \e[31m$TIME_YI\e[39m , $i"
+    fi
+done

src/ast.rs

@@ -84,6 +84,7 @@ pub enum Def {
         nameloc:    Location,
         ret:        Option<AnonArg>,
         args:       Vec<NamedArg>,
+        hints:      HashMap<String, String>,
         attr:       HashMap<String, Location>,
         body:       Block,
         vararg:     bool,

src/parser.rs

@@ -132,6 +132,7 @@ fn p(n: &Path, features: HashMap<String, bool> ) -> Result<Module, pest::error::
                 let mut callassert = Vec::new();
                 let mut calleffect = Vec::new();
                 let mut vis = Visibility::Object;
+                let mut hints = HashMap::new();
 
                 for part in decl {
                     match part.as_rule() {
@@ -194,6 +195,12 @@ fn p(n: &Path, features: HashMap<String, bool> ) -> Result<Module, pest::error::
                         Rule::block => {
                             body = Some(parse_block((file_str, n), features.clone(), part));
                         },
+                        Rule::fn_vattr => {
+                            let mut part = part.into_inner();
+                            let key  = part.next().unwrap().as_str().to_string();
+                            let val  = part.next().unwrap().as_str().to_string();
+                            hints.insert(key, val);
+                        }
                         e => panic!("unexpected rule {:?} in function", e),
                     }
                 }
@@ -208,6 +215,7 @@ fn p(n: &Path, features: HashMap<String, bool> ) -> Result<Module, pest::error::
                                 nameloc,
                                 ret,
                                 attr,
+                                hints,
                                 args,
                                 body: body.unwrap(),
                                 vararg,

src/smt.rs

@@ -740,20 +740,20 @@ impl Solver {
         }
     }
 
-    pub fn new(module_name: String) -> Self {
+    pub fn new(module_name: String, hints: &HashMap<String, String>) -> Self {
 
         //Config::set_global_param_value(":model.partial", "true");
         //Config::set_global_param_value(":parallel.enable", "true");
         //config.set_model_generation(true);
 
 
 
-        let conf = if which::which("yices_smt2_mt").is_ok() {
+        let conf = if let (Some("yices2"), Ok(_)) = (hints.get("solver").as_ref().map(|s|s.as_str()), which::which("yices_smt2_mt")) {
             rsmt2::SmtConf::yices_2()
         } else if which::which("z3").is_ok() {
             rsmt2::SmtConf::z3()
         } else {
-            panic!("z3 or yices_smt2_mt required in PATH")
+            panic!("z3 required in PATH")
         };
 
 
@@ -764,7 +764,9 @@ impl Solver {
         let mut solver = rsmt2::Solver::new(conf, Rsmt2Junk).unwrap();
         solver.path_tee(outfile).unwrap();
 
-        write!(solver,"(set-option :produce-unsat-cores true)\n").unwrap();
+        //insanly slow and we don't actually use it.
+        //write!(solver,"(set-option :produce-unsat-cores true)\n").unwrap();
+
         write!(solver,"(set-logic QF_UFBV)\n").unwrap();
         //write!(solver,"(set-option :parallel.enable true)\n").unwrap();
         //write!(solver,"(set-option :timeout {})\n", TIMEOUT.load(Ordering::Relaxed) as u64).unwrap();

src/symbolic.rs

@@ -3129,7 +3129,7 @@ impl Symbolic {
         ]));
     }
 
-    fn new(module_name: &Name) -> Self {
+    fn new(module_name: &Name, hints: &HashMap<String, String>) -> Self {
         Symbolic {
             stack:  vec![
                 Scope {
@@ -3139,7 +3139,7 @@ impl Symbolic {
                 }
             ],
             memory:  Default::default(),
-            ssa:     Solver::new(module_name.to_string()),
+            ssa:     Solver::new(module_name.to_string(), hints),
             builtin: Default::default(),
             defs:    HashMap::new(),
             current_module_name:    module_name.human_name(),
@@ -3311,9 +3311,9 @@ pub fn execute(module: &mut flatten::Module) -> bool {
     let mut defs        = Vec::new();
     let mut function_at = Vec::new();
     for (i, (d,_,defined_here)) in module.d.clone().into_iter().enumerate() {
-        if let ast::Def::Function{..} = d.def {
+        if let ast::Def::Function{ref hints, ..} = d.def {
             if defined_here {
-                function_at.push((i, d.name.clone(), module.clone()));
+                function_at.push((i, d.name.clone(), module.clone(), hints.clone()));
             }
         }
         defs.push(d.clone());
@@ -3322,16 +3322,16 @@ pub fn execute(module: &mut flatten::Module) -> bool {
 
 
     // execute one in serial on the borrowed module to get modifications to globals
-    if let Some((at, name, _)) = function_at.pop() {
-        let mut sym = Symbolic::new(&Name::from(&name));
+    if let Some((at, name, _, hints)) = function_at.pop() {
+        let mut sym = Symbolic::new(&Name::from(&name), &hints);
         if let Err(e) = sym.execute_module(module, at) {
             parser::emit_error(e.message.clone(), &e.details);
             return false;
         }
     }
 
-    let repl = function_at.into_par_iter().map(|(at, name, mut module)|{
-        let mut sym = Symbolic::new(&Name::from(&name));
+    let repl = function_at.into_par_iter().map(|(at, name, mut module, hints)|{
+        let mut sym = Symbolic::new(&Name::from(&name), &hints);
         match sym.execute_module(&mut module, at) {
             Err(e) => {
                 parser::emit_error(e.message.clone(), &e.details);

src/zz.pest

@@ -91,12 +91,13 @@ named_typei = _{ type_part  ~ named_typei | ident }
 
 // declarations
 
+fn_vattr    = {"@" ~ ident ~ "=" ~ ident }
 fn_attr     = {"inline" | "extern"}
 fn_args     = { named_type ~ ( "," ~ named_type )* ~ ( "," ~ vararg)? ~  ","? }
 ret_arg     = {"->" ~ anon_type }
 call_assert = {"where" ~ expr }
 call_effect = {"model" ~ expr }
-function    = { ( exported | key_shared)? ~ fn_attr* ~ "fn" ~ ident ~ "(" ~ fn_args? ~")" ~ ret_arg? ~ ( call_assert | call_effect)* ~ block }
+function    = { ( exported | key_shared)? ~ fn_attr* ~ "fn" ~ ident ~ "(" ~ fn_args? ~")" ~ ret_arg? ~ ( fn_vattr | call_assert | call_effect)* ~ block }
 fntype      = { ( exported | key_shared)? ~ fn_attr* ~ "fntype" ~ ident ~ "(" ~ fn_args? ~")" ~ ret_arg? ~ ";" }
 theory      = { ( exported | key_shared)? ~ "theory" ~ ident ~ "(" ~ fn_args? ~")" ~ ret_arg? ~ ";" }