1

Mathsat supports the command check-allsat and Z3 does not support it. Please consider the following example:

(declare-fun m () Bool)
(declare-fun p () Bool)
(declare-fun b () Bool)
(declare-fun c () Bool)
(declare-fun r () Bool)
(declare-fun al () Bool)
(declare-fun all () Bool)
(declare-fun la () Bool)
(declare-fun lal () Bool)
(declare-fun g () Bool)
(declare-fun a () Bool)
(define-fun conjecture () Bool
(and (= (and (not r) c) m) (= p m) (= b m) (= c (not g)) (= (and (not al) (not all)) r)
(=(and la b) al) 
(= (and al la lal) all) (= (and (not g) p a) la) (= (and (not g) (or la a)) lal)))
(assert conjecture)
(check-allsat (m p b c r al all la lal g a))

Executing this code with mathsat all the consistent assignments are obtained. The question is how to determine the number of such consistent assignments using Mathsat?

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Juan Ospina
  • 1,317
  • 1
  • 7
  • 15
  • "The question is how to determine the number of such consistent assignments using Mathsat?" Do you mean "...using Z3?"? If so, have you tried the APIs with model generation, e.g.: http://stackoverflow.com/questions/13395391/z3-finding-all-satisfying-models/13398853#13398853 or http://stackoverflow.com/questions/19578627/model-counting-in-z3py – Taylor T. Johnson Nov 05 '13 at 03:27
  • I mean using Mathsat: how to count the solutions using Mathsat? – Juan Ospina Nov 05 '13 at 11:20

1 Answers1

3

I'm not aware of any command to count the number of solutions. But this can be done easily using MathSAT's API. Create a counter, and increase it each time MathSAT notifies.

static int counter = 0;
static int my_callback(msat_term *model, int size, void *user_data)
{
   counter++; return 1;
}
...
msat_all_sat(env, important, 4, my_callback, &data);
sean
  • 1,632
  • 2
  • 15
  • 34