Version 1 (modified by ibongartz, 7 months ago) (diff)

First version of plugin clips-smt description.

CLIPS-based SMT Planning approach plugin

The plugin offers the functionality to expand a order connected to some goal. Once it is called via some rule in CLIPS a loop function ClipsSmtThread::loop() is activated.

  1. Clear data of previous calls and preprocess data given via a protobuf datastructure consisting of the current worldstate with ClipsSmtThread::clips_smt_init_game().
  2. Encode a formula based on the extracted data with ClipsSmtThread::clips_smt_encoder().
  3. Solve the formula and store the plan information of the model with ClipsSmtThread::clips_smt_solve(z3::expr formula).
  4. Tell the agent that the loop reached its end via
    envs_[data_env]->assert_fact_f("(smt-plan-complete \"%s\")", data_handle.c_str());

Now the agent has the possibility to demand a protobuf datastructure consisting of the plan by calling following method

ClipsSmtThread::clips_smt_request(std::string env_name, std::string handle, void *msgptr)

The principles of the encoder can be found here.