what's the function of CheckAxioms in Opensmt?

[Ming]

Hello,

In the file "CoreSMTSovler.C“ ,there is a statement " res = checkAxioms( );“ in search() function；

we can check Theory consistency using "checkTheory()", why we use checkAxioms()? What's different between them?

By the way,what's meaning of the parameter of CheckTheory()?

Thanks,

Ming

 

[Roberto Bruttomesso]

checkAxioms was meant for checking additional array axioms, but it is
never used in practice. The parameter for checkTheory tells whether we
are checking a partial model (incomplete methods can be used) or a
complete model (complete methods have to be used)

Roberto

> --
> You received this message because you are subscribed to the Google Groups
> "opensmt" group.
> To view this discussion on the web visit
> https://groups.google.com/d/msg/opensmt/-/uoqyMMDA8t4J.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to
> opensmt+u...@googlegroups.com.
> For more options, visit this group at
> http://groups.google.com/group/opensmt?hl=en.



--
Roberto Bruttomesso, PhD - http://tinyurl.com/r0b3r70

[Ming]

Dear Roberto ,

Thank you for your answer!

在 2012年7月12日星期四UTC+8下午3时16分21秒，Roberto写道：

checkAxioms was meant for checking additional array axioms, but it is
never used in practice. The parameter for checkTheory tells whether we
are checking a partial model (incomplete methods can be used) or a
complete model (complete methods have to be used)

Roberto

On Thu, Jul 12, 2012 at 3:47 AM, Ming <lu.d...@gmail.com> wrote:
> Hello,
> In the file "CoreSMTSovler.C“ ,there is a statement " res = checkAxioms( );“
> in search() function；
> we can check Theory consistency using "checkTheory()", why we use
> checkAxioms()? What's different between them?
> By the way,what's meaning of the parameter of CheckTheory()?
> Thanks,
> Ming
>
>
> --
> You received this message because you are subscribed to the Google Groups
> "opensmt" group.
> To view this discussion on the web visit
> https://groups.google.com/d/msg/opensmt/-/uoqyMMDA8t4J.
> To post to this group, send email to ope...@googlegroups.com.
> To unsubscribe from this group, send email to

> opensmt+unsubscribe@googlegroups.com.